[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f (1 + x) = 1 + ↑f x
[PROOFSTEP]
rw [add_comm, map_add_one, add_comm 1]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ OrderHom.toFun (OrderHom.comp f.toOrderHom g.toOrderHom) (x + 1) =
    OrderHom.toFun (OrderHom.comp f.toOrderHom g.toOrderHom) x + 1
[PROOFSTEP]
simp [map_add_one]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
x : ℝ
⊢ ↑↑f⁻¹ (↑↑f x) = x
[PROOFSTEP]
simp only [← mul_apply, f.inv_mul, coe_one, id]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
x : ℝ
⊢ ↑↑f (↑↑f⁻¹ x) = x
[PROOFSTEP]
simp only [← mul_apply, f.mul_inv, coe_one, id]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
a✝ b✝ : ℝ
h :
  ↑{ toFun := ↑↑f, invFun := ↑↑f⁻¹, left_inv := (_ : ∀ (x : ℝ), ↑↑f⁻¹ (↑↑f x) = x),
          right_inv := (_ : ∀ (x : ℝ), ↑↑f (↑↑f⁻¹ x) = x) }
      a✝ ≤
    ↑{ toFun := ↑↑f, invFun := ↑↑f⁻¹, left_inv := (_ : ∀ (x : ℝ), ↑↑f⁻¹ (↑↑f x) = x),
          right_inv := (_ : ∀ (x : ℝ), ↑↑f (↑↑f⁻¹ x) = x) }
      b✝
⊢ a✝ ≤ b✝
[PROOFSTEP]
simpa using mono (↑f⁻¹) h
[GOAL]
f✝ g f : CircleDeg1Lift
h : Bijective ↑f
x y : ℝ
hxy : x ≤ y
⊢ ↑f (↑(Equiv.ofBijective (↑f) h).symm x) ≤ ↑f (↑(Equiv.ofBijective (↑f) h).symm y)
[PROOFSTEP]
simp only [Equiv.ofBijective_apply_symm_apply f h, hxy]
[GOAL]
f✝ g f : CircleDeg1Lift
h : Bijective ↑f
x : ℝ
⊢ ↑f
      (OrderHom.toFun
        { toFun := ↑(Equiv.ofBijective (↑f) h).symm,
          monotone' :=
            (_ : ∀ (x y : ℝ), x ≤ y → ↑(Equiv.ofBijective (↑f) h).symm x ≤ ↑(Equiv.ofBijective (↑f) h).symm y) }
        (x + 1)) =
    ↑f
      (OrderHom.toFun
          { toFun := ↑(Equiv.ofBijective (↑f) h).symm,
            monotone' :=
              (_ : ∀ (x y : ℝ), x ≤ y → ↑(Equiv.ofBijective (↑f) h).symm x ≤ ↑(Equiv.ofBijective (↑f) h).symm y) }
          x +
        1)
[PROOFSTEP]
simp only [Equiv.ofBijective_apply_symm_apply f, f.map_add_one]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ ↑(f ^ (n + 1)) = (↑f)^[n + 1]
[PROOFSTEP]
ext x
[GOAL]
case h
f g : CircleDeg1Lift
n : ℕ
x : ℝ
⊢ ↑(f ^ (n + 1)) x = (↑f)^[n + 1] x
[PROOFSTEP]
simp [coe_pow n, pow_succ']
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℤ
⊢ ↑translate (↑Multiplicative.ofAdd x) ^ n = ↑translate (↑Multiplicative.ofAdd (↑n * x))
[PROOFSTEP]
simp only [← zsmul_eq_mul, ofAdd_zsmul, MonoidHom.map_zpow]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ (↑↑(↑translate (↑Multiplicative.ofAdd x)))^[n] = ↑↑(↑translate (↑Multiplicative.ofAdd (↑n * x)))
[PROOFSTEP]
rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => ↑n + x
[PROOFSTEP]
simpa only [nsmul_one, add_left_iterate] using Function.Commute.iterate_right f.map_one_add n
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => x + ↑n
[PROOFSTEP]
simp only [add_comm _ (n : ℝ), f.commute_nat_add n]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => x - ↑n
[PROOFSTEP]
simpa only [sub_eq_add_neg] using
  (f.commute_add_nat n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => x + ↑-[n+1]
[PROOFSTEP]
simpa [sub_eq_add_neg] using f.commute_sub_nat (n + 1)
[GOAL]
f g : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ↑f fun x => ↑n + x
[PROOFSTEP]
simpa only [add_comm _ (n : ℝ)] using f.commute_add_int n
[GOAL]
f g : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ↑f fun x => x - ↑n
[PROOFSTEP]
simpa only [sub_eq_add_neg] using
  (f.commute_add_int n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv
[GOAL]
f g : CircleDeg1Lift
n : ℤ
⊢ ↑f ↑n = ↑f 0 + ↑n
[PROOFSTEP]
rw [← f.map_add_int, zero_add]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f (fract x) - fract x = ↑f x - x
[PROOFSTEP]
rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ OrderHom.toFun
      { toFun := fun x => max (↑f x) (↑g x),
        monotone' := (_ : ∀ (x y : ℝ), x ≤ y → max (↑f x) (↑g x) ≤ max (↑f y) (↑g y)) }
      (x + 1) =
    OrderHom.toFun
        { toFun := fun x => max (↑f x) (↑g x),
          monotone' := (_ : ∀ (x y : ℝ), x ≤ y → max (↑f x) (↑g x) ≤ max (↑f y) (↑g y)) }
        x +
      1
[PROOFSTEP]
simp [max_add_add_right]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ OrderHom.toFun
      { toFun := fun x => min (↑f x) (↑g x),
        monotone' := (_ : ∀ (x y : ℝ), x ≤ y → min (↑f x) (↑g x) ≤ min (↑f y) (↑g y)) }
      (x + 1) =
    OrderHom.toFun
        { toFun := fun x => min (↑f x) (↑g x),
          monotone' := (_ : ∀ (x y : ℝ), x ≤ y → min (↑f x) (↑g x) ≤ min (↑f y) (↑g y)) }
        x +
      1
[PROOFSTEP]
simp [min_add_add_right]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
x : ℝ
⊢ ↑(f ^ n) x ≤ ↑(g ^ n) x
[PROOFSTEP]
simp only [coe_pow, iterate_mono h n x]
[GOAL]
f g : CircleDeg1Lift
⊢ dist (↑f 0 + ↑g 0) (↑f (↑g 0)) < 1
[PROOFSTEP]
rw [dist_comm, Real.dist_eq, abs_lt, lt_sub_iff_add_lt', sub_lt_iff_lt_add', ← sub_eq_add_neg]
[GOAL]
f g : CircleDeg1Lift
⊢ ↑f 0 + ↑g 0 - 1 < ↑f (↑g 0) ∧ ↑f (↑g 0) < ↑f 0 + ↑g 0 + 1
[PROOFSTEP]
exact ⟨f.lt_map_map_zero g, f.map_map_zero_lt g⟩
[GOAL]
f✝ g f g₁ g₂ : CircleDeg1Lift
h : Semiconj ↑f ↑g₁ ↑g₂
⊢ dist (↑g₁ 0) (↑f (↑g₁ 0) - ↑f 0) + dist (↑f (↑g₁ 0) - ↑f 0) (↑g₂ 0) =
    dist (↑f 0 + ↑g₁ 0) (↑f (↑g₁ 0)) + dist (↑g₂ 0 + ↑f 0) (↑g₂ (↑f 0))
[PROOFSTEP]
simp only [h.eq, Real.dist_eq, sub_sub, add_comm (f 0), sub_sub_eq_add_sub, abs_sub_comm (g₂ (f 0))]
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun x => x - 1) atTop atTop
[PROOFSTEP]
simpa [sub_eq_add_neg] using tendsto_atTop_add_const_right _ _ tendsto_id
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : ↑f x ≤ x + ↑m
n : ℕ
⊢ (↑f)^[n] x ≤ x + ↑n * ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_le_of_map_le f.monotone (monotone_id.add_const (m : ℝ)) h n
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ ↑f x
n : ℕ
⊢ x + ↑n * ↑m ≤ (↑f)^[n] x
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).symm.iterate_le_of_map_le (monotone_id.add_const (m : ℝ)) f.monotone h n
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : ↑f x = x + ↑m
n : ℕ
⊢ (↑f)^[n] x = x + ↑n * ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using (f.commute_add_int m).iterate_eq_of_map_eq n h
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (↑f)^[n] x ≤ x + ↑n * ↑m ↔ ↑f x ≤ x + ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_le_iff_map_le f.monotone (strictMono_id.add_const (m : ℝ)) hn
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (↑f)^[n] x < x + ↑n * ↑m ↔ ↑f x < x + ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_lt_iff_map_lt f.monotone (strictMono_id.add_const (m : ℝ)) hn
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (↑f)^[n] x = x + ↑n * ↑m ↔ ↑f x = x + ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_eq_iff_map_eq f.monotone (strictMono_id.add_const (m : ℝ)) hn
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m ≤ (↑f)^[n] x ↔ x + ↑m ≤ ↑f x
[PROOFSTEP]
simpa only [not_lt] using not_congr (f.iterate_pos_lt_iff hn)
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m < (↑f)^[n] x ↔ x + ↑m < ↑f x
[PROOFSTEP]
simpa only [not_le] using not_congr (f.iterate_pos_le_iff hn)
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ ↑n * ⌊↑f 0⌋ ≤ ⌊(↑f)^[n] 0⌋
[PROOFSTEP]
rw [le_floor, Int.cast_mul, Int.cast_ofNat, ← zero_add ((n : ℝ) * _)]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑n * ↑⌊↑f 0⌋ ≤ (↑f)^[n] 0
[PROOFSTEP]
apply le_iterate_of_add_int_le_map
[GOAL]
case h
f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑⌊↑f 0⌋ ≤ ↑f 0
[PROOFSTEP]
simp [floor_le]
[GOAL]
f g : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n => (↑f)^[n] 0 / ↑n) atTop (𝓝 τ')
⊢ Tendsto (transnumAuxSeq f) atTop (𝓝 τ')
[PROOFSTEP]
simpa [(· ∘ ·), transnumAuxSeq_def, coe_pow] using h.comp (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two)
[GOAL]
f g : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n => (↑f)^[n + 1] 0 / (↑n + 1)) atTop (𝓝 τ')
⊢ Tendsto (fun n => (↑f)^[n + 1] 0 / ↑(n + 1)) atTop (𝓝 τ')
[PROOFSTEP]
exact_mod_cast h
[GOAL]
f g : CircleDeg1Lift
⊢ transnumAuxSeq f 0 = ↑f 0
[PROOFSTEP]
simp [transnumAuxSeq]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n
[PROOFSTEP]
have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n
[PROOFSTEP]
rw [div_div, ← pow_succ, ← abs_of_pos this]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / |2 ^ (n + 1)|
[PROOFSTEP]
replace := abs_pos.2 (ne_of_gt this)
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < |2 ^ (n + 1)|
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / |2 ^ (n + 1)|
[PROOFSTEP]
convert (div_lt_div_right this).2 ((f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)) using 1
[GOAL]
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < |2 ^ (n + 1)|
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) =
    dist (↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0) (↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)) / |2 ^ (n + 1)|
[PROOFSTEP]
simp_rw [transnumAuxSeq, Real.dist_eq]
[GOAL]
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < |2 ^ (n + 1)|
⊢ |↑(f ^ 2 ^ n) 0 / 2 ^ n - ↑(f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)| =
    |↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0 - ↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)| / |2 ^ (n + 1)|
[PROOFSTEP]
rw [← abs_div, sub_div, pow_succ', pow_succ, ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ), pow_mul, sq, mul_apply]
[GOAL]
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => x (2 ^ n) / 2 ^ n) atTop (𝓝 (τ f))
[PROOFSTEP]
refine' f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)
[GOAL]
case refine'_1
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ℕ → ℝ
[PROOFSTEP]
exact fun n => C / 2 ^ n
[GOAL]
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (transnumAuxSeq f t) (x (2 ^ t) / 2 ^ t) ≤ C / 2 ^ t
[PROOFSTEP]
intro n
[GOAL]
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
[PROOFSTEP]
have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _
[GOAL]
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
[PROOFSTEP]
convert (div_le_div_right this).2 (H (2 ^ n)) using 1
[GOAL]
case h.e'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) = dist (↑(f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n
[PROOFSTEP]
rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
[GOAL]
case refine'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => C / 2 ^ n) atTop (𝓝 0)
[PROOFSTEP]
exact mul_zero C ▸ tendsto_const_nhds.mul <| tendsto_inv_atTop_zero.comp <| tendsto_pow_atTop_atTop_of_one_lt one_lt_two
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun n => (↑1)^[n] 0 / ↑n) atTop (𝓝 0)
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g
[PROOFSTEP]
refine tendsto_nhds_unique ?_ (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => transnumAuxSeq f x + transnumAuxSeq g x) atTop (𝓝 (τ (f * g)))
[PROOFSTEP]
simp only [transnumAuxSeq, ← add_div]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => (↑(f ^ 2 ^ x) 0 + ↑(g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))
[PROOFSTEP]
refine (f * g).tendsto_translationNumber_of_dist_bounded_aux (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (↑((f * g) ^ n) 0) ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) ≤ 1
[PROOFSTEP]
rw [h.mul_pow, dist_comm]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) (↑(f ^ n * g ^ n) 0) ≤ 1
[PROOFSTEP]
exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
⊢ τ ↑f⁻¹ + τ ↑f = 0
[PROOFSTEP]
simp [← translationNumber_mul_of_commute (Commute.refl _).units_inv_left]
[GOAL]
f g : CircleDeg1Lift
⊢ τ (f ^ 0) = ↑0 * τ f
[PROOFSTEP]
simp
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ (n + 1)) = ↑(n + 1) * τ f
[PROOFSTEP]
rw [pow_succ', translationNumber_mul_of_commute (Commute.pow_self f n), translationNumber_pow n, Nat.cast_add_one,
  add_mul, one_mul]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ ↑n) = ↑↑n * τ ↑f
[PROOFSTEP]
simp [translationNumber_pow f n]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ -[n+1]) = ↑-[n+1] * τ ↑f
[PROOFSTEP]
simp
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
n : ℕ
⊢ -((↑n + 1) * τ ↑f) = (-1 + -↑n) * τ ↑f
[PROOFSTEP]
ring
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun n => ↑(f ^ (n + 1)) 0 / (↑n + 1)) atTop (𝓝 (τ f))
[PROOFSTEP]
refine'
  tendsto_iff_dist_tendsto_zero.2 <|
    squeeze_zero (fun _ => dist_nonneg) (fun n => _)
      ((tendsto_const_div_atTop_nhds_0_nat 1).comp (tendsto_add_atTop_nat 1))
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ ((fun n => 1 / ↑n) ∘ fun a => a + 1) n
[PROOFSTEP]
dsimp
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
[PROOFSTEP]
have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
[PROOFSTEP]
rw [Real.dist_eq, div_sub' _ _ _ (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this, Nat.cast_add_one,
  div_le_div_right this, ← Nat.cast_add_one]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1
