awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- 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
⊢ 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
-- 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
H₁' : s * (↑f.range : Set G) = Set.univ
c' : ℝ := max c₀ (c g)
x : G
⊢ b * h x - c' ≤ h ((f : (a : G) → G) x)

Tactic:
grind [powMonoidHom_apply]

Premises used: powMonoidHom_apply
-- 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
H₁' : s * (↑f.range : Set G) = Set.univ
c' : ℝ := max c₀ (c g)
⊢ ∀ (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]
-- 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
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

Tactic:
Group.fg_of_descent (fun U u hu ↦ ?_) ha H₀ s.toFinite H₁' (fun g' hg' x ↦ ?_) H₃'

Premises used: Group.fg_of_descent, Set.toFinite
-- 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
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
refine_2 : ∀ (g' : G) (hg' : g' ∈ s) (x : G), h x ≤ a * h (g' * x) + c'
⊢ Group.FG G

Tactic:
refine Group.fg_of_descent (fun U u hu ↦ ?_) ha H₀ s.toFinite H₁' (fun g' hg' x ↦ ?_) H₃'

Premises used: Group.fg_of_descent, Set.toFinite
-- 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
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
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)
⊢ u ∈ U

Tactic:
obtain ⟨u', hu₁, rfl⟩ := mem_map.mp hu

Premises used: Iff.mp, Subgroup.mem_map, rfl
-- 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
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' ∈ 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:
U.pow_mem hu₁ n

Premises used: Set.Mem, Subgroup.pow_mem
-- 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
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' ∈ 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:
exact U.pow_mem hu₁ n

Premises used: Subgroup.pow_mem
-- 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
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)
g' : G
hg' : g' ∈ s
x : G
⊢ h x ≤ a * h (g' * x) + c'

Tactic:
grind
-- Module: Mathlib.GroupTheory.Descent
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
x : G
⊢ 4 * h x - (h 1 + C) ≤ h (HPow.hPow (β := ℕ) x 2)

Tactic:
grind [pow_two, div_self']

Premises used: pow_two, div_self'
-- Module: Mathlib.GroupTheory.Descent
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
⊢ ∀ (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']
-- Module: Mathlib.GroupTheory.Descent
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)
g x : G
⊢ h x ≤ 2 * h (g * x) + (2 * h g⁻¹ + C)

Tactic:
grind [mul_inv_cancel_comm]

Premises used: mul_inv_cancel_comm
-- Module: Mathlib.GroupTheory.Descent
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)
⊢ ∀ (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]
-- Module: Mathlib.GroupTheory.Descent
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)
H₂' : ∀ (g x : G), h x ≤ 2 * h (g * x) + (2 * h g⁻¹ + C)
⊢ LE.le (α := ℝ) 0 2

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.Descent
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)
H₂' : ∀ (g x : G), h x ≤ 2 * h (g * x) + (2 * h g⁻¹ + C)
⊢ LT.lt (α := ℝ) 2 4

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.Descent
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)
H₂' : ∀ (g x : G), h x ≤ 2 * h (g * x) + (2 * h g⁻¹ + C)
⊢ Group.FG G

Tactic:
exact fg_of_descent (b := 4) (by norm_num) (by norm_num) H₁ H₂' H₃'

Premises used: CommGroup.fg_of_descent
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
α : Type u_2
inst : Monoid A
inst_1 : Pow A α
inst_2 : Zero α
inst_3 : RootableBy A α
n : α
hn : n ≠ 0
⊢ Function.Surjective (β := A) fun (a : A) ↦ a ^ n

Tactic:
fun x =>
  ⟨RootableBy.root x n, RootableBy.root_cancel _ hn⟩

Premises used: RootableBy.root_cancel, Exists.intro, Function.Surjective, RootableBy.root
-- Module: Mathlib.GroupTheory.Divisible
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
x : A
⊢ Eq.{u_1 + 1} (α := A)
    (if x : Eq.{u_2 + 1} (α := α) 0 0 then 1
    else ⋯.choose (p := fun (a : A) ↦ (fun (a : A) ↦ HPow.hPow.{u_1, u_2, u_1} (β := α) a 0) a = x))
    1

Tactic:
dif_pos rfl

