awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
⊢ h y < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
have suffices : a * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) + 2 * c < b * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
Tactic: suffices a * h (g * f y) + 2 * c < b * h (g * f y) by nlinarith [H₂ g hg (f y), H₃ y]
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (hypothesis)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
this : 2 * c / (b - a) < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
⊢ a * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) + 2 * c <
    b * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
have this₁ : 2 * c < (b - a) * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
Tactic: field_simp [sub_pos.mpr H₀] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
⊢ a * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) + 2 * c <
    b * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
have suffices : 2 * c / (b - a) < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
Tactic: suffices 2 * c / (b - a) < h (g * f y) by field_simp [sub_pos.mpr H₀] at this; grind
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
⊢ 2 * c / (b - a) < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
have suffices : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∉ S
Tactic: suffices g * f y ∉ S by grind
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (hypothesis)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
⊢ False
have H' : h y < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
Tactic: have H' : h y < h (g * f y) := by
    suffices a * h (g * f y) + 2 * c < b * h (g * f y) by nlinarith [H₂ g hg (f y), H₃ y]
    suffices 2 * c / (b - a) < h (g * f y) by field_simp [sub_pos.mpr H₀] at this; grind
    suffices g * f y ∉ S by grind
    exact notMem_of_notMem_closure hx₁
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
H' : h y < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
⊢ False
have pos : ∀ (hy : y ∈ U), False
Tactic: by_cases hy : y ∈ U
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
H' : h y < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
pos : ∀ (hy : y ∈ U), False
⊢ False
have neg : ∀ (hy : y ∉ U), False
Tactic: by_cases hy : y ∈ U
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
⊢ Group.FG G
have obtain : ∀ (g : G) (hg₁ : g ∈ s) (hg₂ : ∀ b ∈ s, c b ≤ c g), Group.FG G
Tactic: obtain ⟨g, hg₁, hg₂⟩ := s.exists_max_image c s.toFinite <| Set.range_nonempty qi
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
⊢ s * (↑f.range : Set G) = Set.univ
have refine : ∀ (x : G), ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x
Tactic: refine Set.eq_univ_iff_forall.mpr fun x ↦ Set.mem_mul.mpr ⟨qi (q x), by simp [s], ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
| ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x
have h₁ : ∀ (y : G), y ∈ (↑f.range : Set G) ∧ qi (q x) * y = x
Tactic: enter [1, y]
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x y : G
| y ∈ (↑f.range : Set G) ∧ qi (q x) * y = x
have h₁ : y ∈ f.range ∧ x / qi (q x) = y
Tactic: rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
| ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x
have h₁ : ∀ (y : G), y ∈ f.range ∧ x / qi (q x) = y
Tactic: enter [1, y]; rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
⊢ ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x
have conv : ∃ y ∈ f.range, x / qi (q x) = y
Tactic: conv => enter [1, y]; rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
x : G
⊢ ∃ y ∈ f.range, x / qi (q x) = y
have simp : x / qi (q x) ∈ f.range
Tactic: simp only [↓existsAndEq, and_true]
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
⊢ Group.FG G
have H₁' : s * (↑f.range : Set G) = Set.univ
Tactic: have H₁' : s * f.range = .univ := by
    refine Set.eq_univ_iff_forall.mpr fun x ↦ Set.mem_mul.mpr ⟨qi (q x), by simp [s], ?_⟩
    conv => enter [1, y]; rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]
    simp only [↓existsAndEq, and_true]
    exact eq_iff_div_mem.mp (Function.surjInv_eq mk_surjective _).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