[PROOFSTEP]
apply dist_pow_map_zero_mul_translationNumber_le
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun n => ↑(f ^ (n + 1)) 0 / ↑(n + 1)) atTop (𝓝 (τ f))
[PROOFSTEP]
exact_mod_cast f.tendsto_translation_number₀'
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ n) x - x) / ↑n) atTop (𝓝 (τ f))
[PROOFSTEP]
rw [← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x)))))
[PROOFSTEP]
refine (tendsto_translation_number₀ _).congr fun n ↦ ?_
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ ↑((↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x))) ^ n) 0 / ↑n =
    (↑(f ^ n) x - x) / ↑n
[PROOFSTEP]
simp [sub_eq_neg_add, Units.conj_pow']
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ (n + 1)) x - x) / (↑n + 1)) atTop (𝓝 (τ f))
[PROOFSTEP]
exact_mod_cast (tendsto_add_atTop_iff_nat 1).2 (f.tendsto_translationNumber x)
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑↑(↑translate (↑Multiplicative.ofAdd x)))^[n + 1] 0 / (↑n + 1)) atTop (𝓝 x)
[PROOFSTEP]
simp only [translate_iterate, translate_apply, add_zero, Nat.cast_succ,
  mul_div_cancel_left (G₀ := ℝ) _ (Nat.cast_add_one_ne_zero _), tendsto_const_nhds]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ ↑f x
