[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
k : α
n : ℕ
x a a' : α
h : k + a = a'
⊢ k + term n x a = term n x a'
[PROOFSTEP]
simp [h.symm, term, add_comm, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
k : α
n : ℤ
x a a' : α
h : k + a = a'
⊢ k + termg n x a = termg n x a'
[PROOFSTEP]
simp [h.symm, termg, add_comm, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
x a k a' : α
h : a + k = a'
⊢ term n x a + k = term n x a'
[PROOFSTEP]
simp [h.symm, term, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a k a' : α
h : a + k = a'
⊢ termg n x a + k = termg n x a'
[PROOFSTEP]
simp [h.symm, termg, add_assoc]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
n₁ : ℕ
x a₁ : α
n₂ : ℕ
a₂ : α
n' : ℕ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ term n₁ x a₁ + term n₂ x a₂ = term n' x a'
[PROOFSTEP]
simp [h₁.symm, h₂.symm, term, add_nsmul, add_assoc, add_left_comm]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'
[PROOFSTEP]
simp [h₁.symm, h₂.symm, termg, add_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)
[PROOFSTEP]
exact add_add_add_comm (n₁ • x) a₁ (n₂ • x) a₂
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
x a : α
⊢ term 0 x a = a
[PROOFSTEP]
simp [term, zero_nsmul, one_nsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
x a : α
⊢ termg 0 x a = a
[PROOFSTEP]
simp [termg, zero_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -termg n x a = termg n' x a'
[PROOFSTEP]
simp [h₂.symm, h₁.symm, termg]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -a + -(n • x) = -(n • x) + -a
[PROOFSTEP]
exact add_comm _ _
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
c : ℕ
⊢ smul c 0 = 0
[PROOFSTEP]
simp [smul, nsmul_zero]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
c : ℤ
⊢ smulg c 0 = 0
[PROOFSTEP]
simp [smulg, zsmul_zero]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
c n : ℕ
x a : α
n' : ℕ
a' : α
h₁ : c * n = n'
h₂ : smul c a = a'
⊢ smul c (term n x a) = term n' x a'
[PROOFSTEP]
simp [h₂.symm, h₁.symm, term, smul, nsmul_add, mul_nsmul']
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
c n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : c * n = n'
h₂ : smulg c a = a'
⊢ smulg c (termg n x a) = termg n' x a'
[PROOFSTEP]
simp [h₂.symm, h₁.symm, termg, smulg, zsmul_add, mul_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
x : α
⊢ x = term 1 x 0
[PROOFSTEP]
simp [term]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
x : α
⊢ x = termg 1 x 0
[PROOFSTEP]
simp [termg]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
x x' : α
h : x = x'
⊢ x = term 1 x' 0
[PROOFSTEP]
simp [term, h]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
x x' : α
h : x = x'
⊢ x = termg 1 x' 0
[PROOFSTEP]
simp [termg, h]
[GOAL]
α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a - b = c
[PROOFSTEP]
rw [sub_eq_add_neg, h]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
l : ℕ
r : α
tl : ℕ
tr t : α
prl : l = tl
prr : r = tr
prt : smul tl tr = t
⊢ smul l r = t
[PROOFSTEP]
simp [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
l : ℤ
r : α
tl : ℤ
tr t : α
prl : l = tl
prr : r = tr
prt : smulg tl tr = t
⊢ smulg l r = t
[PROOFSTEP]
simp [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
l : ℕ
r : α
tl : ℕ
zl : ℤ
tr t : α
prl₁ : l = tl
prl₂ : ↑tl = zl
prr : r = tr
prt : smulg zl tr = t
⊢ smul l r = t
[PROOFSTEP]
simp [← prt, prl₁, ← prl₂, prr, smul, smulg, coe_nat_zsmul]
[GOAL]
α : Type u_1
inst✝ : AddCommMonoid α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t
[PROOFSTEP]
rw [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t
[PROOFSTEP]
rw [prl, prr, prt]
[GOAL]
α : Type u_1
inst✝ : AddCommGroup α
a ta t : α
pra : a = ta
prt : -ta = t
⊢ -a = t
[PROOFSTEP]
simp [pra, prt]


[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b = 0
⊢ a + b = 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b ≤ 0
⊢ a + b ≤ 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b < 0
⊢ a + b < 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a ≤ 0
hb : b = 0
⊢ a + b ≤ 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a < 0
hb : b = 0
⊢ a + b < 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
inst✝ : StrictOrderedRing α
a b : α
ha : a < 0
hb : 0 < b
this : -b * a > 0
⊢ 0 < -(b * a)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a b : α
ha : a ≤ 0
hb : 0 < b
this : -b * a ≥ 0
⊢ b * a ≤ 0
[PROOFSTEP]
simpa
  -- used alongside `mul_neg` and `mul_nonpos`, so has the same argument pattern for uniformity
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
x✝ : 0 < b
⊢ b * a = 0
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
x✝ : R a 0
h : b = 0
⊢ a * b = 0
[PROOFSTEP]
simp [h]
  -- used in the `nlinarith` normalization steps. The `_` argument is for uniformity.
[GOAL]
α : Type u_1
R : α → α → Prop
inst✝ : Semiring α
a b : α
h : a = 0
x✝ : R b 0
⊢ a * b = 0
[PROOFSTEP]
simp [h]


[GOAL]
x y r : ℕ
hr : y * y + r = x
hle : Nat.ble r (2 * y) = true
⊢ Nat.sqrt x = y
[PROOFSTEP]
rw [← hr, ← pow_two]
[GOAL]
x y r : ℕ
hr : y * y + r = x
hle : Nat.ble r (2 * y) = true
⊢ Nat.sqrt (y ^ 2 + r) = y
[PROOFSTEP]
rw [two_mul] at hle
[GOAL]
x y r : ℕ
hr : y * y + r = x
hle : Nat.ble r (y + y) = true
⊢ Nat.sqrt (y ^ 2 + r) = y
[PROOFSTEP]
exact Nat.sqrt_add_eq' _ (Nat.le_of_ble_eq_true hle)


[GOAL]
x y : ℤ
d : ℕ
hd : Int.gcd x y = d
h : Nat.beq d 1 = false
⊢ ¬IsCoprime x y
[PROOFSTEP]
rw [Int.isCoprime_iff_gcd_eq_one, hd]
[GOAL]
x y : ℤ
d : ℕ
hd : Int.gcd x y = d
h : Nat.beq d 1 = false
⊢ ¬d = 1
[PROOFSTEP]
exact Nat.ne_of_beq_eq_false h


[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedSemiring A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e
[PROOFSTEP]
rw [NormNum.IsNat.to_eq h rfl]
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedSemiring A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n
[PROOFSTEP]
apply Nat.cast_pos.2
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedSemiring A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < n
[PROOFSTEP]
simpa using w
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : OrderedSemiring A
h : NormNum.IsNat e n
⊢ 0 ≤ e
[PROOFSTEP]
rw [NormNum.IsNat.to_eq h rfl]
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : OrderedSemiring A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n
[PROOFSTEP]
exact Nat.cast_nonneg n
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ e ≠ 0
[PROOFSTEP]
rw [NormNum.IsInt.neg_to_eq h rfl]
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ -↑n ≠ 0
[PROOFSTEP]
simp only [ne_eq, neg_eq_zero]
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ ¬↑n = 0
[PROOFSTEP]
apply ne_of_gt
[GOAL]
case h
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℕ
inst✝ : StrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ 0 < ↑n
[PROOFSTEP]
simpa using w
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e
[PROOFSTEP]
have pos_invOf_d : (0 < ⅟(d : A)) := pos_invOf_of_invertible_cast d
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
⊢ 0 < e
[PROOFSTEP]
have pos_n : (0 < (n : A)) := Int.cast_pos (n := n) |>.2 (of_decide_eq_true h)
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < e
[PROOFSTEP]
rw [eq]
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < ↑n * ⅟↑d
[PROOFSTEP]
exact mul_pos pos_n pos_invOf_d
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e
[PROOFSTEP]
rw [eq, of_decide_eq_true h]
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
[PROOFSTEP]
simp
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
⊢ e ≠ 0
[PROOFSTEP]
have pos_invOf_d : (0 < ⅟(d : A)) := pos_invOf_of_invertible_cast d
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
⊢ e ≠ 0
[PROOFSTEP]
have neg_n : ((n : A) < 0) := Int.cast_lt_zero (n := n) |>.2 (of_decide_eq_true h)
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
⊢ e ≠ 0
[PROOFSTEP]
have neg := mul_neg_of_neg_of_pos neg_n pos_invOf_d
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ e ≠ 0
[PROOFSTEP]
rw [eq]
[GOAL]
u : Level
α : Q(Type u)
zα : Q(Zero «$α»)
pα : Q(PartialOrder «$α»)
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n < 0) = true
pos_invOf_d : 0 < ⅟↑d
neg_n : ↑n < 0
neg : ↑n * ⅟↑d < 0
⊢ ↑n * ⅟↑d ≠ 0
[PROOFSTEP]
exact ne_iff_lt_or_gt.2 (Or.inl neg)


[GOAL]
⊢ 0 < Complex.I.im
[PROOFSTEP]
simp
[GOAL]
z : ℍ
⊢ 0 < ↑Complex.normSq ↑z
[PROOFSTEP]
rw [Complex.normSq_pos]
[GOAL]
z : ℍ
⊢ ↑z ≠ 0
[PROOFSTEP]
exact z.ne_zero
[GOAL]
z : ℍ
⊢ 0 < (-↑z)⁻¹.im
[PROOFSTEP]
simpa using div_pos z.property (normSq_pos z)
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : cd ≠ 0
⊢ ↑(cd 0) * ↑z + ↑(cd 1) ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
⊢ cd = 0
[PROOFSTEP]
have : cd 0 = 0 := by
  -- we will need this twice
  apply_fun Complex.im at h
  simpa only [z.im_ne_zero, Complex.add_im, add_zero, coe_im, zero_mul, or_false_iff, Complex.ofReal_im,
    Complex.zero_im, Complex.mul_im, mul_eq_zero] using h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
⊢ cd 0 = 0
[PROOFSTEP]
apply_fun Complex.im at h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : (↑(cd 0) * ↑z + ↑(cd 1)).im = 0.im
⊢ cd 0 = 0
[PROOFSTEP]
simpa only [z.im_ne_zero, Complex.add_im, add_zero, coe_im, zero_mul, or_false_iff, Complex.ofReal_im, Complex.zero_im,
  Complex.mul_im, mul_eq_zero] using h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
this : cd 0 = 0
⊢ cd = 0
[PROOFSTEP]
simp only [this, zero_mul, Complex.ofReal_zero, zero_add, Complex.ofReal_eq_zero] at h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd = 0
[PROOFSTEP]
ext i
[GOAL]
case h
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
i : Fin 2
⊢ cd i = OfNat.ofNat 0 i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.head
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd { val := 0, isLt := (_ : 0 < 2) } = OfNat.ofNat 0 { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
assumption
[GOAL]
case h.tail.head
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd { val := 1, isLt := (_ : (fun a => a < 2) 1) } = OfNat.ofNat 0 { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
assumption
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom g z ≠ 0
[PROOFSTEP]
intro H
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
⊢ False
[PROOFSTEP]
have DET := (mem_glpos _).1 g.prop
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < ↑(↑GeneralLinearGroup.det ↑g)
⊢ False
[PROOFSTEP]
have hz := z.prop
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < ↑(↑GeneralLinearGroup.det ↑g)
hz : 0 < (↑z).im
⊢ False
[PROOFSTEP]
simp only [GeneralLinearGroup.det_apply_val] at DET
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
⊢ False
[PROOFSTEP]
have H1 : (↑ₘg 1 0 : ℝ) = 0 ∨ z.im = 0 := by simpa [num, denom] using congr_arg Complex.im H
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
⊢ ↑↑g 1 0 = 0 ∨ im z = 0
[PROOFSTEP]
simpa [num, denom] using congr_arg Complex.im H
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0 ∨ im z = 0
⊢ False
[PROOFSTEP]
cases' H1 with H1
[GOAL]
case inl
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0
⊢ False
[PROOFSTEP]
simp only [H1, Complex.ofReal_zero, denom, zero_mul, zero_add, Complex.ofReal_eq_zero] at H
[GOAL]
case inl
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0
H : ↑↑g 1 1 = 0
⊢ False
[PROOFSTEP]
rw [Matrix.det_fin_two (↑ₘg : Matrix (Fin 2) (Fin 2) ℝ)] at DET
[GOAL]
case inl
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
DET : 0 < ↑↑g 0 0 * ↑↑g 1 1 - ↑↑g 0 1 * ↑↑g 1 0
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0
H : ↑↑g 1 1 = 0
⊢ False
[PROOFSTEP]
simp only [H, H1, mul_zero, sub_zero, lt_self_iff_false] at DET
[GOAL]
case inr
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
h✝ : im z = 0
⊢ False
[PROOFSTEP]
change z.im > 0 at hz
[GOAL]
case inr
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
h✝ : im z = 0
hz : im z > 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (smulAux' g z).im = det ↑↑g * im z / ↑Complex.normSq (denom g z)
[PROOFSTEP]
rw [smulAux', Complex.div_im]
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (num g z).im * (denom g z).re / ↑Complex.normSq (denom g z) -
      (num g z).re * (denom g z).im / ↑Complex.normSq (denom g z) =
    det ↑↑g * im z / ↑Complex.normSq (denom g z)
[PROOFSTEP]
field_simp [smulAux', num, denom]
  -- porting note: the local notation still didn't work here
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑↑g 0 0 * im z * (↑↑g 1 0 * re z + ↑↑g 1 1) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) -
      (↑↑g 0 0 * re z + ↑↑g 0 1) * (↑↑g 1 0 * im z) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    det ↑↑g * im z / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))
[PROOFSTEP]
rw [Matrix.det_fin_two ((g : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)]
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑↑g 0 0 * im z * (↑↑g 1 0 * re z + ↑↑g 1 1) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) -
      (↑↑g 0 0 * re z + ↑↑g 0 1) * (↑↑g 1 0 * im z) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑↑g 0 0 * ↑↑g 1 1 - ↑↑g 0 1 * ↑↑g 1 0) * im z / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))
[PROOFSTEP]
ring
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ 0 < (smulAux' g z).im
[PROOFSTEP]
rw [smulAux'_im]
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ 0 < det ↑↑g * im z / ↑Complex.normSq (denom g z)
[PROOFSTEP]
convert mul_pos ((mem_glpos _).1 g.prop) (div_pos z.im_pos (Complex.normSq_pos.mpr (denom_ne_zero g z))) using 1
[GOAL]
case h.e'_4
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ det ↑↑g * im z / ↑Complex.normSq (denom g z) = ↑(↑GeneralLinearGroup.det ↑g) * (im z / ↑Complex.normSq (denom g z))
[PROOFSTEP]
simp only [GeneralLinearGroup.det_apply_val]
[GOAL]
case h.e'_4
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ det ↑↑g * im z / ↑Complex.normSq (denom g z) = det ↑↑g * (im z / ↑Complex.normSq (denom g z))
[PROOFSTEP]
ring
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom (x * y) z = denom x (smulAux y z) * denom y z
[PROOFSTEP]
change _ = (_ * (_ / _) + _) * _
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom (x * y) z = (↑(↑↑x 1 0) * (num y z / denom y z) + ↑(↑↑x 1 1)) * denom y z
[PROOFSTEP]
field_simp [denom_ne_zero]
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom (x * y) z = ↑(↑↑x 1 0) * num y z + ↑(↑↑x 1 1) * denom y z
[PROOFSTEP]
simp only [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, denom, num, Subgroup.coe_mul, GeneralLinearGroup.coe_mul,
  Fintype.univ_ofSubsingleton, Fin.mk_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
  Complex.ofReal_mul]
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (↑(↑↑x 1 0) * ↑(↑↑y 0 0) + ↑(↑↑x 1 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 1 0) * ↑(↑↑y 0 1) + ↑(↑↑x 1 1) * ↑(↑↑y 1 1)) =
    ↑(↑↑x 1 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 1 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))
[PROOFSTEP]
ring
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ smulAux (x * y) z = smulAux x (smulAux y z)
[PROOFSTEP]
ext1
  -- Porting note: was `change _ / _ = (_ * (_ / _) + _) * _`
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑(smulAux (x * y) z) = ↑(smulAux x (smulAux y z))
[PROOFSTEP]
change _ / _ = (_ * (_ / _) + _) / _
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (x * y) z / denom (x * y) z = (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)
[PROOFSTEP]
rw [denom_cocycle]
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (x * y) z / (denom x (smulAux y z) * denom y z) =
    (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)
[PROOFSTEP]
field_simp [denom_ne_zero]
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (x * y) z * (denom y z * denom x (smulAux y z)) =
    (↑(↑↑x 0 0) * num y z + ↑(↑↑x 0 1) * denom y z) * (denom x (smulAux y z) * denom y z)
[PROOFSTEP]
simp only [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, num, denom, Subgroup.coe_mul, GeneralLinearGroup.coe_mul,
  Fintype.univ_ofSubsingleton, Fin.mk_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
  Complex.ofReal_mul]
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ((↑(↑↑x 0 0) * ↑(↑↑y 0 0) + ↑(↑↑x 0 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 0 0) * ↑(↑↑y 0 1) + ↑(↑↑x 0 1) * ↑(↑↑y 1 1))) *
      ((↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)) * (↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1))) =
    (↑(↑↑x 0 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 0 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))) *
      ((↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1)) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)))
[PROOFSTEP]
ring
[GOAL]
z : ℍ
⊢ 1 • z = z
[PROOFSTEP]
ext1
[GOAL]
case h
z : ℍ
⊢ ↑(1 • z) = ↑z
[PROOFSTEP]
change _ / _ = _
[GOAL]
case h
z : ℍ
⊢ num 1 z / denom 1 z = ↑z
[PROOFSTEP]
simp [num, denom]
[GOAL]
Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
⊢ det ↑↑↑g = 1
[PROOFSTEP]
simp only [SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, SpecialLinearGroup.det_coe, coe']
[GOAL]
Γ : Subgroup SL(2, ℤ)
⊢ ∀ (x : SL(2, ℤ)) (y : { x // x ∈ GL(2, ℝ)⁺ }) (z : ℍ), (x • y) • z = x • y • z
[PROOFSTEP]
intro s g z
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : SL(2, ℤ)
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (s • g) • z = s • g • z
[PROOFSTEP]
simp only [SLOnGLPos_smul_apply]
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : SL(2, ℤ)
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (↑s * g) • z = s • g • z
[PROOFSTEP]
apply mul_smul'
[GOAL]
Γ : Subgroup SL(2, ℤ)
⊢ ∀ (x : { x // x ∈ Γ }) (y : { x // x ∈ GL(2, ℝ)⁺ }) (z : ℍ), (x • y) • z = x • y • z
[PROOFSTEP]
intro s g z
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (s • g) • z = s • g • z
[PROOFSTEP]
simp only [subgroup_on_glpos_smul_apply]
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (↑↑s * g) • z = s • g • z
[PROOFSTEP]
apply mul_smul'
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : SL(2, ℤ)
z : ℍ
⊢ (s • g) • z = s • g • z
[PROOFSTEP]
rw [subgroup_on_SL_apply]
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : SL(2, ℤ)
z : ℍ
⊢ (↑s * g) • z = s • g • z
[PROOFSTEP]
apply MulAction.mul_smul
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ -g • z = g • z
[PROOFSTEP]
ext1
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑(-g • z) = ↑(g • z)
[PROOFSTEP]
change _ / _ = _ / _
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (-g) z / denom (-g) z = num g z / denom g z
[PROOFSTEP]
field_simp [denom_ne_zero]
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (-g) z * denom g z = num g z * denom (-g) z
[PROOFSTEP]
simp only [num, denom, Complex.ofReal_neg, neg_mul, GLPos.coe_neg_GL, Units.val_neg, neg_apply]
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (-(↑(↑↑g 0 0) * ↑z) + -↑(↑↑g 0 1)) * (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑(↑↑g 0 0) * ↑z + ↑(↑↑g 0 1)) * (-(↑(↑↑g 1 0) * ↑z) + -↑(↑↑g 1 1))
[PROOFSTEP]
ring_nf
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
z : ℍ
⊢ -g • z = g • z
[PROOFSTEP]
simp only [coe_GLPos_neg, sl_moeb, coe_int_neg, neg_smul, coe']
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
⊢ (↑↑(↑toGLPos g) 1 0 * im z) ^ 2 ≤ ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
let c := (↑ₘg 1 0 : ℝ)
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
⊢ (↑↑(↑toGLPos g) 1 0 * im z) ^ 2 ≤ ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
let d := (↑ₘg 1 1 : ℝ)
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (↑↑(↑toGLPos g) 1 0 * im z) ^ 2 ≤ ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
calc
  (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
  _ = Complex.normSq (denom g z) := by dsimp [denom, Complex.normSq]; ring
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (c * im z) ^ 2 ≤ (c * im z) ^ 2 + (c * re z + d) ^ 2
[PROOFSTEP]
nlinarith
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (c * im z) ^ 2 + (c * re z + d) ^ 2 = ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
dsimp [denom, Complex.normSq]
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (↑g 1 0 * im z) ^ 2 + (↑g 1 0 * re z + ↑g 1 1) ^ 2 =
    (↑g 1 0 * re z - 0 * im z + ↑g 1 1) * (↑g 1 0 * re z - 0 * im z + ↑g 1 1) +
      (↑g 1 0 * im z + 0 * re z + 0) * (↑g 1 0 * im z + 0 * re z + 0)
[PROOFSTEP]
ring
[GOAL]
g : SL(2, ℤ)
z : ℍ
Γ : Subgroup SL(2, ℤ)
⊢ im (g • z) = im z / ↑Complex.normSq (denom (↑g) z)
[PROOFSTEP]
convert im_smul_eq_div_normSq g z
[GOAL]
case h.e'_3.h.e'_5
g : SL(2, ℤ)
z : ℍ
Γ : Subgroup SL(2, ℤ)
⊢ im z = det ↑↑↑g * im z
[PROOFSTEP]
simp only [GeneralLinearGroup.det_apply_val, coe_GLPos_coe_GL_coe_matrix, Int.coe_castRingHom, (g : SL(2, ℝ)).prop,
  one_mul, coe']
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
z : ℍ
⊢ denom (↑g) z = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)
[PROOFSTEP]
simp [denom, coe']
[GOAL]
x : { x // 0 < x }
z : ℍ
⊢ 0 < (↑x • ↑z).im
[PROOFSTEP]
simpa using mul_pos x.2 z.2
[GOAL]
x : ℝ
z : ℍ
⊢ 0 < (↑x + ↑z).im
[PROOFSTEP]
simpa using z.im_pos
[GOAL]
x✝ : ℍ
⊢ ↑(0 +ᵥ x✝) = ↑x✝
[PROOFSTEP]
simp [HVAdd.hVAdd]
[GOAL]
x y : ℝ
z : ℍ
⊢ ↑(x + y +ᵥ z) = ↑(x +ᵥ (y +ᵥ z))
[PROOFSTEP]
simp [HVAdd.hVAdd, add_assoc]
[GOAL]
z : ℍ
⊢ ModularGroup.S • z = mk (-↑z)⁻¹ (_ : 0 < (-↑z)⁻¹.im)
[PROOFSTEP]
rw [specialLinearGroup_apply]
[GOAL]
z : ℍ
⊢ mk
      ((↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 0 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 0 1))) /
        (↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 1 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 1 1))))
      (_ : 0 < (↑(ModularGroup.S • z)).im) =
    mk (-↑z)⁻¹ (_ : 0 < (-↑z)⁻¹.im)
[PROOFSTEP]
simp [ModularGroup.S, neg_div, inv_neg, coeToGL]
[GOAL]
z : ℍ
n : ℤ
⊢ ModularGroup.T ^ n • z = ↑n +ᵥ z
[PROOFSTEP]
rw [← ext_iff, coe_vadd, add_comm, specialLinearGroup_apply, coe_mk]
  -- Porting note: added `coeToGL` and merged `rw` and `simp`
[GOAL]
z : ℍ
n : ℤ
⊢ (↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 0 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 0 1))) /
      (↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 1 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 1 1))) =
    ↑z + ↑↑n
[PROOFSTEP]
simp [coeToGL, ModularGroup.coe_T_zpow, of_apply, cons_val_zero, algebraMap.coe_one, Complex.ofReal_one, one_mul,
  cons_val_one, head_cons, algebraMap.coe_zero, zero_mul, zero_add, div_one]
[GOAL]
z : ℍ
⊢ ModularGroup.T • z = 1 +ᵥ z
[PROOFSTEP]
simpa only [Int.cast_one] using modular_T_zpow_smul z 1
[GOAL]
g : SL(2, ℝ)
hc : ↑↑g 1 0 = 0
⊢ ∃ u v, (fun x x_1 => x • x_1) g = (fun z => v +ᵥ z) ∘ fun z => u • z
[PROOFSTEP]
obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc
[GOAL]
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
⊢ ∃ u v,
    (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } =
      (fun z => v +ᵥ z) ∘ fun z => u • z
[PROOFSTEP]
refine' ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, _⟩
[GOAL]
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } =
    (fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z
[PROOFSTEP]
ext1 ⟨z, hz⟩
[GOAL]
case intro.intro.intro.h.mk
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
      { val := z, property := hz } =
    ((fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z) { val := z, property := hz }
[PROOFSTEP]
ext1
[GOAL]
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z) { val := z, property := hz })
[PROOFSTEP]
suffices ↑a * z * a + b * a = b * a + a * a * z by
  -- Porting note: added `coeToGL` and merged `rw` and `simpa`simpa [coeToGL, specialLinearGroup_apply, add_mul]
[GOAL]
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
this : ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z) { val := z, property := hz })
[PROOFSTEP]
simpa [coeToGL, specialLinearGroup_apply, add_mul]
[GOAL]
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
[PROOFSTEP]
ring
[GOAL]
g : SL(2, ℝ)
hc : ↑↑g 1 0 ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) g =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
have h_denom := denom_ne_zero g
[GOAL]
g : SL(2, ℝ)
hc : ↑↑g 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) g =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
induction' g using Matrix.SpecialLinearGroup.fin_two_induction with a b c d h
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 ≠ 0
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
replace hc : c ≠ 0
[GOAL]
case hc
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 ≠ 0
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
⊢ c ≠ 0
[PROOFSTEP]
simpa using hc
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
refine' ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, _⟩
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
    (fun x x_1 => x +ᵥ x_1) (a / c) ∘
      (fun x x_1 => x • x_1) ModularGroup.S ∘
        (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) }
[PROOFSTEP]
ext1 ⟨z, hz⟩
[GOAL]
case h.h.mk
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
      { val := z, property := hz } =
    ((fun x x_1 => x +ᵥ x_1) (a / c) ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘
          (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) })
      { val := z, property := hz }