H₁' : s * (↑f.range : Set G) = Set.univ
c' : ℝ := max c₀ (c g)
⊢ Group.FG G
have H₃' : ∀ (x : G), b * h x - c' ≤ h ((f : (a : G) → G) x)
Tactic: have H₃' x : b * h x - c' ≤ h (f x) := by grind [powMonoidHom_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
H₁' : s * (↑f.range : Set G) = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h ((f : (a : G) → G) x)
⊢ Group.FG G
have refine_1 : ∀ (U : Subgroup G) (u : G) (hu : u ∈ Subgroup.map f U), u ∈ U
Tactic: refine Group.fg_of_descent (fun U u hu ↦ ?_) ha H₀ s.toFinite H₁' (fun g' hg' x ↦ ?_) H₃'
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
H₁' : s * (↑f.range : Set G) = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h ((f : (a : G) → G) x)
refine_1 : ∀ (U : Subgroup G) (u : G) (hu : u ∈ Subgroup.map f U), u ∈ U
⊢ Group.FG G
have refine_2 : ∀ (g' : G) (hg' : g' ∈ s) (x : G), h x ≤ a * h (g' * x) + c'
Tactic: refine Group.fg_of_descent (fun U u hu ↦ ?_) ha H₀ s.toFinite H₁' (fun g' hg' x ↦ ?_) H₃'
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom n))
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst_1 : Northcott h
f : G →* G := powMonoidHom n
q : (a : G) → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
H₁' : s * (↑f.range : Set G) = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h ((f : (a : G) → G) x)
U : Subgroup G
u : G
hu : u ∈ Subgroup.map f U
⊢ u ∈ U
have refine_1 : ∀ (u' : G) (hu₁ : u' ∈ U) (hu : Membership.mem (α := G) (Subgroup.map f U) ((f : (a : G) → G) u' : G)),
  Membership.mem (α := G) U ((f : (a : G) → G) u' : G)
Tactic: obtain ⟨u', hu₁, rfl⟩ := mem_map.mp hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
h : G → ℝ
C : ℝ
H₁ : Subgroup.FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom 2))
H₂ : ∀ (x : G), 0 ≤ h x
H₃ : ∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C
inst_1 : Northcott h
⊢ Group.FG G
have H₃' : ∀ (x : G), 4 * h x - (h 1 + C) ≤ h (HPow.hPow (β := ℕ) x 2)
Tactic: have H₃' x : 4 * h x - (h 1 + C) ≤ h (x ^ 2) := by grind [pow_two, div_self']
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
h : G → ℝ
C : ℝ
H₁ : Subgroup.FiniteIndex.{u_1} (G := G) (MonoidHom.range (G := G) (powMonoidHom 2))
H₂ : ∀ (x : G), 0 ≤ h x
H₃ : ∀ (x y : G), |h (x * y) + h (x / y) - 2 * (h x + h y)| ≤ C
inst_1 : Northcott h
H₃' : ∀ (x : G), 4 * h x - (h 1 + C) ≤ h (HPow.hPow (β := ℕ) x 2)
⊢ Group.FG G
have H₂' : ∀ (g x : G), h x ≤ 2 * h (g * x) + (2 * h g⁻¹ + C)
Tactic: have H₂' g x : h x ≤ 2 * h (g * x) + (2 * h g⁻¹ + C) := by grind [mul_inv_cancel_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
α : Type u_2
inst : Monoid A
inst_1 : Pow A α
inst_2 : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective (β := A) fun (a : A) ↦ a ^ n
n : α
a : A
hn : n ≠ 0
⊢ HPow.hPow (α := A) (if x : n = 0 then 1 else ⋯.choose (p := fun (a_1 : A) ↦ a_1 ^ n = a)) n = a
have rw : sorry.choose (p := fun (a_1 : A) ↦ a_1 ^ n = a) ^ n = a
Tactic: rw [dif_neg hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ HSMul.hSMul (β := AddSubgroup A) n ⊤
have rw : Membership.mem (γ := AddSubgroup A) ⊤ a
Tactic: rw [H hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
n : ℤ
a : A
hn : n ≠ 0
⊢ HSMul.hSMul (β := A) n
      (if hn : n = 0 then 0
      else
        Exists.choose (p := fun (a_1 : A) ↦
          a_1 ∈ (↑⊤ : Set A) ∧
            (((DistribMulAction.toAddMonoidEnd ℤ A : (a : ℤ) → AddMonoid.End A) n : AddMonoid.End A) : (a : A) → A)
                a_1 =
              a)
          ⋯) =
    a
have simp_rw : HSMul.hSMul (β := A) n
    (Exists.choose (p := fun (a_1 : A) ↦
      a_1 ∈ (↑⊤ : Set A) ∧
        (((DistribMulAction.toAddMonoidEnd ℤ A : (a : ℤ) → AddMonoid.End A) n : AddMonoid.End A) : (a : A) → A) a_1 = a)
      sorry) =
  a
Tactic: simp_rw [dif_neg hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
n : ℤ
a : A
hn : n ≠ 0
⊢ HSMul.hSMul (β := A) n
      (Exists.choose (p := fun (a_1 : A) ↦
        a_1 ∈ (↑⊤ : Set A) ∧
          (((DistribMulAction.toAddMonoidEnd ℤ A : (a : ℤ) → AddMonoid.End A) n : AddMonoid.End A) : (a : A) → A) a_1 =
            a)
        ⋯) =
    a
have generalize_proofs : ∀
  (h1 :
    ∃ a_1 ∈ (↑⊤ : Set A),
      (((DistribMulAction.toAddMonoidEnd ℤ A : (a : ℤ) → AddMonoid.End A) n : AddMonoid.End A) : (a : A) → A) a_1 = a),
  n •
      h1.choose (p := fun (a_1 : A) ↦
        a_1 ∈ (↑⊤ : Set A) ∧
          (((DistribMulAction.toAddMonoidEnd ℤ A : (a : ℤ) → AddMonoid.End A) n : AddMonoid.End A) : (a : A) → A) a_1 =
            a) =
    a
Tactic: generalize_proofs h1
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
𝕜 : Type u_1
inst : DivisionRing 𝕜
inst_1 : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ n • (q / (↑n : 𝕜)) = q
have rw : (↑n : 𝕜) * (q / (↑n : 𝕜)) = q
Tactic: rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel₀ q (Int.cast_ne_zero.mpr hn)]
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
𝕜 : Type u_1
inst : DivisionRing 𝕜
inst_1 : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
rw : (↑n : 𝕜) * (q / (↑n : 𝕜)) = q
⊢ n • (q / (↑n : 𝕜)) = q
have rw₁ : q / (↑n : 𝕜) * (↑n : 𝕜) = q
Tactic: rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel₀ q (Int.cast_ne_zero.mpr hn)]
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
𝕜 : Type u_1
inst : DivisionRing 𝕜
inst_1 : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
rw : (↑n : 𝕜) * (q / (↑n : 𝕜)) = q
rw₁ : q / (↑n : 𝕜) * (↑n : 𝕜) = q
⊢ n • (q / (↑n : 𝕜)) = q
have rw₂ : q = q
Tactic: rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel₀ q (Int.cast_ne_zero.mpr hn)]
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℕ
n : ℤ
a : A
hn : n ≠ 0
⊢ HPow.hPow (α := A)
      (match (motive := ℤ → A) n with
        | ofNat n => @RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a n
        | -[n+1] => (@RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a (n + 1))⁻¹ :
        A)
      n =
    a