n : ℕ
⊢ x + ↑m * (↑n + 1) ≤ ↑(f ^ (n + 1)) x
[PROOFSTEP]
simp only [coe_pow, mul_comm (m : ℝ), ← Nat.cast_add_one, f.le_iterate_of_add_int_le_map h]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + ↑⌊τ f⌋ + 1
[PROOFSTEP]
rw [add_assoc]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + (↑⌊τ f⌋ + 1)
[PROOFSTEP]
norm_cast
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + ↑(⌊τ f⌋ + 1)
[PROOFSTEP]
refine' map_lt_of_translationNumber_lt_int _ _ _
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑(⌊τ f⌋ + 1)
[PROOFSTEP]
push_cast
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑⌊τ f⌋ + 1
[PROOFSTEP]
exact lt_floor_add_one _
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ x + ↑⌊τ f⌋ + 1 ≤ x + τ f + 1
[PROOFSTEP]
gcongr
[GOAL]
case bc.bc
f g : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f
[PROOFSTEP]
apply floor_le
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
⊢ τ f = ↑m / ↑n
[PROOFSTEP]
have := (f ^ n).translationNumber_of_eq_add_int h
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n
[PROOFSTEP]
rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ f * ↑n = ↑m
⊢ ↑n ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.2 (ne_of_gt hn)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
⊢ τ f < z
[PROOFSTEP]
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f y - y ≤ f x - x :=
  isCompact_Icc.exists_forall_ge (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f < z
[PROOFSTEP]
refine' lt_of_le_of_lt _ (sub_lt_iff_lt_add'.2 <| hz x)
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f ≤ ↑f x - x
[PROOFSTEP]
apply translationNumber_le_of_le_add
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 ≤ x_1 + (↑f x - x)
[PROOFSTEP]
simp only [← sub_le_iff_le_add']
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 - x_1 ≤ ↑f x - x
[PROOFSTEP]
exact f.forall_map_sub_of_Icc (fun a => a ≤ f x - x) hx
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
⊢ z < τ f
[PROOFSTEP]
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
⊢ ∃ x, x ∈ Icc 0 1 ∧ ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
[PROOFSTEP]
exact isCompact_Icc.exists_forall_le (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
[PROOFSTEP]
refine' lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) _
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ↑f x - x ≤ τ f
[PROOFSTEP]
apply le_translationNumber_of_add_le
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), x_1 + (↑f x - x) ≤ ↑f x_1
[PROOFSTEP]
simp only [← le_sub_iff_add_le']
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), ↑f x - x ≤ ↑f x_1 - x_1
[PROOFSTEP]
exact f.forall_map_sub_of_Icc _ hx
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by
  by_contra' H
  exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
⊢ ∃ x, ↑f x ≤ x + τ f
[PROOFSTEP]
by_contra' H
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
H : ∀ (x : ℝ), x + τ f < ↑f x
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
[GOAL]
case intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by
  by_contra' H
  exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
⊢ ∃ x, x + τ f ≤ ↑f x
[PROOFSTEP]
by_contra' H
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
H : ∀ (x : ℝ), ↑f x < x + τ f
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ ↑f b
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
exact intermediate_value_univ₂ hf (continuous_id.add continuous_const) ha hb
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ τ f = ↑m ↔ ∃ x, ↑f x = x + ↑m
[PROOFSTEP]
constructor
[GOAL]
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ τ f = ↑m → ∃ x, ↑f x = x + ↑m
[PROOFSTEP]
intro h
[GOAL]
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + ↑m
[PROOFSTEP]
simp only [← h]
[GOAL]
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
exact f.exists_eq_add_translationNumber hf
[GOAL]
case mpr
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ (∃ x, ↑f x = x + ↑m) → τ f = ↑m
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mpr.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
x : ℝ
hx : ↑f x = x + ↑m
⊢ τ f = ↑m
[PROOFSTEP]
exact f.translationNumber_of_eq_add_int hx
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
n : ℕ
⊢ Continuous ↑(f ^ n)
[PROOFSTEP]
rw [coe_pow]
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
n : ℕ
⊢ Continuous (↑f)^[n]
[PROOFSTEP]
exact hf.iterate n
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
rw [eq_div_iff, mul_comm, ← translationNumber_pow]
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
skip
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact ne_of_gt (Nat.cast_pos.2 hn)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
have : ∀ x, BddAbove (range fun g => f₂ g⁻¹ (f₁ g x)) :=
  by
  refine' fun x => ⟨x + 2, _⟩
  rintro _ ⟨g, rfl⟩
  have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
    rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv, MonoidHom.coe_toHomUnits]
  calc
    f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) := mono _ (map_lt_add_translationNumber_add_one _ _).le
    _ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
    _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := (add_le_add_right (map_lt_add_translationNumber_add_one _ _).le _)
    _ = x + 2 := by
      simp [this, add_assoc, one_add_one_eq_two]
        -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
          -- to `ℝ ≃o ℝ`.
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
⊢ ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
[PROOFSTEP]
refine' fun x => ⟨x + 2, _⟩
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
⊢ x + 2 ∈ upperBounds (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
[PROOFSTEP]
rintro _ ⟨g, rfl⟩
[GOAL]
case intro
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
⊢ (fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x)) g ≤ x + 2
[PROOFSTEP]
have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
  rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv, MonoidHom.coe_toHomUnits]
