awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.DedekindFinite
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
a b : M
hab : a * b = 1
c : M
hbc : Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ b * x) c) 1
rwa rwa₁ rwa₂ rwa₃ : b * c = 1
⊢ b * a = 1

Tactic:
rwa [left_inv_eq_right_inv hab hbc]

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.GroupTheory.Descent
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
suffices : U = ⊤
⊢ FG G

Tactic:
suffices U = ⊤ from Group.fg_iff.mpr ⟨S, this, hs.union <| Northcott.finite_le _⟩
-- Module: Mathlib.GroupTheory.Descent
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
by_contra! : ∀ (H : U ≠ ⊤), False
⊢ U = ⊤

Tactic:
by_contra! H
-- Module: Mathlib.GroupTheory.Descent
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 ≠ ⊤
⊢ (↑U : Set G)ᶜ.Nonempty

Tactic:
rw [← SetLike.coe_ne_coe, coe_top, ← Set.nonempty_compl] at H

Premises used: Subgroup.coe_top, SetLike.coe_ne_coe, Set.nonempty_compl
-- Module: Mathlib.GroupTheory.Descent
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
obtain : ∀ (x : G) (hx₁ : x ∈ (↑U : Set G)ᶜ) (hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h x ≤ h a'), False
⊢ False

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := Northcott.exists_min_image h Uᶜ H

Premises used: Compl.compl, Northcott.exists_min_image, SetLike.coe
-- Module: Mathlib.GroupTheory.Descent
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
x : G
hx₁ : x ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h x ≤ h a'
obtain :
  ∀ (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
⊢ False

Tactic:
obtain ⟨g, hg, z, ⟨y, rfl⟩, rfl⟩ := Set.mem_mul.mp <| H₁ ▸ Set.mem_univ x

Premises used: Iff.mp, rfl, Set.mem_mul
-- Module: Mathlib.GroupTheory.Descent
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 :
  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))
nlinarith :
  h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h y →
    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)) +
              (h ((f : (a : G) → G) y) - (a * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) + c)) +
            (b * h y - c - h ((f : (a : G) → G) y)) +
          (0 - (0 - a) * (h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) - h y)) +
        (0 - (a - b) * (h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) - h y)) =
      0
⊢ h y < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))

Tactic:
nlinarith [H₂ g hg (f y), H₃ y]

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Descent
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'
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))
⊢ h y < 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]
-- Module: Mathlib.GroupTheory.Descent
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))
⊢ 2 * c < (b - a) * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))

Tactic:
field_simp [sub_pos.mpr H₀] at this

Premises used: Iff.mpr, sub_pos
-- Module: Mathlib.GroupTheory.Descent
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))

Tactic:
grind
-- Module: Mathlib.GroupTheory.Descent
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'
suffices : 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))

Tactic:
suffices 2 * c / (b - a) < h (g * f y) by field_simp [sub_pos.mpr H₀] at this; grind
-- Module: Mathlib.GroupTheory.Descent
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 : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∉ S
⊢ 2 * c / (b - a) < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))

Tactic:
grind
-- Module: Mathlib.GroupTheory.Descent
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'
suffices : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∉ S
⊢ 2 * c / (b - a) < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))

Tactic:
suffices g * f y ∉ S by grind
-- Module: Mathlib.GroupTheory.Descent
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'
⊢ HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∉ S

Tactic:
notMem_of_notMem_closure hx₁

Premises used: Subgroup.notMem_of_notMem_closure
-- Module: Mathlib.GroupTheory.Descent
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'
⊢ HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∉ S

Tactic:
exact notMem_of_notMem_closure hx₁

Premises used: Subgroup.notMem_of_notMem_closure
-- Module: Mathlib.GroupTheory.Descent
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))

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₁
-- Module: Mathlib.GroupTheory.Descent
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
neg : ∀ (hy : y ∉ U), False
⊢ False

Tactic:
by_cases hy : y ∈ U
-- Module: Mathlib.GroupTheory.Descent
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))
hy : y ∈ U
⊢ False

Tactic:
hx₁ <| U.mul_mem (mem_closure_of_mem <| .inl hg) <| hf U <| mem_map_of_mem f hy

Premises used: Subgroup.mem_map_of_mem, Subgroup.mem_closure_of_mem, Or.inl, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Descent
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))
hy : y ∈ U
⊢ False

Tactic:
exact hx₁ <| U.mul_mem (mem_closure_of_mem <| .inl hg) <| hf U <| mem_map_of_mem f hy

Premises used: Subgroup.mem_map_of_mem, Subgroup.mem_closure_of_mem, Or.inl, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Descent
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))
hy : y ∉ U
⊢ False

Tactic:
H'.not_ge <| hx₂ y hy

Premises used: LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Descent
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))
hy : y ∉ U
⊢ False

Tactic:
exact H'.not_ge <| hx₂ y hy

Premises used: LT.lt.not_ge
-- Module: Mathlib.GroupTheory.Descent
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
obtain : ∀ (g : G) (hg₁ : g ∈ s) (hg₂ : ∀ b ∈ s, c b ≤ c g), Group.FG G
⊢ Group.FG G

Tactic:
obtain ⟨g, hg₁, hg₂⟩ := s.exists_max_image c s.toFinite <| Set.range_nonempty qi

Premises used: Set.exists_max_image, Set.toFinite, Set.range_nonempty
-- Module: Mathlib.GroupTheory.Descent
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
⊢ qi (q x) ∈ s

Tactic:
simp [s]
-- Module: Mathlib.GroupTheory.Descent
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
refine : ∀ (x : G), ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x
⊢ s * (↑f.range : Set G) = Set.univ

Tactic:
refine Set.eq_univ_iff_forall.mpr fun x ↦ Set.mem_mul.mpr ⟨qi (q x), by simp [s], ?_⟩

Premises used: Iff.mpr, Set.eq_univ_iff_forall, And.intro, Exists.intro, Set.mem_mul
-- Module: Mathlib.GroupTheory.Descent
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
h₁ : ∀ (y : G), y ∈ (↑f.range : Set G) ∧ qi (q x) * y = x
| ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x

Tactic:
enter [1, y]
-- Module: Mathlib.GroupTheory.Descent
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
h₁ : y ∈ f.range ∧ x / qi (q x) = y
| y ∈ (↑f.range : Set G) ∧ qi (q x) * y = x

Tactic:
rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]

Premises used: div_eq_iff_eq_mul', eq_comm, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Descent
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
h₁ : ∀ (y : G), y ∈ f.range ∧ x / qi (q x) = y
| ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x

Tactic:
enter [1, y]; rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]

Premises used: div_eq_iff_eq_mul', eq_comm, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Descent
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
conv : ∃ y ∈ f.range, x / qi (q x) = y
⊢ ∃ y ∈ (↑f.range : Set G), qi (q x) * y = x

Tactic:
conv => enter [1, y]; rw [eq_comm, ← div_eq_iff_eq_mul', SetLike.mem_coe]

Premises used: div_eq_iff_eq_mul', eq_comm, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.Descent
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
simp : x / qi (q x) ∈ f.range
⊢ ∃ y ∈ f.range, x / qi (q x) = y

Tactic:
simp only [↓existsAndEq, and_true]

Premises used: and_true, ExistsAndEq.existsAndEq
-- Module: Mathlib.GroupTheory.Descent
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
⊢ x / qi (q x) ∈ f.range

Tactic:
eq_iff_div_mem.mp (Function.surjInv_eq mk_surjective _).symm

Premises used: QuotientGroup.eq_iff_div_mem, Function.surjInv_eq, Iff.mp, QuotientGroup.mk_surjective, Eq.symm