[PROOFSTEP]
ext1
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun x x_1 => x +ᵥ x_1) (a / c) ∘
          (fun x x_1 => x • x_1) ModularGroup.S ∘
            (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) })
        { val := z, property := hz })
[PROOFSTEP]
suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹ by
  -- Porting note: golfed broken proofsimpa only [modular_S_smul, inv_neg, Function.comp_apply, coe_vadd,
    Complex.ofReal_mul, coe_pos_real_smul, Complex.real_smul, Complex.ofReal_div, coe_mk]
[GOAL]
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
this : (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun x x_1 => x +ᵥ x_1) (a / c) ∘
          (fun x x_1 => x • x_1) ModularGroup.S ∘
            (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) })
        { val := z, property := hz })
[PROOFSTEP]
simpa only [modular_S_smul, inv_neg, Function.comp_apply, coe_vadd, Complex.ofReal_mul, coe_pos_real_smul,
  Complex.real_smul, Complex.ofReal_div, coe_mk]
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
replace hc : (c : ℂ) ≠ 0
[GOAL]
case hc
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑c ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
replace h_denom : ↑c * z + d ≠ 0
[GOAL]
case h_denom
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
⊢ ↑c * z + ↑d ≠ 0
[PROOFSTEP]
simpa using h_denom ⟨z, hz⟩
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
have h_aux : (c : ℂ) * d + ↑c * ↑c * z ≠ 0 :=
  by
  rw [mul_assoc, ← mul_add, add_comm]
  exact mul_ne_zero hc h_denom