[GOAL]
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
⊢ τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
[PROOFSTEP]
rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv, MonoidHom.coe_toHomUnits]
[GOAL]
case intro
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
this : τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
⊢ (fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x)) g ≤ x + 2
[PROOFSTEP]
calc
  f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) := mono _ (map_lt_add_translationNumber_add_one _ _).le
  _ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
  _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := (add_le_add_right (map_lt_add_translationNumber_add_one _ _).le _)
  _ = x + 2 := by
    simp [this, add_assoc, one_add_one_eq_two]
      -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
        -- to `ℝ ≃o ℝ`.
[GOAL]
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
this : τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
⊢ ↑(↑f₂ g⁻¹) (x + τ (↑f₁ g) + 1) = ↑(↑f₂ g⁻¹) (x + τ (↑f₂ g)) + 1
[PROOFSTEP]
rw [h, map_add_one]
[GOAL]
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
this : τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
⊢ x + τ (↑f₂ g) + τ (↑f₂ g⁻¹) + 1 + 1 = x + 2
[PROOFSTEP]
simp [this, add_assoc, one_add_one_eq_two]
  -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
    -- to `ℝ ≃o ℝ`.
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
set F₁ := toOrderIso.comp f₁.toHomUnits
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
set F₂ := toOrderIso.comp f₂.toHomUnits
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
have hF₁ : ∀ g, ⇑(F₁ g) = f₁ g := fun _ => rfl
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
have hF₂ : ∀ g, ⇑(F₂ g) = f₂ g := fun _ => rfl
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
refine' ⟨⟨⟨_, fun x y hxy => _⟩, fun x => _⟩, csSup_div_semiconj F₂ F₁ fun x => _⟩
[GOAL]
case refine'_1
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x y : ℝ
hxy : x ≤ y
⊢ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)) ≤ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') y))
[PROOFSTEP]
simp only [hF₁, hF₂, ← map_inv, coe_mk]
[GOAL]
case refine'_2
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ OrderHom.toFun
      { toFun := fun x => sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)),
        monotone' :=
          (_ :
            ∀ (x y : ℝ),
              x ≤ y →
                sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)) ≤ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') y))) }
      (x + 1) =
    OrderHom.toFun
        { toFun := fun x => sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)),
          monotone' :=
            (_ :
              ∀ (x y : ℝ),
                x ≤ y →
                  sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)) ≤ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') y))) }
        x +
      1
[PROOFSTEP]
simp only [hF₁, hF₂, ← map_inv, coe_mk]
[GOAL]
case refine'_3
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ BddAbove (range fun g => ↑(↑F₂ g)⁻¹ (↑(↑F₁ g) x))
[PROOFSTEP]
simp only [hF₁, hF₂, ← map_inv, coe_mk]
[GOAL]
case refine'_1
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x y : ℝ
hxy : x ≤ y
⊢ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x)) ≤ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') y))
[PROOFSTEP]
exact ciSup_mono (this y) fun g => mono _ (mono _ hxy)
[GOAL]
case refine'_2
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') (x + 1))) = sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x)) + 1
[PROOFSTEP]
simp only [map_add_one]
[GOAL]
case refine'_2
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x) + 1) = sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x)) + 1
[PROOFSTEP]
exact
  (Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) (monotone_id.add_const (1 : ℝ))
      (this x)).symm