have ofNat : ∀ (a_1 : ℕ) (hn : ofNat a_1 ≠ 0),
  HPow.hPow (α := A)
      (match (motive := ℤ → A) ofNat a_1 with
        | ofNat n => @RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a n
        | -[n+1] => (@RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a (n + 1))⁻¹ :
        A)
      (ofNat a_1) =
    a
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℕ
n : ℤ
a : A
hn : n ≠ 0
ofNat :
  ∀ (a_1 : ℕ) (hn : Int.ofNat a_1 ≠ 0),
    HPow.hPow (α := A)
        (match (motive := ℤ → A) Int.ofNat a_1 with
          | Int.ofNat n => @RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a n
          | -[n+1] => (@RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a (n + 1))⁻¹ :
          A)
        (Int.ofNat a_1) =
      a
⊢ HPow.hPow (α := A)
      (match (motive := ℤ → A) n with
        | Int.ofNat n => @RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a n
        | -[n+1] => (@RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a (n + 1))⁻¹ :
        A)
      n =
    a
have negSucc : ∀ (a_1 : ℕ) (hn : -[a_1+1] ≠ 0),
  HPow.hPow (α := A)
      (match (motive := ℤ → A) -[a_1+1] with
        | Int.ofNat n => @RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a n
        | -[n+1] => (@RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a (n + 1))⁻¹ :
        A)
      -[a_1+1] =
    a
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (hypothesis)
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℕ
a : A
a_1 : ℕ
hn : ofNat a_1 ≠ 0
⊢ HPow.hPow (α := A)
      (match (motive := ℤ → A) ofNat a_1 with
        | ofNat n => @RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a n
        | -[n+1] => (@RootableBy.root _ _ DivInvMonoid.toMonoid Monoid.toPow MulZeroClass.toZero _ a (n + 1))⁻¹ :
        A)
      (ofNat a_1) =
    a
have hn₁ : a_1 ≠ 0
Tactic: rw [Int.ofNat_eq_natCast, Nat.cast_ne_zero] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (hypothesis)
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ @RootableBy.root _ ℤ DivInvMonoid.toMonoid DivInvMonoid.toZPow MulZeroClass.toZero _ a (↑n : ℤ) ^ n = a
have this : HPow.hPow (β := ℤ) (@RootableBy.root _ ℤ DivInvMonoid.toMonoid DivInvMonoid.toZPow MulZeroClass.toZero _ a (↑n : ℤ))
    (↑n : ℤ) =
  a
Tactic: have := RootableBy.root_cancel a (show (n : ℤ) ≠ 0 from mod_cast hn)
-- Lean 4 proof step from Mathlib.GroupTheory.Divisible (goal)
Goal:
A : Type u_1
B : Type u_2
α : Type u_3
inst : Zero α
inst_1 : Monoid A
inst_2 : Monoid B
inst_3 : Pow A α
inst_4 : Pow B α
inst_5 : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f (@RootableBy.root _ _ inst_1 inst_3 inst _ y n) ^ n = x
have rw : f (@RootableBy.root _ _ inst_1 inst_3 inst _ y n ^ n) = x
Tactic: rw [← hpow (RootableBy.root y n) n, RootableBy.root_cancel _ hn, hy]