[GOAL]
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
⊢ ↑c * ↑d + ↑c * ↑c * z ≠ 0
[PROOFSTEP]
rw [mul_assoc, ← mul_add, add_comm]
[GOAL]
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
⊢ ↑c * (↑c * z + ↑d) ≠ 0
[PROOFSTEP]
exact mul_ne_zero hc h_denom
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
replace h : (a * d - b * c : ℂ) = (1 : ℂ)
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
⊢ ↑a * ↑d - ↑b * ↑c = 1
[PROOFSTEP]
norm_cast
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
h : ↑a * ↑d - ↑b * ↑c = 1
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
field_simp
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
h : ↑a * ↑d - ↑b * ↑c = 1
⊢ (↑a * z + ↑b) * (↑c * (↑c * ↑d + ↑c * ↑c * z)) = (↑a * (↑c * ↑d + ↑c * ↑c * z) - ↑c) * (↑c * z + ↑d)
[PROOFSTEP]
linear_combination (-(z * (c : ℂ) ^ 2) - c * d) * h


[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h
[PROOFSTEP]
rw [w]


[GOAL]
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ Int.gcd x y = d
[PROOFSTEP]
refine Nat.dvd_antisymm ?_ (Int.coe_nat_dvd.1 (Int.dvd_gcd h₁ h₂))
[GOAL]
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ Int.gcd x y ∣ d
[PROOFSTEP]
rw [← Int.coe_nat_dvd, ← h₃]
[GOAL]
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(Int.gcd x y) ∣ x * a + y * b
[PROOFSTEP]
apply dvd_add
[GOAL]
case h₁
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(Int.gcd x y) ∣ x * a
[PROOFSTEP]
exact (Int.gcd_dvd_left _ _).mul_right _
[GOAL]
case h₂
d : ℕ
x y a b : ℤ
h₁ : ↑d ∣ x
h₂ : ↑d ∣ y
h₃ : x * a + y * b = ↑d
⊢ ↑(Int.gcd x y) ∣ y * b
[PROOFSTEP]
exact (Int.gcd_dvd_right _ _).mul_right _
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Nat.gcd x y = d
[PROOFSTEP]
rw [← Int.coe_nat_gcd]
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ Int.gcd ↑x ↑y = d
[PROOFSTEP]
apply
  int_gcd_helper' a (-b) (Int.coe_nat_dvd.mpr (Nat.dvd_of_mod_eq_zero hu))
    (Int.coe_nat_dvd.mpr (Nat.dvd_of_mod_eq_zero hv))
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + ↑y * -↑b = ↑d
[PROOFSTEP]
rw [mul_neg, ← sub_eq_add_neg, sub_eq_iff_eq_add']
[GOAL]
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a = ↑y * ↑b + ↑d
[PROOFSTEP]
exact_mod_cast h
[GOAL]
x y d m : ℕ
hd : Nat.gcd x y = d
d0 : Nat.beq d 0 = false
dm : x * y = d * m
⊢ (fun x x_1 => x * x_1) d (Nat.lcm x y) = (fun x x_1 => x * x_1) d m
[PROOFSTEP]
dsimp only
  -- Porting note: the `dsimp only` was not necessary in Lean3.
[GOAL]
x y d m : ℕ
hd : Nat.gcd x y = d
d0 : Nat.beq d 0 = false
dm : x * y = d * m
⊢ d * Nat.lcm x y = d * m
[PROOFSTEP]
rw [← dm, ← hd, Nat.gcd_mul_lcm]
[GOAL]
x y : ℤ
x' y' d : ℕ
hx : Int.natAbs x = x'
hy : Int.natAbs y = y'
h : Nat.gcd x' y' = d
⊢ Int.gcd x y = d
[PROOFSTEP]
subst_vars
[GOAL]
x y : ℤ
⊢ Int.gcd x y = Nat.gcd (Int.natAbs x) (Int.natAbs y)
[PROOFSTEP]
rw [Int.gcd_def]
[GOAL]
x y : ℤ
x' y' d : ℕ
hx : Int.natAbs x = x'
hy : Int.natAbs y = y'
h : Nat.lcm x' y' = d
⊢ Int.lcm x y = d
[PROOFSTEP]
subst_vars
[GOAL]
x y : ℤ
⊢ Int.lcm x y = Nat.lcm (Int.natAbs x) (Int.natAbs y)
[PROOFSTEP]
rw [Int.lcm_def]


[GOAL]
n k : ℕ
h : MinFacHelper n k
⊢ 1 < n
[PROOFSTEP]
have : 2 < minFac n := h.1.trans_le h.2.2
[GOAL]
n k : ℕ
h : MinFacHelper n k
this : 2 < minFac n
⊢ 1 < n
[PROOFSTEP]
rcases eq_zero_or_pos n with rfl | h
[GOAL]
case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0
[PROOFSTEP]
contradiction
[GOAL]
case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < minFac n
h : n > 0
⊢ 1 < n
[PROOFSTEP]
rcases(succ_le_of_lt h).eq_or_lt with rfl | h
[GOAL]
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < minFac (succ 0)
h : succ 0 > 0
⊢ 1 < succ 0
[PROOFSTEP]
contradiction
[GOAL]
case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < minFac n
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n
[PROOFSTEP]
exact h
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ MinFacHelper n 3
[PROOFSTEP]
refine ⟨by norm_num, by norm_num, ?_⟩
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 2 < 3
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 % 2 = 1
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ minFac n
[PROOFSTEP]
refine (le_minFac'.mpr λ p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p
[PROOFSTEP]
rcases hp.eq_or_lt with rfl | h
[GOAL]
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2
[PROOFSTEP]
simp [(Nat.dvd_iff_mod_eq_zero ..).1 hpn] at h2
[GOAL]
case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p
[PROOFSTEP]
exact h
[GOAL]
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ MinFacHelper n k'
[PROOFSTEP]
rw [← e]
[GOAL]
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ MinFacHelper n (k + 2)
[PROOFSTEP]
refine ⟨Nat.lt_add_right _ _ _ h.1, ?_, ?_⟩
[GOAL]
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ (k + 2) % 2 = 1
[PROOFSTEP]
rw [add_mod, mod_self, add_zero, mod_mod]
[GOAL]
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k % 2 = 1
[PROOFSTEP]
exact h.2.1
[GOAL]
case refine_2
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k + 2 ≤ minFac n
[PROOFSTEP]
rcases h.2.2.eq_or_lt with rfl | h2
[GOAL]
case refine_2.inl
n k' : ℕ
e : minFac n + 2 = k'
h : MinFacHelper n (minFac n)
np : minFac n ≠ minFac n
⊢ minFac n + 2 ≤ minFac n
[PROOFSTEP]
exact (np rfl).elim
[GOAL]
case refine_2.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2 : k < minFac n
⊢ k + 2 ≤ minFac n
[PROOFSTEP]
rcases(succ_le_of_lt h2).eq_or_lt with h2 | h2
[GOAL]
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ k + 2 ≤ minFac n
[PROOFSTEP]
refine ((h.1.trans_le h.2.2).ne ?_).elim
[GOAL]
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ 2 = minFac n
[PROOFSTEP]
have h3 : 2 ∣ minFac n
[GOAL]
case h3
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ 2 ∣ minFac n
[PROOFSTEP]
rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
[GOAL]
case h3
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ (1 + 1 % 2) % 2 = 0
[PROOFSTEP]
norm_num
[GOAL]
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 ∣ minFac n
⊢ 2 = minFac n
[PROOFSTEP]
rw [dvd_prime <| minFac_prime h.one_lt.ne'] at h3
[GOAL]
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 = 1 ∨ 2 = minFac n
⊢ 2 = minFac n
[PROOFSTEP]
norm_num at h3
[GOAL]
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 = minFac n
⊢ 2 = minFac n
[PROOFSTEP]
exact h3
[GOAL]
case refine_2.inr.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k < minFac n
⊢ k + 2 ≤ minFac n
[PROOFSTEP]
exact h2
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
⊢ MinFacHelper n k'
[PROOFSTEP]
refine minFacHelper_1 e h λ h2 ↦ ?_
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
[PROOFSTEP]
rw [← h2] at nk
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime (minFac n)
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
[PROOFSTEP]
exact nk <| minFac_prime h.one_lt.ne'
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : beq (n % k) 0 = false
h : MinFacHelper n k
⊢ MinFacHelper n k'
[PROOFSTEP]
refine minFacHelper_1 e h λ h2 ↦ ?_
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
[PROOFSTEP]
have nk := Nat.ne_of_beq_eq_false nk
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk✝ : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
nk : ¬n % k = 0
⊢ False
[PROOFSTEP]
rw [← Nat.dvd_iff_mod_eq_zero, ← h2] at nk
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk✝ : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
nk : ¬minFac n ∣ n
⊢ False
[PROOFSTEP]
exact nk <| minFac_dvd n
[GOAL]
a : ℕ
h : a % 2 = 0
⊢ minFac a = ↑2
[PROOFSTEP]
rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ IsNat (minFac n) k
[PROOFSTEP]
rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat (minFac n) k
[PROOFSTEP]
exact ⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ IsNat (minFac n) n
[PROOFSTEP]
refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ Nat.Prime n
[PROOFSTEP]
rw [Nat.prime_def_le_sqrt]
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt n → ¬m ∣ n
[PROOFSTEP]
refine ⟨h1.one_lt, λ m hm hmn h2mn ↦ ?_⟩
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ sqrt n
h2mn : m ∣ n
⊢ False
[PROOFSTEP]
exact
  lt_irrefl m <|
    calc
      m ≤ sqrt n := hmn
      _ < k := (sqrt_lt.mpr (ble_eq_false.mp h2))
      _ ≤ n.minFac := h1.2.2
      _ ≤ m := Nat.minFac_le_of_dvd hm h2mn


[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
h : f = g
x : (forget C).obj X
⊢ ↑f x = ↑g x
[PROOFSTEP]
rw [h]


[GOAL]
u : Level
α :
  let u := u;
  Q(Type u)
x✝ : Q(Semiring «$α»)
n k✝ : ℕ
lit k : Q(ℕ)
this : «$lit» =Q «$k» + 2
⊢ Q(«$α»)
[PROOFSTEP]
exact q(OfNat.ofNat $lit)


[GOAL]
a : ℕ
⊢ jacobiSymNat a 0 = 1
[PROOFSTEP]
rw [jacobiSymNat, jacobiSym.zero_right]
[GOAL]
a : ℕ
⊢ jacobiSymNat a 1 = 1
[PROOFSTEP]
rw [jacobiSymNat, jacobiSym.one_right]
[GOAL]
b : ℕ
hb : Nat.beq (b / 2) 0 = false
⊢ jacobiSymNat 0 b = 0
[PROOFSTEP]
rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]
[GOAL]
b : ℕ
hb : Nat.beq (b / 2) 0 = false
⊢ 1 < b
[PROOFSTEP]
calc
  1 < 2 * 1 := by decide
  _ ≤ 2 * (b / 2) := (Nat.mul_le_mul_of_nonneg_left (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb))))
  _ ≤ b := Nat.mul_div_le b 2
[GOAL]
b : ℕ
hb : Nat.beq (b / 2) 0 = false
⊢ 1 < 2 * 1
[PROOFSTEP]
decide
[GOAL]
b : ℕ
⊢ jacobiSymNat 1 b = 1
[PROOFSTEP]
rw [jacobiSymNat, Nat.cast_one, jacobiSym.one_left]
[GOAL]
p : ℕ
pp : Fact (Nat.Prime p)
a r : ℤ
hr : IsInt (jacobiSym a p) r
⊢ IsInt (legendreSym p a) r
[PROOFSTEP]
rwa [@jacobiSym.legendreSym.to_jacobiSym p pp a]
[GOAL]
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym a b = r
[PROOFSTEP]
rw [← hr, jacobiSymNat, jacobiSym.mod_left, hb', hab, ← h]
[GOAL]
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [← hr, jacobiSymNat, jacobiSymNat, _root_.jacobiSym.mod_left a b, ← hab]
[GOAL]
a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b
[PROOFSTEP]
rfl
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
⊢ jacobiSymNat a b = 0
[PROOFSTEP]
refine'
  jacobiSym.eq_zero_iff.mpr
    ⟨ne_of_gt ((Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb₀)).trans_le (Nat.div_le_self b 2)), fun hf => _⟩
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
⊢ False
[PROOFSTEP]
have h : 2 ∣ a.gcd b := Nat.dvd_gcd (Nat.dvd_of_mod_eq_zero ha) (Nat.dvd_of_mod_eq_zero hb₁)
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
h : 2 ∣ Nat.gcd a b
⊢ False
[PROOFSTEP]
change 2 ∣ (a : ℤ).gcd b at h
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
h : 2 ∣ Int.gcd ↑a ↑b
⊢ False
[PROOFSTEP]
rw [hf, ← even_iff_two_dvd] at h
[GOAL]
a b : ℕ
hb₀ : Nat.beq (b / 2) 0 = false
ha : a % 2 = 0
hb₁ : b % 2 = 0
hf : Int.gcd ↑a ↑b = 1
h : Even 1
⊢ False
[PROOFSTEP]
exact Nat.not_even_one h
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have ha' : legendreSym 2 a = 1 := by simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑a = 1
[PROOFSTEP]
simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc')
[GOAL]
case inl
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
ha' : legendreSym 2 ↑a = 1
hc : b / 2 = 0
hr : jacobiSymNat a 0 = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]
[GOAL]
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
⊢ jacobiSymNat a b = r
[PROOFSTEP]
haveI : NeZero c :=
  ⟨hc'⟩
    -- for `jacobiSym.mul_right`
[GOAL]
case inr
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
ha' : legendreSym 2 ↑a = 1
hc' : c ≠ 0
this : NeZero c
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right, ←
  jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have : ((2 : ℕ) : ℤ).gcd b = 1 := by
  rw [Int.coe_nat_gcd, ← Nat.mod_add_div b 2, hb, Nat.gcd_add_mul_left_right, Nat.gcd_one_right]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ Int.gcd ↑2 ↑b = 1
[PROOFSTEP]
rw [Int.coe_nat_gcd, ← Nat.mod_add_div b 2, hb, Nat.gcd_add_mul_left_right, Nat.gcd_one_right]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
this : Int.gcd ↑2 ↑b = 1
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [← Nat.mod_add_div a 4, ha, hc, Nat.zero_add, (by decide : 4 = 2 ^ 2), jacobiSymNat, Nat.cast_mul, Nat.cast_pow,
  jacobiSym.mul_left, jacobiSym.sq_one' this, one_mul]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
this : Int.gcd ↑2 ↑b = 1
⊢ 4 = 2 ^ 2
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8); rw [← Nat.mul_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 1 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8)
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 1 = 2 * (4 * (b / 8)) + 1
[PROOFSTEP]
rw [← Nat.mul_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 1 = 2 * 4 * (b / 8) + 1
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑1 * jacobiSym (↑c) b = r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8) + 3; rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 7 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8) + 3
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 7 = 2 * (4 * (b / 8) + 3) + 1
[PROOFSTEP]
rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 7 = 2 * 4 * (b / 8) + (2 * 3 + 1)
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb, (by decide : ZMod.χ₈ (7 : ℕ) = 1)]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑7 = 1
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ 1 * jacobiSym (↑c) b = r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8) + 1; rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 3 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8) + 1
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 3 = 2 * (4 * (b / 8) + 1) + 1
[PROOFSTEP]
rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 3 = 2 * 4 * (b / 8) + (2 * 1 + 1)
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb, (by decide : ZMod.χ₈ (3 : ℕ) = -1)]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑3 = -1
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ -1 * jacobiSym (↑c) b = -r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
have hb' : Odd b := by
  rw [← Nat.div_add_mod b 8, hb, Odd]
  use 4 * (b / 8) + 2; rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]; congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ Odd b