[GOAL]
case refine'_3
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
[PROOFSTEP]
exact this x
[GOAL]
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
n : Multiplicative ℤ
⊢ τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) n) =
    τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) n)
[PROOFSTEP]
simp [h]
[GOAL]
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
this :
  ∀ (n : Multiplicative ℤ),
    τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) n) =
      τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj ↑F ↑(↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) g)
      ↑(↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) g)
⊢ Semiconj ↑F ↑↑f₁ ↑↑f₂
[PROOFSTEP]
simpa using hF (Multiplicative.ofAdd 1)
[GOAL]
f g f₁ f₂ : CircleDeg1Lift
h₁ : IsUnit f₁
h₂ : IsUnit f₂
h : τ f₁ = τ f₂
⊢ ∃ F, Semiconj ↑F ↑f₁ ↑f₂
[PROOFSTEP]
rcases h₁, h₂ with ⟨⟨f₁, rfl⟩, ⟨f₂, rfl⟩⟩
[GOAL]
case intro.intro
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
⊢ ∃ F, Semiconj ↑F ↑↑f₁ ↑↑f₂
[PROOFSTEP]
exact units_semiconj_of_translationNumber_eq h


[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n m : ℕ
⊢ IsNat n m → IsNat (↑n) m
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.refl
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ IsNat n m → IsNat (↑n) m
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m
[PROOFSTEP]
exact ⟨by simp⟩
[GOAL]
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ ↑↑m = ↑m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Ring R
n m : ℤ
⊢ IsInt n m → IsInt (↑n) m
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
R : Type u_1
inst✝ : DivisionRing R
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : DivisionRing R
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
simp only []
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
[PROOFSTEP]
norm_cast
[GOAL]
α : Type ?u.44519
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * (↑k * b) = 1
hc2 : ↑k * b * c = 1
⊢ Invertible b
[PROOFSTEP]
rw [← mul_assoc] at hc1
[GOAL]
α : Type ?u.44519
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : ↑k * b * c = 1
⊢ Invertible b
[PROOFSTEP]
rw [Nat.cast_commute k, mul_assoc, Nat.cast_commute k] at hc2
[GOAL]
α : Type ?u.44519
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : b * (c * ↑k) = 1
⊢ Invertible b
[PROOFSTEP]
exact ⟨_, hc1, hc2⟩
[GOAL]
α : Type ?u.46618
inst✝¹ : Semiring α
a k b : ℕ
inst✝ : Invertible ↑a
h : a = k * b
⊢ ↑a = ↑k * ↑b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsRat a na da →
      IsRat b nb db →
        Int.add (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc → Nat.mul da db = Nat.mul k dc → IsRat (f a b) nc dc
[PROOFSTEP]
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * db + nb * da = k * nc) (h₂ : da * db = k * dc)
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
[PROOFSTEP]
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da : α) db
[GOAL]
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)
[PROOFSTEP]
simpa using invertibleMul (da : α) db
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this : Invertible ↑(da * db)
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
[PROOFSTEP]
have := invertibleOfMul' (α := α) h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
[PROOFSTEP]
use this
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : (fun x => ↑x * (⅟↑da * ⅟↑db)) (na * ↑db + nb * ↑da) = (fun x => ↑x * (⅟↑da * ⅟↑db)) (↑k * nc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp only [Int.cast_add, Int.cast_mul, Int.cast_ofNat, ← mul_assoc, add_mul, mul_mul_invOf_self_cancel] at h₁
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
h₂ : (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (da * db) = (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (k * dc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [← mul_assoc, H] at h₁ h₂
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
rw [h₁, h₂, Nat.cast_commute]
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
[PROOFSTEP]
simp only [mul_mul_invOf_self_cancel, (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
  (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑(Int.neg num✝) * ⅟↑denom✝
[PROOFSTEP]
rw [← neg_mul, ← Int.cast_neg]
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ ↑(-num✝) * ⅟↑denom✝ = ↑(Int.neg num✝) * ⅟↑denom✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ IsRat (f a b) nc dc
[PROOFSTEP]
rw [hf, sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ IsRat (a + -b) nc dc
[PROOFSTEP]
refine isRat_add rfl ra (isRat_neg (n' := -nb) rfl rb rfl) (k := k) (nc := nc) ?_ h₂
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (Int.mul (-nb) ↑da) = Int.mul (↑k) nc
[PROOFSTEP]
rw [show Int.mul (-nb) _ = _ from neg_mul ..]
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (-(nb * ↑da)) = Int.mul (↑k) nc
[PROOFSTEP]
exact h₁
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HMul.hMul →
    IsRat a na da → IsRat b nb db → Int.mul na nb = Int.mul (↑k) nc → Nat.mul da db = Nat.mul k dc → IsRat (f a b) nc dc
[PROOFSTEP]
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * nb = k * nc) (h₂ : da * db = k * dc)
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
[PROOFSTEP]
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da : α) db
[GOAL]
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)
[PROOFSTEP]
simpa using invertibleMul (da : α) db
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this : Invertible ↑(da * db)
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
[PROOFSTEP]
have := invertibleOfMul' (α := α) h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
[PROOFSTEP]
refine ⟨this, ?_⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₁ := congr_arg (Int.cast (R := α)) h₁
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑(na * nb) = ↑(↑k * nc)
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
simp only [Int.cast_mul, Int.cast_ofNat] at h₁
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (da * db) = (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (k * dc)
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [← mul_assoc] at h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
rw [H] at h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑db * ⅟↑da * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [mul_mul_invOf_self_cancel] at h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
rw [h₂, Nat.cast_commute]
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑da * ⅟↑db = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
[PROOFSTEP]
simp only [mul_mul_invOf_self_cancel, (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
  (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
[GOAL]
«$α» : Type u
«$a» «$b» : «$α»
«$sα» : Semiring «$α»
«$f» : «$α» → «$α» → «$α» := HMul.hMul
«$e» : «$α» := «$a» * «$b»
«$mα'» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$mα» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$mα» «$mα'»
[GOAL]
«$α» : Type u
«$a» «$b» : «$α»
«$sα» : Semiring «$α»
«$f» : «$α» → «$α» → «$α» := HMul.hMul
«$e» : «$α» := «$a» * «$b»
«$na» «$nb» : ℕ
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
apply AddCommMonoidWithOne.toAddMonoidWithOne
[GOAL]
a b : ℕ
c : ℕ
h1 : Nat.pow a b = c
⊢ Nat.pow a (2 * b) = Nat.mul c c
[PROOFSTEP]
simp [two_mul, pow_add, ← h1]
[GOAL]
a b : ℕ
c : ℕ
h1 : Nat.pow a b = c
⊢ Nat.pow a (2 * b + 1) = Nat.mul c (Nat.mul c a)
[PROOFSTEP]
simp [two_mul, pow_add, mul_assoc, ← h1]
[GOAL]
a✝ b✝ : Q(ℕ)
depth : ℕ
a b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q (Nat.pow «$a» «$b₀» = «$c₀»)
b' : ℕ := Expr.natLit! b
d : ℕ := depth >>> 1
hi : Q(ℕ)
⊢ «$p» =Q (Nat.pow «$a» «$b₀» = «$c₀»)
[PROOFSTEP]
exact hp
[GOAL]
a b : ℕ
c : ℕ
h1 : Nat.pow a b = c
⊢ Int.pow (Int.ofNat a) b = Int.ofNat c
[PROOFSTEP]
simp [← h1]
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.pow (Int.negOfNat a) b = Int.ofNat c
[PROOFSTEP]
rw [← hb, Int.negOfNat_eq, pow_eq, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc, ← h1]
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (Nat.pow a b' * Nat.pow a b')
[PROOFSTEP]
simp
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.pow (Int.negOfNat a) b = Int.negOfNat c
[PROOFSTEP]
rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc, ←
  h1]
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ -Int.ofNat a * (Int.ofNat a ^ b' * Int.ofNat a ^ b') = -Int.ofNat (Nat.pow a b' * (Nat.pow a b' * a))
[PROOFSTEP]
simp [mul_assoc, mul_comm, mul_left_comm]
[GOAL]
α : Type u_1
inst✝ : Semiring α
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(Nat.pow n✝¹ n✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝¹ : ℤ
n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(Int.pow n✝¹ n✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → ℕ → α
a : α
an cn : ℤ
ad b b' cd : ℕ
⊢ f = HPow.hPow → IsRat a an ad → IsNat b b' → Int.pow an b' = cn → Nat.pow ad b' = cd → IsRat (f a b) cn cd
[PROOFSTEP]
rintro rfl ⟨_, rfl⟩ ⟨rfl⟩ (rfl : an ^ b = _) (rfl : ad ^ b = _)
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
[PROOFSTEP]
have := invertiblePow (ad : α) b
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
[PROOFSTEP]
rw [← Nat.cast_pow] at this
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
[PROOFSTEP]
use this
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ (↑an * ⅟↑ad) ^ b = ↑(an ^ b) * ⅟↑(ad ^ b)
[PROOFSTEP]
simp [invOf_pow, Commute.mul_pow]
[GOAL]
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat (Nat.succ n)) d → IsRat a⁻¹ (Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
rintro ⟨_, rfl⟩
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ IsRat (↑(Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
refine ⟨this, by simp⟩
[GOAL]
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ (↑(Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ = ↑(Int.ofNat d) * ⅟↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑1)⁻¹ = ↑1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑0)⁻¹ = ↑0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑(Int.negOfNat 1))⁻¹ = ↑(Int.negOfNat 1)
[PROOFSTEP]
simp [inv_neg_one]
[GOAL]
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.negOfNat (Nat.succ n)) d → IsRat a⁻¹ (Int.negOfNat d) (Nat.succ n)
[PROOFSTEP]
rintro ⟨_, rfl⟩
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.negOfNat d) (Nat.succ n)
[PROOFSTEP]
simp only [Int.negOfNat_eq]
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
generalize Nat.succ n = n at *
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ IsRat (↑(-Int.ofNat n) * ⅟↑d)⁻¹ (-Int.ofNat d) n
[PROOFSTEP]
use this
[GOAL]
case eq
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, Int.cast_neg, Int.cast_ofNat, invOf_eq_inv, inv_neg, neg_mul, mul_inv_rev, inv_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ / x✝²) x✝¹ x✝
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
[PROOFSTEP]
exact h
[GOAL]
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (mkRat ↑n✝¹ ↑n✝) num✝ denom✝
[PROOFSTEP]
rw [Rat.mkRat_eq_div]
[GOAL]
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
simp only [σh, Rat.ofScientific_true_def]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
exact eq
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
n✝¹ n✝ x✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
h : x✝ = Nat.mul n✝¹ (10 ^ n✝)
⊢ OfScientific.ofScientific (↑n✝¹) false ↑n✝ = ↑x✝
[PROOFSTEP]
simp [σh, Rat.ofScientific_false_def, h]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
n✝¹ n✝ x✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
h : x✝ = Nat.mul n✝¹ (10 ^ n✝)
⊢ ↑(↑n✝¹ * 10 ^ n✝) = ↑n✝¹ * 10 ^ n✝
[PROOFSTEP]
norm_cast
[GOAL]
x y : ℕ
⊢ Nat.ble x y = false ↔ y < x
[PROOFSTEP]
rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]
[GOAL]
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : Nat.beq n✝¹ n✝ = false
⊢ ¬↑n✝¹ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : Nat.beq n✝¹ n✝ = false
⊢ ¬n✝¹ = n✝
[PROOFSTEP]
exact Nat.ne_of_beq_eq_false h
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬↑n✝¹ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬n✝¹ = n✝
[PROOFSTEP]
exact of_decide_eq_false h
[GOAL]
α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
[PROOFSTEP]
rw [mul_invOf_eq_iff_eq_mul_right, ← Int.commute_cast, mul_assoc, ← mul_left_eq_iff_eq_invOf_mul, Int.commute_cast]
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
congr
[GOAL]
case e_a.h.e_5.h
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := Int.cast_mono (α := α) <| of_decide_eq_true h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h✝ : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h :
  ⅟↑db * ((fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) * ⅟↑da) ≤
    ⅟↑db * ((fun x => ↑x) (Int.mul num✝ (Int.ofNat da)) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
rw [← mul_assoc, Int.commute_cast] at h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h✝ : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑(Int.mul num✝¹ (Int.ofNat db)) * ⅟↑db * ⅟↑da ≤ ⅟↑db * ((fun x => ↑x) (Int.mul num✝ (Int.ofNat da)) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
simp at h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h✝ : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑num✝¹ * ⅟↑da ≤ ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
rwa [Int.commute_cast] at h
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * ↑db < num✝ * ↑da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := Int.cast_strictMono (α := α) <| of_decide_eq_true h
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ⅟↑db * ((fun x => ↑x) (num✝¹ * ↑db) * ⅟↑da) < ⅟↑db * ((fun x => ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
rw [← mul_assoc, Int.commute_cast] at h
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑(num✝¹ * ↑db) * ⅟↑db * ⅟↑da < ⅟↑db * ((fun x => ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
simp at h
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
rwa [Int.commute_cast] at h
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (Int.mul num✝¹ (Int.ofNat denom✝) = Int.mul num✝ (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
rw [Rat.invOf_denom_swap]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (Int.mul num✝¹ (Int.ofNat denom✝) = Int.mul num✝ (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
[PROOFSTEP]
exact_mod_cast of_decide_eq_false h
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
n✝ : ℕ
⊢ Nat.succ ↑n✝ = ↑(Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ - ↑n✝ = ↑(Nat.sub n✝¹ n✝)
[PROOFSTEP]
simp
[GOAL]
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ % ↑n✝ = ↑(Nat.mod n✝¹ n✝)
[PROOFSTEP]
aesop
[GOAL]
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ / ↑n✝ = ↑(Nat.div n✝¹ n✝)
[PROOFSTEP]
aesop


[GOAL]
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Finite ℤ M
hM : IsTorsion ℤ M
⊢ _root_.Finite M
[PROOFSTEP]
rcases Module.equiv_directSum_of_isTorsion hM with ⟨ι, _, p, h, e, ⟨l⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ _root_.Finite M
[PROOFSTEP]
haveI : ∀ i : ι, NeZero (p i ^ e i).natAbs := fun i => ⟨Int.natAbs_ne_zero.mpr <| pow_ne_zero (e i) (h i).ne_zero⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this : ∀ (i : ι), NeZero (Int.natAbs (p i ^ e i))
⊢ _root_.Finite M
[PROOFSTEP]
haveI : ∀ i : ι, _root_.Finite <| ℤ ⧸ Submodule.span ℤ {p i ^ e i} := fun i =>
  Finite.of_equiv _ (p i ^ e i).quotientSpanEquivZMod.symm.toEquiv
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this✝ : ∀ (i : ι), NeZero (Int.natAbs (p i ^ e i))
this : ∀ (i : ι), _root_.Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ _root_.Finite M
[PROOFSTEP]
haveI : _root_.Finite (⨁ i, ℤ ⧸ (Submodule.span ℤ {p i ^ e i} : Submodule ℤ ℤ)) :=
  Finite.of_equiv _ DFinsupp.equivFunOnFintype.symm
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Finite ℤ M
hM : IsTorsion ℤ M
ι : Type
w✝ : Fintype ι
p : ι → ℤ
h : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
this✝¹ : ∀ (i : ι), NeZero (Int.natAbs (p i ^ e i))
this✝ : ∀ (i : ι), _root_.Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})
this : _root_.Finite (⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i})
⊢ _root_.Finite M
[PROOFSTEP]
exact Finite.of_equiv _ l.symm.toEquiv
[GOAL]
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
⊢ ∃ n ι x p x e, Nonempty (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ :=
  @Module.equiv_free_prod_directSum _ _ _ _ _ _ _ (Module.Finite.iff_addGroup_fg.mpr hG)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ ∃ n ι x p x e, Nonempty (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
refine' ⟨n, ι, fι, fun i => (p i).natAbs, fun i => _, e, ⟨_⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_1
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
i : ι
⊢ Nat.Prime ((fun i => Int.natAbs (p i)) i)
[PROOFSTEP]
rw [← Int.prime_iff_natAbs_prime, ← GCDMonoid.irreducible_iff_prime]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_1
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
i : ι
⊢ Irreducible (p i)
[PROOFSTEP]
exact hp i
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.refine'_2
G : Type u
inst✝ : AddCommGroup G
hG : AddGroup.FG G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℤ
hp : ∀ (i : ι), Irreducible (p i)
e : ι → ℕ
f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}
⊢ G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod ((fun i => Int.natAbs (p i)) i ^ e i)
[PROOFSTEP]
exact
  f.toAddEquiv.trans
    ((AddEquiv.refl _).prodCongr <|
      DFinsupp.mapRange.addEquiv fun i =>
        ((Int.quotientSpanEquivZMod _).trans <| ZMod.ringEquivCongr <| (p i).natAbs_pow _).toAddEquiv)
[GOAL]
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
obtain ⟨n, ι, fι, p, hp, e, ⟨f⟩⟩ := equiv_free_prod_directSum_zmod G
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
n : ℕ
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
cases' n with n
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.zero
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin Nat.zero →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
have : Unique (Fin Nat.zero →₀ ℤ) := { uniq := by simp only [Nat.zero_eq, eq_iff_true_of_subsingleton] }
[GOAL]
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin Nat.zero →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∀ (a : Fin Nat.zero →₀ ℤ), a = default
[PROOFSTEP]
simp only [Nat.zero_eq, eq_iff_true_of_subsingleton]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.zero
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin Nat.zero →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Unique (Fin Nat.zero →₀ ℤ)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
exact ⟨ι, fι, p, hp, e, ⟨f.trans AddEquiv.uniqueProd⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.succ
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (Nat.succ n) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
haveI := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.succ
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (Nat.succ n) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Fintype (Fin (Nat.succ n) →₀ ℤ)
⊢ ∃ ι x p x e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
[PROOFSTEP]
exact
  (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
      ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim


[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ Normal (derivedSeries G n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Normal (derivedSeries G Nat.zero)
[PROOFSTEP]
exact (⊤ : Subgroup G).normal_of_characteristic
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : Normal (derivedSeries G n)
⊢ Normal (derivedSeries G (Nat.succ n))
[PROOFSTEP]
exact @Subgroup.commutator_normal G _ (derivedSeries G n) (derivedSeries G n) ih ih
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ map f (derivedSeries G Nat.zero) ≤ derivedSeries G' Nat.zero
[PROOFSTEP]
exact le_top
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : map f (derivedSeries G n) ≤ derivedSeries G' n
⊢ map f (derivedSeries G (Nat.succ n)) ≤ derivedSeries G' (Nat.succ n)
[PROOFSTEP]
simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ derivedSeries G' Nat.zero ≤ map f (derivedSeries G Nat.zero)
[PROOFSTEP]
exact (map_top_of_surjective f hf).ge
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
ih : derivedSeries G' n ≤ map f (derivedSeries G n)
⊢ derivedSeries G' (Nat.succ n) ≤ map f (derivedSeries G (Nat.succ n))
[PROOFSTEP]
exact commutator_le_map_commutator ih ih
[GOAL]
G✝ : Type u_1
G' : Type u_2
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
⊢ IsSolvable G
[PROOFSTEP]
letI hG' : CommGroup G := { hG with mul_comm := h }
[GOAL]
G✝ : Type u_1
G' : Type u_2
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
[PROOFSTEP]
cases hG
[GOAL]
case mk
G✝ : Type u_1
G' : Type u_2
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_3
toDivInvMonoid✝ : DivInvMonoid G
mul_left_inv✝ : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
[PROOFSTEP]
exact CommGroup.isSolvable
[GOAL]
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Subsingleton G
⊢ ⊤ = ⊥
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
⊢ IsSolvable G
[PROOFSTEP]
obtain ⟨n, hn⟩ := id hG''
[GOAL]
case mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ IsSolvable G
[PROOFSTEP]
obtain ⟨m, hm⟩ := id hG'
[GOAL]
case mk.intro.mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ IsSolvable G
[PROOFSTEP]
refine' ⟨⟨n + m, le_bot_iff.mp (map_bot f ▸ hm ▸ _)⟩⟩
[GOAL]
case mk.intro.mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
[PROOFSTEP]
clear hm
[GOAL]
case mk.intro.mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
[PROOFSTEP]
induction' m with m hm
[GOAL]
case mk.intro.mk.intro.zero
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ derivedSeries G (n + Nat.zero) ≤ map f (derivedSeries G' Nat.zero)
[PROOFSTEP]
exact
  f.range_eq_map ▸
    ((derivedSeries G n).map_eq_bot_iff.mp (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans
      hfg
[GOAL]
case mk.intro.mk.intro.succ
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ derivedSeries G (n + Nat.succ m) ≤ map f (derivedSeries G' (Nat.succ m))
[PROOFSTEP]
exact commutator_le_map_commutator hm hm
[GOAL]
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
⊢ derivedSeries G (Nat.succ n) = _root_.commutator G
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
⊢ derivedSeries G (Nat.succ Nat.zero) = _root_.commutator G
[PROOFSTEP]
exact derivedSeries_one G
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
⊢ derivedSeries G (Nat.succ (Nat.succ n)) = _root_.commutator G
[PROOFSTEP]
rw [_root_.derivedSeries_succ, ih, _root_.commutator]
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
[PROOFSTEP]
cases' (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h h
[GOAL]
case succ.inl
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
[PROOFSTEP]
rw [h, commutator_bot_left]
[GOAL]
case succ.inr
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
[PROOFSTEP]
rwa [h]
[GOAL]
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ ∀ (a b : G), a * b = b * a
[PROOFSTEP]
cases n
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
⊢ ∀ (a b : G), a * b = b * a
[PROOFSTEP]
intro a b
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ a * b = b * a
[PROOFSTEP]
refine' (mem_bot.1 _).trans (mem_bot.1 _).symm
[GOAL]
case zero.refine'_1
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ a * b ∈ ⊥
[PROOFSTEP]
rw [← hn]
[GOAL]
case zero.refine'_1
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ a * b ∈ derivedSeries G Nat.zero
[PROOFSTEP]
exact mem_top _
[GOAL]
case zero.refine'_2
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ b * a ∈ ⊥
[PROOFSTEP]
rw [← hn]
[GOAL]
case zero.refine'_2
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ b * a ∈ derivedSeries G Nat.zero
[PROOFSTEP]
exact mem_top _
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : derivedSeries G (Nat.succ n✝) = ⊥
⊢ ∀ (a b : G), a * b = b * a
[PROOFSTEP]
rw [IsSimpleGroup.derivedSeries_succ] at hn
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
⊢ ∀ (a b : G), a * b = b * a
[PROOFSTEP]
intro a b
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a
[PROOFSTEP]
rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ closure (commutatorSet G)
[PROOFSTEP]
exact subset_closure ⟨a, b, rfl⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
let x : Equiv.Perm (Fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], by decide, by decide⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
let y : Equiv.Perm (Fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], by decide, by decide⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
⊢ Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
⊢ Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
let z : Equiv.Perm (Fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], by decide, by decide⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
⊢ Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
⊢ Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
⊢ x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
refine' not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => _
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ x ≠ 1
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
⊢ x ∈ derivedSeries (Perm (Fin 5)) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ x ∈ derivedSeries (Perm (Fin 5)) Nat.zero
[PROOFSTEP]
exact mem_top x
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : x ∈ derivedSeries (Perm (Fin 5)) n
⊢ x ∈ derivedSeries (Perm (Fin 5)) (Nat.succ n)
[PROOFSTEP]
rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : x ∈ derivedSeries (Perm (Fin 5)) n
⊢ ⁅x, y * x * y⁻¹⁆ ∈ derivedSeries (Perm (Fin 5)) (Nat.succ n)
[PROOFSTEP]
exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
⊢ ¬IsSolvable (Perm X)
[PROOFSTEP]
intro h
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ False
[PROOFSTEP]
have key : Nonempty (Fin 5 ↪ X) := by
  rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ Nonempty (Fin 5 ↪ X)
[PROOFSTEP]
rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
key : Nonempty (Fin 5 ↪ X)
⊢ False
[PROOFSTEP]
exact
  Equiv.Perm.fin_5_not_solvable
    (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))