Premises used: dif_pos, rfl
-- Module: Mathlib.GroupTheory.Divisible
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
x : A
⊢ Eq.{u_1 + 1} (α := A)
    (if x : Eq.{u_2 + 1} (α := α) 0 0 then 1
    else ⋯.choose (p := fun (a : A) ↦ (fun (a : A) ↦ HPow.hPow.{u_1, u_2, u_1} (β := α) a 0) a = x))
    1

Tactic:
exact dif_pos rfl

Premises used: dif_pos, rfl
-- Module: Mathlib.GroupTheory.Divisible
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
x : A
⊢ Eq.{u_1 + 1} (α := A)
    (if x : Eq.{u_2 + 1} (α := α) 0 0 then 1
    else ⋯.choose (p := fun (a : A) ↦ (fun (a : A) ↦ HPow.hPow.{u_1, u_2, u_1} (β := α) a 0) a = x))
    1

Tactic:
classical exact dif_pos rfl

Premises used: dif_pos, rfl
-- Module: Mathlib.GroupTheory.Divisible
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
dsimp : HPow.hPow (α := A) (if x : n = 0 then 1 else ⋯.choose (p := fun (a_1 : A) ↦ a_1 ^ n = a)) n = a
⊢ HPow.hPow (α := A) (if x : n = 0 then 1 else ⋯.choose (p := fun (a_1 : A) ↦ (fun (a : A) ↦ a ^ n) a_1 = a)) n = a

Tactic:
dsimp only
-- Module: Mathlib.GroupTheory.Divisible
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
rw : ⋯.choose (p := fun (a_1 : A) ↦ a_1 ^ n = a) ^ n = a
⊢ HPow.hPow (α := A) (if x : n = 0 then 1 else ⋯.choose (p := fun (a_1 : A) ↦ a_1 ^ n = a)) n = a

Tactic:
rw [dif_neg hn]

Premises used: dif_neg
-- Module: Mathlib.GroupTheory.Divisible
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
⊢ ⋯.choose (p := fun (a_1 : A) ↦ a_1 ^ n = a) ^ n = a

Tactic:
(H hn a).choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.GroupTheory.Divisible
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
⊢ ⋯.choose (p := fun (a_1 : A) ↦ a_1 ^ n = a) ^ n = a

Tactic:
exact (H hn a).choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : AddCommGroup A
inst_1 : DivisibleBy A ℤ
n : ℤ
hn : n ≠ 0
⊢ HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤

Tactic:
AddSubgroup.map_top_of_surjective _ fun a => ⟨DivisibleBy.div a n, DivisibleBy.div_cancel _ hn⟩

Premises used: AddSubgroup.map_top_of_surjective, DivisibleBy.div, Exists.intro, DivisibleBy.div_cancel
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
rw : Membership.mem (γ := AddSubgroup A) ⊤ a
⊢ a ∈ HSMul.hSMul (β := AddSubgroup A) n ⊤

Tactic:
rw [H hn]
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ Membership.mem (γ := AddSubgroup A) ⊤ a

Tactic:
trivial
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
n : ℤ
a : A
hn : n ≠ 0
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)
        ⋯) =
    a
⊢ 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

Tactic:
simp_rw [dif_neg hn]

Premises used: dif_neg
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
n : ℤ
a : A
hn : n ≠ 0
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
⊢ 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

Tactic:
generalize_proofs h1
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
n : ℤ
a : A
hn : n ≠ 0
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:
h1.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : AddCommGroup A
H : ∀ {n : ℤ} (_hn : n ≠ 0), HSMul.hSMul (β := AddSubgroup A) n ⊤ = ⊤
n : ℤ
a : A
hn : n ≠ 0
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:
exact h1.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.GroupTheory.Divisible
Goal:
𝕜 : Type u_1
inst : DivisionRing 𝕜
inst_1 : CharZero 𝕜
q : 𝕜
⊢ q / (↑0 : 𝕜) = 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.Divisible
Goal:
𝕜 : Type u_1
inst : DivisionRing 𝕜
inst_1 : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
rw : (↑n : 𝕜) * (q / (↑n : 𝕜)) = q
rw₁ : q / (↑n : 𝕜) * (↑n : 𝕜) = q
rw₂ rw₃ : q = q
⊢ n • (q / (↑n : 𝕜)) = q