[PROOFSTEP]
rw [← Nat.div_add_mod b 8, hb, Odd]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ∃ k, 8 * (b / 8) + 5 = 2 * k + 1
[PROOFSTEP]
use 4 * (b / 8) + 2
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 5 = 2 * (4 * (b / 8) + 2) + 1
[PROOFSTEP]
rw [Nat.mul_add, ← Nat.mul_assoc, Nat.add_assoc]
[GOAL]
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 8 * (b / 8) + 5 = 2 * 4 * (b / 8) + (2 * 2 + 1)
[PROOFSTEP]
congr
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
rw [jacobiSymNat, ← Nat.mod_add_div a 2, ha, hc, Nat.zero_add, Nat.cast_mul, jacobiSym.mul_left, Nat.cast_two,
  jacobiSym.at_two hb', ZMod.χ₈_nat_mod_eight, hb, (by decide : ZMod.χ₈ (5 : ℕ) = -1)]
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ ↑ZMod.χ₈ ↑5 = -1
[PROOFSTEP]
decide
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ -1 * jacobiSym (↑c) b = -r
[PROOFSTEP]
norm_num
[GOAL]
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
hb' : Odd b
⊢ jacobiSym (↑c) b = r
[PROOFSTEP]
exact hr
[GOAL]
a b : ℕ
r : ℤ
ha : a % 4 = 1
hb : b % 2 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_one_mod_four ha (Nat.odd_iff.mpr hb)]
[GOAL]
a b : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 4 = 1
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = r
[PROOFSTEP]
rwa [jacobiSymNat, ← jacobiSym.quadratic_reciprocity_one_mod_four hb (Nat.odd_iff.mpr ha)]
[GOAL]
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSymNat a b = -r
[PROOFSTEP]
rwa [jacobiSymNat, jacobiSym.quadratic_reciprocity_three_mod_four ha hb, neg_inj]


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ⊗≫ g = f ≫ g
[PROOFSTEP]
simp [monoidalComp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
U V W X Y : C
f : U ⟶ V ⊗ W ⊗ X
g : (V ⊗ W) ⊗ X ⟶ Y
⊢ f ⊗≫ g = f ≫ (α_ V W X).inv ≫ g
[PROOFSTEP]
simp [monoidalComp]
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : MonoidalCategory C✝
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g
[PROOFSTEP]
simpa using w
[GOAL]
C✝ : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : MonoidalCategory C✝
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g ≫ 𝟙 Y
⊢ f = g
[PROOFSTEP]
simpa using w


[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ⊗≫ θ = η ≫ θ
[PROOFSTEP]
dsimp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c d e : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ≫ 𝟙 g ≫ θ = η ≫ θ
[PROOFSTEP]
simp


[GOAL]
R✝ : Type ?u.74090
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ Nat.rawCast 1 = 1
[PROOFSTEP]
simp
[GOAL]
R✝ : Type ?u.76702
inst✝¹ : CommSemiring R✝
R : Type u_1
inst✝ : Ring R
⊢ Int.rawCast (Int.negOfNat 1) = -1
[PROOFSTEP]
simp [Int.negOfNat_eq]
[GOAL]
R✝ : Type ?u.78211
inst✝² : CommSemiring R✝
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nat.AtLeastTwo n
⊢ Int.rawCast (Int.negOfNat n) = -OfNat.ofNat n
[PROOFSTEP]
simp [Int.negOfNat_eq, OfNat.ofNat]
[GOAL]
R✝ : Type ?u.80333
inst✝¹ : CommSemiring R✝
n : ℤ
d : ℕ
R : Type u_1
inst✝ : DivisionRing R
⊢ Rat.rawCast n d = ↑n / ↑d
[PROOFSTEP]
simp


[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib n' = a'
[PROOFSTEP]
rw [← hn, fib_two_mul, H.1, H.2, ← h1]
[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib (n' + 1) = b'
[PROOFSTEP]
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]
[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib n' = a'
[PROOFSTEP]
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h1]
[GOAL]
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ fib (n' + 1) = b'
[PROOFSTEP]
rw [← hn, fib_two_mul_add_two, H.1, H.2, h2]


[GOAL]
α : Type u_1
inst✝ : Ring α
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = ↑a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n : ℕ
⊢ ↑(Int.negOfNat n) = -↑n
[PROOFSTEP]
simp [Int.negOfNat_eq, Int.cast_neg]
[GOAL]
α : Type u_1
inst✝ : Ring α
a✝ : ℕ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑(Int.ofNat a✝) * ⅟↑1 = ↑a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ 1 * ↑1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝) * ⅟↑1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num✝ * ⅟↑1 = ↑num✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ 1 * ↑1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝ : ℤ
⊢ ↑n✝ = ↑n✝ * ⅟↑1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
n : ℤ
d : ℕ
inst✝ : DivisionRing α
inv : Invertible ↑d
⊢ ↑n * ⅟↑d = Rat.rawCast n d
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.negOfNat n) * ⅟↑d = -(↑n / ↑d)
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n d : ℕ
inv✝ : Invertible ↑d
⊢ ↑(Int.ofNat n) * ⅟↑d = ↑n / ↑d
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : ↑d ≠ 0
this : Invertible ↑d
⊢ Rat.rawCast n d = ↑n * ⅟↑d
[PROOFSTEP]
simp [div_eq_mul_inv]


[GOAL]
p : Prop
as ps as₁ : List Prop
⊢ as = List.reverseAux as₁ ps → implies (mk as) p ps (List.length as₁) → p
[PROOFSTEP]
induction ps generalizing as₁ with
| nil => exact fun _ ↦ id
| cons a as ih =>
  refine fun e H ↦ @ih (a :: as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
  induction as₁ with simp
  | cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
p : Prop
as ps as₁ : List Prop
⊢ as = List.reverseAux as₁ ps → implies (mk as) p ps (List.length as₁) → p
[PROOFSTEP]
induction ps generalizing as₁ with
| nil => exact fun _ ↦ id
| cons a as ih =>
  refine fun e H ↦ @ih (a :: as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
  induction as₁ with simp
  | cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case nil
p : Prop
as as₁ : List Prop
⊢ as = List.reverseAux as₁ [] → implies (mk as) p [] (List.length as₁) → p
[PROOFSTEP]

| nil => exact fun _ ↦ id
[GOAL]
case nil
p : Prop
as as₁ : List Prop
⊢ as = List.reverseAux as₁ [] → implies (mk as) p [] (List.length as₁) → p
[PROOFSTEP]
exact fun _ ↦ id
[GOAL]
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
⊢ as✝ = List.reverseAux as₁ (a :: as) → implies (mk as✝) p (a :: as) (List.length as₁) → p
[PROOFSTEP]

| cons a as ih =>
  refine fun e H ↦ @ih (a :: as₁) e (H ?_)
  subst e; clear ih H
  suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
  induction as₁ with simp
  | cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
⊢ as✝ = List.reverseAux as₁ (a :: as) → implies (mk as✝) p (a :: as) (List.length as₁) → p
[PROOFSTEP]
refine fun e H ↦ @ih (a :: as₁) e (H ?_)
[GOAL]
case cons
p : Prop
as✝ : List Prop
a : Prop
as : List Prop
ih : ∀ (as₁ : List Prop), as✝ = List.reverseAux as₁ as → implies (mk as✝) p as (List.length as₁) → p
as₁ : List Prop
e : as✝ = List.reverseAux as₁ (a :: as)
H : implies (mk as✝) p (a :: as) (List.length as₁)
⊢ mk as✝ (List.length as₁) ↔ a
[PROOFSTEP]
subst e
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
ih :
  ∀ (as₁_1 : List Prop),
    List.reverseAux as₁ (a :: as) = List.reverseAux as₁_1 as →
      implies (mk (List.reverseAux as₁ (a :: as))) p as (List.length as₁_1) → p
H : implies (mk (List.reverseAux as₁ (a :: as))) p (a :: as) (List.length as₁)
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
[PROOFSTEP]
clear ih H
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
⊢ mk (List.reverseAux as₁ (a :: as)) (List.length as₁) ↔ a
[PROOFSTEP]
suffices ∀ n n', n' = List.length as₁ + n → ∀ bs, mk (as₁.reverseAux bs) n' ↔ mk bs n from this 0 _ rfl (a :: as)
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
[PROOFSTEP]
induction as₁ with simp
| cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons
p a : Prop
as as₁ : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
[PROOFSTEP]
induction as₁ with simp
| cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
⊢ ∀ (n n' : ℕ), n' = List.length (b :: as₁) + n → ∀ (bs : List Prop), mk (List.reverseAux (b :: as₁) bs) n' ↔ mk bs n
[PROOFSTEP]
simp
[GOAL]
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
⊢ ∀ (n : ℕ) (bs : List Prop), mk (List.reverseAux as₁ (b :: bs)) (Nat.succ (List.length as₁) + n) ↔ mk bs n
[PROOFSTEP]

| cons b as₁ ih => exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons.cons
p a : Prop
as : List Prop
b : Prop
as₁ : List Prop
ih : ∀ (n n' : ℕ), n' = List.length as₁ + n → ∀ (bs : List Prop), mk (List.reverseAux as₁ bs) n' ↔ mk bs n
⊢ ∀ (n : ℕ) (bs : List Prop), mk (List.reverseAux as₁ (b :: bs)) (Nat.succ (List.length as₁) + n) ↔ mk bs n
[PROOFSTEP]
exact fun n bs ↦ ih (n + 1) _ (Nat.succ_add ..) _
[GOAL]
case cons.nil
p a : Prop
as : List Prop
⊢ ∀ (n n' : ℕ), n' = List.length [] + n → ∀ (bs : List Prop), mk (List.reverseAux [] bs) n' ↔ mk bs n
[PROOFSTEP]
simp
[GOAL]
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
⊢ reify v (and f₁ f₂) (a ∨ b)
[PROOFSTEP]
refine ⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩
[GOAL]
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
⊢ False
[PROOFSTEP]
rcases List.mem_append.1 h with h | h
[GOAL]
case inl
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₁
⊢ False
[PROOFSTEP]
exact hn $ Or.inl $ h₁.1 fun Hc ↦ hn' $ Hc.1 _ h
[GOAL]
case inr
v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
H : ¬Valuation.satisfies_fmla v (and f₁ f₂)
hn : ¬(a ∨ b)
c : Clause
h✝ : c ∈ and f₁ f₂
hn' : ¬Valuation.satisfies v c
h : c ∈ f₂
⊢ False
[PROOFSTEP]
exact hn $ Or.inr $ h₂.1 fun Hc ↦ hn' $ Hc.1 _ h


[GOAL]
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ commProb (M × M') = commProb M * commProb M'
[PROOFSTEP]
simp_rw [commProb_def, div_mul_div_comm, Nat.card_prod, Nat.cast_mul, mul_pow, ← Nat.cast_mul, ← Nat.card_prod, Commute,
  SemiconjBy, Prod.ext_iff]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // (p.fst * p.snd).fst = (p.snd * p.fst).fst ∧ (p.fst * p.snd).snd = (p.snd * p.fst).snd }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // p.fst * p.snd = p.snd * p.fst } × { p // p.fst * p.snd = p.snd * p.fst })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ Nat.card { p // (p.fst * p.snd).fst = (p.snd * p.fst).fst ∧ (p.fst * p.snd).snd = (p.snd * p.fst).snd } =
    Nat.card ({ p // p.fst * p.snd = p.snd * p.fst } × { p // p.fst * p.snd = p.snd * p.fst })
[PROOFSTEP]
exact
  Nat.card_congr
    ⟨fun x => ⟨⟨⟨x.1.1.1, x.1.2.1⟩, x.2.1⟩, ⟨⟨x.1.1.2, x.1.2.2⟩, x.2.2⟩⟩, fun x =>
      ⟨⟨⟨x.1.1.1, x.2.1.1⟩, ⟨x.1.1.2, x.2.1.2⟩⟩, ⟨x.1.2, x.2.2⟩⟩, fun x => rfl, fun x => rfl⟩
[GOAL]
M : Type u_1
inst✝² : Mul M
α : Type u_3
i : α → Type u_2
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ commProb ((a : α) → i a) = ∏ a : α, commProb (i a)
[PROOFSTEP]
simp_rw [commProb_def, Finset.prod_div_distrib, Finset.prod_pow, ← Nat.cast_prod, ← Nat.card_pi, Commute, SemiconjBy,
  Function.funext_iff]
[GOAL]
M : Type u_1
inst✝² : Mul M
α : Type u_3
i : α → Type u_2
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // ∀ (a : α), (p.fst * p.snd) a = (p.snd * p.fst) a }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ↑(Nat.card ((a : α) → { p // p.fst * p.snd = p.snd * p.fst })) / ↑(Nat.card ((a : α) → i a)) ^ 2
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
M : Type u_1
inst✝² : Mul M
α : Type u_3
i : α → Type u_2
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ Nat.card { p // ∀ (a : α), (p.fst * p.snd) a = (p.snd * p.fst) a } =
    Nat.card ((a : α) → { p // p.fst * p.snd = p.snd * p.fst })
[PROOFSTEP]
exact
  Nat.card_congr
    ⟨fun x a => ⟨⟨x.1.1 a, x.1.2 a⟩, x.2 a⟩, fun x => ⟨⟨fun a => (x a).1.1, fun a => (x a).1.2⟩, fun a => (x a).2⟩,
      fun x => rfl, fun x => rfl⟩
[GOAL]
M : Type u_1
inst✝² : Mul M
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Mul β
⊢ commProb (α → β) = commProb β ^ card α
[PROOFSTEP]
rw [commProb_pi, Finset.prod_const, Finset.card_univ]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ commProb M ≤ 1
[PROOFSTEP]
refine' div_le_one_of_le _ (sq_nonneg (Nat.card M : ℚ))
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ ↑(Nat.card { p // Commute p.fst p.snd }) ≤ ↑(Nat.card M) ^ 2
[PROOFSTEP]
rw [← Nat.cast_pow, Nat.cast_le, sq, ← Nat.card_prod]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
⊢ Nat.card { p // Commute p.fst p.snd } ≤ Nat.card (M × M)
[PROOFSTEP]
apply Finite.card_subtype_le
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
[PROOFSTEP]
haveI := Fintype.ofFinite M
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
[PROOFSTEP]
rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card ↑{x | Commute x.fst x.snd}) / ↑(card M) ^ 2 = 1 ↔ Commutative fun x x_1 => x * x_1
[PROOFSTEP]
rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod, set_fintype_card_eq_univ_iff,
  Set.eq_univ_iff_forall]
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.fst x.snd}) ↔ Commutative fun x x_1 => x * x_1
[PROOFSTEP]
exact ⟨fun h x y ↦ h (x, y), fun h x ↦ h x.1 x.2⟩
[GOAL]
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0
[PROOFSTEP]
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
[GOAL]
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
⊢ commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
[GOAL]
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
by_cases h : (Nat.card G : ℚ) = 0
[GOAL]
case pos
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
rw [h, zero_mul, div_zero, div_zero]
[GOAL]
case neg
M : Type u_1
inst✝² : Mul M
inst✝¹ : Finite M
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
[PROOFSTEP]
exact mul_div_mul_right _ _ h
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ commProb { x // x ∈ H } ≤ commProb G * ↑(index H) ^ 2
[PROOFSTEP]
rw [commProb_def, commProb_def, div_le_iff, mul_assoc, ← mul_pow, ← Nat.cast_mul, mul_comm H.index, H.card_mul_index,
  div_mul_cancel, Nat.cast_le]
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Nat.card { p // Commute p.fst p.snd } ≤ Nat.card { p // Commute p.fst p.snd }
[PROOFSTEP]
refine' Finite.card_le_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) _
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Function.Injective fun p =>
    { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }
[PROOFSTEP]
exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
p q : { p // Commute p.fst p.snd }
h :
  (fun p => { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }) p =
    (fun p => { val := (↑(↑p).fst, ↑(↑p).snd), property := (_ : ↑((↑p).fst * (↑p).snd) = ↑((↑p).snd * (↑p).fst)) }) q
⊢ p = q
[PROOFSTEP]
simpa only [Subtype.ext_iff, Prod.ext_iff] using h
[GOAL]
case h
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0
[PROOFSTEP]
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')
[GOAL]
M : Type u_1
inst✝³ : Mul M
inst✝² : Finite M
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card { x // x ∈ H }) ^ 2
[PROOFSTEP]
exact pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2
[GOAL]
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card { x // x ∈ H })
[PROOFSTEP]
rw [commProb_def', commProb_def', div_le_iff, mul_assoc, ← Nat.cast_mul, ← Subgroup.index, H.card_mul_index,
  div_mul_cancel, Nat.cast_le]
[GOAL]
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)
[PROOFSTEP]
apply Finite.card_le_of_surjective
[GOAL]
case hf
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective ?f
case f
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ ConjClasses G → ConjClasses (G ⧸ H)
[PROOFSTEP]
show Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
[GOAL]
case hf
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
[PROOFSTEP]
exact ConjClasses.map_surjective Quotient.surjective_Quotient_mk''
[GOAL]
case h
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ ↑(Nat.card G) ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'
[GOAL]
M : Type u_1
inst✝⁴ : Mul M
inst✝³ : Finite M
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : Normal H
⊢ 0 < ↑(Nat.card (G ⧸ H))
[PROOFSTEP]
exact Nat.cast_pos.mpr Finite.card_pos


[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
ha : IsLeast {g | g ∈ H ∧ 0 < g} a
⊢ H = closure {a}
[PROOFSTEP]
obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
⊢ H = closure {a}
[PROOFSTEP]
refine' le_antisymm _ (H.closure_le.mpr <| by simp [a_in])
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
⊢ {a} ⊆ ↑H
[PROOFSTEP]
simp [a_in]
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
⊢ H ≤ closure {a}
[PROOFSTEP]
intro g g_in
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
⊢ g ∈ closure {a}
[PROOFSTEP]
obtain ⟨k, ⟨nonneg, lt⟩, _⟩ := existsUnique_zsmul_near_of_pos' a_pos g
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
⊢ g ∈ closure {a}
[PROOFSTEP]
have h_zero : g - k • a = 0 := by
  by_contra h
  have h : a ≤ g - k • a := by
    refine' a_min ⟨_, _⟩
    · exact AddSubgroup.sub_mem H g_in (AddSubgroup.zsmul_mem H a_in k)
    · exact lt_of_le_of_ne nonneg (Ne.symm h)
  have h' : ¬a ≤ g - k • a := not_le.mpr lt
  contradiction
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
⊢ g - k • a = 0
[PROOFSTEP]
by_contra h
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
h : ¬g - k • a = 0
⊢ False
[PROOFSTEP]
have h : a ≤ g - k • a := by
  refine' a_min ⟨_, _⟩
  · exact AddSubgroup.sub_mem H g_in (AddSubgroup.zsmul_mem H a_in k)
  · exact lt_of_le_of_ne nonneg (Ne.symm h)
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
h : ¬g - k • a = 0
⊢ a ≤ g - k • a
[PROOFSTEP]
refine' a_min ⟨_, _⟩
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
h : ¬g - k • a = 0
⊢ g - k • a ∈ H
[PROOFSTEP]
exact AddSubgroup.sub_mem H g_in (AddSubgroup.zsmul_mem H a_in k)
[GOAL]
case refine'_2
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
h : ¬g - k • a = 0
⊢ 0 < g - k • a
[PROOFSTEP]
exact lt_of_le_of_ne nonneg (Ne.symm h)
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
h✝ : ¬g - k • a = 0
h : a ≤ g - k • a
⊢ False
[PROOFSTEP]
have h' : ¬a ≤ g - k • a := not_le.mpr lt
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
h✝ : ¬g - k • a = 0
h : a ≤ g - k • a
h' : ¬a ≤ g - k • a
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 0 < g}
a_in : a ∈ H
a_pos : 0 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k => 0 ≤ g - k • a ∧ g - k • a < a) y → y = k
nonneg : 0 ≤ g - k • a
lt : g - k • a < a
h_zero : g - k • a = 0
⊢ g ∈ closure {a}
[PROOFSTEP]
simp [sub_eq_zero.mp h_zero, AddSubgroup.mem_closure_singleton]
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
[PROOFSTEP]
have hex : ∀ g > 0, ∃ n : ℕ, g ∈ Ioc (n • a) ((n + 1) • a) := fun g hg =>
  by
  rcases existsUnique_add_zsmul_mem_Ico h₀ 0 (g - a) with ⟨m, ⟨hm, hm'⟩, -⟩
  simp only [zero_add, sub_le_iff_le_add, sub_add_cancel, ← add_one_zsmul] at hm hm'
  lift m to ℕ
  · rw [← Int.lt_add_one_iff, ← zsmul_lt_zsmul_iff h₀, zero_zsmul]
    exact hg.trans_le hm
  · simp only [← Nat.cast_succ, coe_nat_zsmul] at hm hm'
    exact ⟨m, hm', hm⟩
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
[PROOFSTEP]
rcases existsUnique_add_zsmul_mem_Ico h₀ 0 (g - a) with ⟨m, ⟨hm, hm'⟩, -⟩
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g - a ≤ 0 + m • a
hm' : 0 + m • a < g - a + a
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
[PROOFSTEP]
simp only [zero_add, sub_le_iff_le_add, sub_add_cancel, ← add_one_zsmul] at hm hm'
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
[PROOFSTEP]
lift m to ℕ
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ 0 ≤ m
[PROOFSTEP]
rw [← Int.lt_add_one_iff, ← zsmul_lt_zsmul_iff h₀, zero_zsmul]
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℤ
hm : g ≤ (m + 1) • a
hm' : m • a < g
⊢ 0 < (m + 1) • a
[PROOFSTEP]
exact hg.trans_le hm
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℕ
hm : g ≤ (↑m + 1) • a
hm' : ↑m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
[PROOFSTEP]
simp only [← Nat.cast_succ, coe_nat_zsmul] at hm hm'
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
g : G
hg : g > 0
m : ℕ
hm : g ≤ Nat.succ m • a
hm' : m • a < g
⊢ ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
[PROOFSTEP]
exact ⟨m, hm', hm⟩
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
[PROOFSTEP]
have : ∃ n : ℕ, Set.Nonempty (H ∩ Ioc (n • a) ((n + 1) • a))
[GOAL]
case this
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
[PROOFSTEP]
rcases(bot_or_exists_ne_zero H).resolve_left hbot with ⟨g, hgH, hg₀⟩
[GOAL]
case this.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
g : G
hgH : g ∈ H
hg₀ : g ≠ 0
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
[PROOFSTEP]
rcases hex |g| (abs_pos.2 hg₀) with ⟨n, hn⟩
[GOAL]
case this.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
g : G
hgH : g ∈ H
hg₀ : g ≠ 0
n : ℕ
hn : |g| ∈ Ioc (n • a) ((n + 1) • a)
⊢ ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
[PROOFSTEP]
exact ⟨n, _, (@abs_mem_iff (AddSubgroup G) G _ _).2 hgH, hn⟩
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
[PROOFSTEP]
classical rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
[PROOFSTEP]
rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩
[GOAL]
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
[PROOFSTEP]
by_contra hxmin
[GOAL]
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ¬∃ b, IsLeast {g | g ∈ H ∧ 0 < g} b
⊢ False
[PROOFSTEP]
simp only [IsLeast, not_and, mem_setOf_eq, mem_lowerBounds, not_exists, not_forall, not_le] at hxmin
[GOAL]
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
⊢ False
[PROOFSTEP]
rcases hxmin x ⟨hxH, (nsmul_nonneg h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
⊢ False
[PROOFSTEP]
rcases hex y hy₀ with ⟨m, hm⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
⊢ False
[PROOFSTEP]
cases' lt_or_le m n with hmn hnm
[GOAL]
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inl
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hmn : m < n
⊢ False
[PROOFSTEP]
exact hmin m hmn ⟨y, hyH, hm⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hnm : n ≤ m
⊢ False
[PROOFSTEP]
refine disjoint_left.1 hd (sub_mem hxH hyH) ⟨sub_pos.2 hxy, sub_lt_iff_lt_add'.2 ?_⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
hbot : H ≠ ⊥
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hex : ∀ (g : G), g > 0 → ∃ n, g ∈ Ioc (n • a) ((n + 1) • a)
this : ∃ n, Set.Nonempty (↑H ∩ Ioc (n • a) ((n + 1) • a))
n : ℕ
hmin : ∀ (m : ℕ), m < n → ¬Set.Nonempty (↑H ∩ Ioc (m • a) ((m + 1) • a))
x : G
hxH : x ∈ ↑H
hnx : n • a < x
hxn : x ≤ (n + 1) • a
hxmin : ∀ (x : G), x ∈ H ∧ 0 < x → ∃ x_1 h, x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 0 < y
m : ℕ
hm : y ∈ Ioc (m • a) ((m + 1) • a)
hnm : n ≤ m
⊢ x < y + a
[PROOFSTEP]
calc
  x ≤ (n + 1) • a := hxn
  _ ≤ (m + 1) • a := (nsmul_le_nsmul h₀.le (add_le_add_right hnm _))
  _ = m • a + a := (succ_nsmul' _ _)
  _ < y + a := add_lt_add_right hm.1 _
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
⊢ ∃ b, H = closure {b}
[PROOFSTEP]
rcases eq_or_ne H ⊥ with rfl | hbot
[GOAL]
case inl
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
a : G
h₀ : 0 < a
hd : Disjoint (↑⊥) (Ioo 0 a)
⊢ ∃ b, ⊥ = closure {b}
[PROOFSTEP]
exact ⟨0, closure_singleton_zero.symm⟩
[GOAL]
case inr
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup G
a : G
h₀ : 0 < a
hd : Disjoint (↑H) (Ioo 0 a)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}
[PROOFSTEP]
exact (exists_isLeast_pos hbot h₀ hd).imp fun _ => cyclic_of_min
[GOAL]
G : Type u_1
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
H : AddSubgroup ℤ
this : Ioo 0 1 = ∅
⊢ Disjoint (↑H) (Ioo 0 1)
[PROOFSTEP]
simp [this]