mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫
      (forgetStalk IM I M R x).inv ≫ ↾⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ smoothSheaf.evalHom IM I R x

Tactic:
rw [smoothSheafCommRing.ι_forgetStalk_inv_assoc, smoothSheaf.ι_evalHom]

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      ↾⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
    ↾smoothSheaf.evalAt IM I (↑(CommRingCat.of R)) x (unop U)
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hx
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiff[s]
hu : UniqueMDiff[u]
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst✝⁹] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
this✝ :
  ↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 (↑(extChartAt I x₀) x₀)]
    ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
this :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
⊢ ↑(extChartAt I x₀) x₀ ∈ ↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target

Tactic:
· simp [hx₀]

Goal state after:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E' : Type u_2
E'' : Type u_3
E''' : Type u_4
F : Type u_5
F' : Type u_6
H : Type u_7
H' : Type u_8
G : Type u_9
G' : Type u_10
E : Type u
inst✝²⁸ : NontriviallyNormedField 𝕜
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
M' : Type u_12
N : Type u_13
N' : Type u_14
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x✝¹ : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsSubmersionAtOfComplement F I J n f✝ x✝¹
hg : IsSubmersionAtOfComplement F' I' J' n g✝ x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : E ≃L[𝕜] E'' × F
hfprop : EqOn (↑(ψ₁.extend J) ∘ f ∘ ↑(φ₁.extend I).symm) (Prod.fst ∘ ⇑equiv₁) (φ₁.extend I).target
equiv₂ : E' ≃L[𝕜] E''' × F'
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (Prod.fst ∘ ⇑equiv₂) (φ₂.extend I').target
x : E × E'
x✝ : x ∈ (φ₁.extend I).target ×ˢ (φ₂.extend I').target
hx : x.1 ∈ (φ₁.extend I).target
hx' : x.2 ∈ (φ₂.extend I').target
⊢ (Prod.fst ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm) x =
    (Prod.fst ∘ Prod.fst ∘ ⇑((equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')))
      x

Tactic:
simpa using hfprop hx

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False

Tactic:
· exact h 0 (by simp)

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r ↑i.val) = n / n.gcd i.val

Tactic:
rw [← r_one_pow, orderOf_pow, orderOf_r_one]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ IsMulCommutative M

Tactic:
have := Fintype.ofFinite M

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ commProb M = 1 ↔ IsMulCommutative M
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Submonoid.closure (Set.range cs.simple) = ⊤

Tactic:
have : range cs.simple = range cs.simple ∪ (range cs.simple)⁻¹ := by
    simp_rw [inv_range, inv_simple, union_self]

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ Submonoid.closure (Set.range cs.simple) = ⊤
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
this : w ∈ Submonoid.closure (Set.range cs.simple)
⊢ p w

Tactic:
induction this using Submonoid.closure_induction_left with
  | one => exact one
  | mul_left i mi y my ih =>
    rw [Set.mem_range] at mi
    exact mi.choose_spec ▸ mul_simple_left _ _ ih

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (FreeGroup.lift f) (M.relation (i, i').1 (i, i').2) = 1

Tactic:
relation,

Goal state after:
B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
i i' : B
⊢ (FreeGroup.lift f) ((FreeGroup.of (i, i').1 * FreeGroup.of (i, i').2) ^ M.M (i, i').1 (i, i').2) = 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
⊢ ¬m₁ = 1 →
    ((m₁ = m₂ * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1) ↔
      (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂)

Tactic:
intro hm1

Goal state after:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ (m₁ = m₂ * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1) ↔
    (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.length 1 = 0

Tactic:
exact cs.length_one

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsReflection (w * t * w⁻¹)

Tactic:
by
  obtain ⟨u, i, rfl⟩ := ht
  use w * u, i
  group

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.IsReduced ω.reverse ↔ cs.IsReduced ω

Tactic:
simp [IsReduced]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg.nil
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
hij : ¬i = j
ne_one✝ : ∀ l ∈ [], l.snd ≠ 1
chain_ne✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) []
⊢ (⟨i, m₁⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
      (i ≠ j ∧
          ∃ (h : { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
            { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ };
                  {
                    head :=
                      m₂ *
                        if h :
                            ∃ (h : { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
                              ({ toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head h).fst = j then
                          ⋯ ▸ ({ toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head ⋯).snd
                        else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
            (∃ m',
                ⟨j, m'⟩ ∈ { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head? ∧
                  m₁ = ⋯ ▸ (m₂ * m')) ∨
              { toList := [], ne_one := ne_one✝, chain_ne := chain_ne✝ }.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

Tactic:
simp [or_comm, hij, Ne.symm hij, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg.cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
hij : ¬i = j
head✝ : (i : ι) × M i
tail✝ : List ((i : ι) × M i)
ne_one✝ : ∀ l ∈ head✝ :: tail✝, l.snd ≠ 1
chain_ne✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (head✝ :: tail✝)
⊢ (⟨i, m₁⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
      (i ≠ j ∧
          ∃ (h : { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
            { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ };
                  {
                    head :=
                      m₂ *
                        if h :
                            ∃ (h : { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ≠ []),
                              ({ toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head
                                    h).fst =
                                j then
                          ⋯ ▸ ({ toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head ⋯).snd
                        else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.tail ∨
            (∃ m',
                ⟨j, m'⟩ ∈ { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.toList.head? ∧
                  m₁ = ⋯ ▸ (m₂ * m')) ∨
              { toList := head✝ :: tail✝, ne_one := ne_one✝, chain_ne := chain_ne✝ }.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

Tactic:
simp [or_comm, hij, Ne.symm hij, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: 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.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : ↑U ≠ ↑⊤
⊢ False

Tactic:
coe_top,

Goal state after:
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.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : ↑U ≠ Set.univ
⊢ False
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j : ι
w : NeWord M i j
⊢ ∀ l ∈ w.toList, l.snd ≠ 1

Tactic:
induction w
    · simpa only [toList, List.mem_singleton, ne_eq, forall_eq]
    · intro l h
      simp only [toList, List.mem_append] at h
      cases h <;> aesop

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: 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.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
⊢ FG G

Tactic:
by
  set q := QuotientGroup.mk (s := map f ⊤)
  -- Main proof idea: `s` together with elements of sufficiently small "height" `h` generates `G`.
  let S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
  let U := closure S
  suffices U = ⊤ from Group.fg_iff.mpr ⟨S, this, hs.union <| Northcott.finite_le _⟩
  by_contra! H -- Assume for contradiction that these elements generate a proper subgroup `U`.
  rw [← SetLike.coe_ne_coe, coe_top, ← Set.nonempty_compl] at H
  -- Then we can find an element `x : G` not in `U` and of minimal height.
  obtain ⟨x, hx₁, hx₂⟩ := Northcott.exists_min_image h Uᶜ H
  -- Now we construct an element `y` of smaller height and not in `U`.
  obtain ⟨g, hg, z, ⟨y, rfl⟩, rfl⟩ := Set.mem_mul.mp <| H₁ ▸ Set.mem_univ x
  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₁
  -- To obtain a contradiction, we do cases on whether `y ∈ U`.
  by_cases hy : y ∈ U
  · exact hx₁ <| U.mul_mem (mem_closure_of_mem <| .inl hg) <| hf U <| mem_map_of_mem f hy
  · exact H'.not_ge <| hx₂ y hy

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
⊢ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
exact mem_doubleCoset.mp (h.symm ▸ mem_doubleCoset_self H K b)

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : Quotient ↑H ↑K
h : ¬Disjoint (doubleCoset (Quotient.out a) ↑H ↑K) (doubleCoset (Quotient.out b) ↑H ↑K)
⊢ a = b

Tactic:
simpa [out_eq'] using mk_eq_of_doubleCoset_eq (eq_of_not_disjoint h)

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_1.e'_4
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑s • n = (↑s * ↑t) • ↑s' • n'

Tactic:
simp_rw [smul_smul, ← mul_rotate s'.val, ← smul_smul, ← h', smul_smul]

Goal state after:
case e'_1.e'_4
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * (↑t' * ↑s)) • n = (↑s' * (↑s * ↑t')) • n
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.refine_2
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : ↑s • 0 < ↑1 • m
⊢ 0 < m

Tactic:
simpa using ha

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
a : ↥H
ha : x = ↑a * q
⊢ x = ↑a * q * 1

Tactic:
simpa using ha

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
⊢ Function.Bijective fun g ↦ { toFun := fun φ ↦ φ g, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
by
      refine (Nat.bijective_iff_injective_and_card _).mpr ⟨fun _ _ h ↦ ?_, ?_⟩
      · rwa [mk.injEq, OneHom.mk.injEq, funext_iff, forall_apply_eq_apply_iff] at h
      · rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hpp.inl
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hlt : 0 < n
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

Tactic:
have h1n : 1 ≤ n := hlt
      calc
        a i ^ n • X' j ⊆ a i ^ n • (Y i)ᶜ :=
          smul_set_mono ((hXYdisj j i).union_left <| hYdisj hij.symm).subset_compl_right
        _ ⊆ X i := by
          clear hnne0 hlt
          induction n, h1n using Int.leInduction with
          | base => rw [zpow_one]; exact hX i
          | succ n _hle hi =>
            calc
              a i ^ (n + 1) • (Y i)ᶜ = (a i ^ n * a i) • (Y i)ᶜ := by rw [zpow_add, zpow_one]
              _ = a i ^ n • a i • (Y i)ᶜ := mul_smul _ _ _
              _ ⊆ a i ^ n • X i := smul_set_mono <| hX i
              _ ⊆ a i ^ n • (Y i)ᶜ := smul_set_mono (hXYdisj i i).subset_compl_right
              _ ⊆ X i := hi
        _ ⊆ X' i := Set.subset_union_left

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case base
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
⊢ a i ^ (-1) • (X i)ᶜ ⊆ Y i

Tactic:
rw [zpow_neg, zpow_one]; exact hY i

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : H.FiniteIndex
⊢ Group.FG ↥H

Tactic:
obtain ⟨S, hS⟩ := hG.1

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
⊢ Group.FG ↥H