Tactic:
rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel₀ q (Int.cast_ne_zero.mpr hn)]

Premises used: Iff.mpr, zsmul_eq_mul, div_mul_cancel₀, Int.cast_commute, Int.cast_ne_zero, Commute.eq
-- Module: Mathlib.GroupTheory.Divisible
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
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
⊢ 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

Tactic:
cases n
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℕ
a : A
a_1 : ℕ
hn : ofNat a_1 ≠ 0
⊢ a_1 ≠ 0

Tactic:
rw [Int.ofNat_eq_natCast, Nat.cast_ne_zero] at hn

Premises used: Int.ofNat_eq_natCast, Nat.cast_ne_zero
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℕ
a : A
a_1 : ℕ
hn : 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:
simp [RootableBy.root_cancel _ hn]

Premises used: RootableBy.root_cancel
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℕ
a : A
a_1 : ℕ
hn : -[a_1+1] ≠ 0
⊢ HPow.hPow (α := A)
      (match (motive := ℤ → A) -[a_1+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)
      -[a_1+1] =
    a

Tactic:
simp [RootableBy.root_cancel _ (Nat.add_one_ne_zero _)]

Premises used: RootableBy.root_cancel, Nat.add_one_ne_zero
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ 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)
-- Module: Mathlib.GroupTheory.Divisible
Goal:
A : Type u_1
inst : Group A
inst_1 : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
this :
  HPow.hPow (β := ℤ) (@RootableBy.root _ ℤ DivInvMonoid.toMonoid DivInvMonoid.toZPow MulZeroClass.toZero _ a (↑n : ℤ))
      (↑n : ℤ) =
    a
⊢ @RootableBy.root _ ℤ DivInvMonoid.toMonoid DivInvMonoid.toZPow MulZeroClass.toZero _ a (↑n : ℤ) ^ n = a

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Divisible
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
rw : f (@RootableBy.root _ _ inst_1 inst_3 inst _ y n ^ n) = x
rw₁ : f y = x
rw₂ rw₃ : x = x
⊢ 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]

Premises used: RootableBy.root_cancel, RootableBy.root
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
s : ℕ+
⊢ Eq.{u_1 + 1} (α := DivisibleHull M) (mk 0 s) 0

Tactic:
simp [mk]

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
motive : DivisibleHull M → Prop
mk : ∀ (num : M) (den : ℕ+), motive (DivisibleHull.mk num den)
⊢ ∀ (x : DivisibleHull M), motive x

Tactic:
LocalizedModule.induction_on fun m s ↦ mk m (↑ⁿ.symm s)

Premises used: LocalizedModule.induction_on
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_1
inst : AddCommMonoid M
m m' : M
s s' : ℕ+
rw :
  (∃ (u : ↥(nonZeroDivisors ℕ)),
      u • HSMul.hSMul (α := ↥(nonZeroDivisors ℕ)) ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s' : ↥(nonZeroDivisors ℕ)) m =
        u •
          HSMul.hSMul (α := ↥(nonZeroDivisors ℕ)) ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s : ↥(nonZeroDivisors ℕ))
            m') ↔
    ∃ (b : ↥(nonZeroDivisors ℕ)),
      (↑((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) b) : ℕ) • (↑s' : ℕ) • m =
        (↑((↑ⁿ.symm : (a : ↥(nonZeroDivisors ℕ)) → ℕ+) b) : ℕ) • (↑s : ℕ) • m'
⊢ Eq (α := DivisibleHull M) (LocalizedModule.mk m ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s))
      (LocalizedModule.mk m' ((↑ⁿ : (a : ℕ+) → ↥(nonZeroDivisors ℕ)) s')) ↔
    ∃ (u : ℕ+), (↑u : ℕ) • (↑s' : ℕ) • m = (↑u : ℕ) • (↑s : ℕ) • m'

Tactic:
rw [LocalizedModule.mk_eq, ↑ⁿ.exists_congr_left]

Premises used: Equiv.exists_congr_left, LocalizedModule.mk_eq, PNat.equivNonZeroDivisorsNat, MulEquiv.toEquiv, OrderMonoidIso.toMulEquiv