mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
⊢ ∃ C > 0, ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < C

Tactic:
rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace% x) x
    with ⟨C, C_pos, hC⟩

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
⊢ ∃ C > 0, ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ < C
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
⊢ Set.range ⇑(ConcreteCategory.hom ((locallyRingedSpace IM M).ofRestrict ⋯).base) ⊆
    Set.range ⇑(ConcreteCategory.hom (locallyRingedSpaceMap Subtype.val ⋯).base)

Tactic:
by rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
⊢ Set.range ⇑(ConcreteCategory.hom (locallyRingedSpaceMap Subtype.val ⋯).base) ⊆
    Set.range ⇑(ConcreteCategory.hom ((locallyRingedSpace IM M).ofRestrict ⋯).base)

Tactic:
by rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
x' : M
⊢ (if σ x' = σ' x' then 1 else 0) • σ x' = (if σ x' = σ' x' then 1 else 0) • σ' x'

Tactic:
split_ifs with hx' <;> simp [hx']

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

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ :
  ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x =
    ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : ↑(f.toFun (f.ind x hx)) x = ↑(f.toFun (f.ind x hx)) y
⊢ x = y

Tactic:
f.apply_ind x hx

Goal state after:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
y : M
a✝ : y ∈ s
h :
  ∀ (x_1 : ι),
    (↑(f.toFun x_1) x • ↑(extChartAt I (f.c x_1)) x, ↑(f.toFun x_1) x) =
      (↑(f.toFun x_1) y • ↑(extChartAt I (f.c x_1)) y, ↑(f.toFun x_1) y)
h₁ :
  ↑(f.toFun (f.ind x hx)) x • ↑(extChartAt I (f.c (f.ind x hx))) x =
    ↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y
h₂ : 1 = ↑(f.toFun (f.ind x hx)) y
⊢ x = y
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) = Nat.card ↥(_root_.commutator G)

Tactic:
by
  rw [commutator_eq_closure G, ← image_commutatorSet_closureCommutatorRepresentatives, ←
    MonoidHom.map_closure, ← commutator_eq_closure]
  exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

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

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n

Tactic:
apply (Nat.le_of_dvd (NeZero.pos n) <|
      orderOf_dvd_of_pow_eq_one <| @r_one_pow_n n).lt_or_eq.resolve_left
    intro h
    have h1 : (r 1 : DihedralGroup n) ^ orderOf (r 1) = 1 := pow_orderOf_eq_one _
    rw [r_one_pow] at h1
    injection h1 with h2
    rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2
    exact absurd h2.symm (orderOf_pos _).ne

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

Goal state before:
pp: n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
simp_rw [Nat.card_congr (oddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]

Goal state after:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ n + (n + (n + n * n)) = n * (n + 3)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)

Tactic:
dif_neg h0,

Goal state after:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ (if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    3 :: reciprocalFactors (n / 2)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
⊢ (if x : n = 0 then [0]
    else
      if x : n = 1 then []
      else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)

Tactic:
dif_neg h0,

Goal state after:
n : ℕ
h1 : n ≠ 1
h2 : Odd n
h0 : n ≠ 0
⊢ (if x : n = 1 then []
    else if Even n then 3 :: reciprocalFactors (n / 2) else n % 4 * n :: reciprocalFactors (n / 4 + 1)) =
    n % 4 * n :: reciprocalFactors (n / 4 + 1)
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_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
⊢ p w

Tactic:
let p' : ((w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop) :=
    fun w _ ↦ p w
  have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
  induction this using Submonoid.closure_induction_right with
  | one => exact one
  | mul_right y my i mi ih =>
    rw [Set.mem_range] at mi
    exact mi.choose_spec ▸ mul_simple_right _ _ ih

Goal state after:
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
a : PresentedGroup M.relationsSet
⊢ cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm a) = cs.mulEquiv (cs.mulEquiv.symm a)

Tactic:
by rfl

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

Goal state before:
pp: case succ
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) =
    if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)

Tactic:
| succ k h' =>

Goal state after:
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
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)

Tactic:
tsub_eq_of_eq_add (mul_two (M i i'))

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : cs.wordProd (alternatingWord i i' (M.M i i')) = cs.wordProd (alternatingWord i' i (M.M i i'))
⊢ cs.wordProd (braidWord M i i') = cs.wordProd (braidWord M i' i)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ y :: l, l_1.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)),
    { toList := y :: l, ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := y :: l, ne_one := hnot1, chain_ne := hchain }.toList
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain }.toList

Tactic:
rw [List.isChain_cons_cons] at hchain
      specialize hi hnot1.2 hchain.2 (by rintro ⟨rfl⟩)
      obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi
      obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?
      refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩
      simpa [toWord] using hw'

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m m' : M
s s' : ℕ+
⊢ mk m s ≤ mk m' s' ↔ ↑s' • m ≤ ↑s • m'

Tactic:
by rfl

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
hbc : b ≤ c
ma : M
sa : ℕ+
hab : mk ma sa ≤ b
⊢ mk ma sa ≤ c

Tactic:
induction b with

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
c : DivisibleHull M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
hbc : mk mb sb ≤ c
hab : mk ma sa ≤ mk mb sb
⊢ mk ma sa ≤ c
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
h : mk ma sa ≤ b
h' : b ≤ mk ma sa
⊢ mk ma sa = b

Tactic:
induction b with

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : mk ma sa ≤ mk mb sb
h' : mk mb sb ≤ mk ma sa
⊢ mk ma sa = mk mb sb
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b : DivisibleHull M
ma : M
sa : ℕ+
⊢ mk ma sa ≤ b ∨ b ≤ mk ma sa

Tactic:
induction b with

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
⊢ mk ma sa ≤ mk mb sb ∨ mk mb sb ≤ mk ma sa
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : DivisibleHull M
h : b < c
ma : M
sa : ℕ+
⊢ mk ma sa + b < mk ma sa + c

Tactic:
induction b with

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
c : DivisibleHull M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : mk mb sb < c
⊢ mk ma sa + mk mb sb < mk ma sa + c
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
b c : DivisibleHull M
h : b < c
⊢ a • b < a • c

Tactic:
induction b with

Goal state after:
case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
c : DivisibleHull M
mb : M
sb : ℕ+
h : mk mb sb < c
⊢ a • mk mb sb < a • c
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), ¬h = 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
w : Word H
Heq : (lift f) w.prod = 1
⊢ w.prod = 1

Tactic:
empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq,

Goal state after:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), ¬h = 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
w : Word H
Heq : (lift f) w.prod = 1
⊢ Word.empty.prod = 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ↑↑s • mk m s = ↑↑s' • mk m s'
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')

Tactic:
apply_fun ArchimedeanClass.mk at this

Goal state after:
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ArchimedeanClass.mk (↑↑s • mk m s) = ArchimedeanClass.mk (↑↑s' • mk m s')
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
b : DivisibleHull M
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝ den✝) ≤ ArchimedeanClass.mk b
⊢ (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤ b.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯

Tactic:
induction b with

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
num✝¹ : M
den✝¹ : ℕ+
num✝ : M
den✝ : ℕ+
h : ArchimedeanClass.mk (mk num✝¹ den✝¹) ≤ ArchimedeanClass.mk (mk num✝ den✝)
⊢ (mk num✝¹ den✝¹).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤
    (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯
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)
Φ : (Subgroup (G →* Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
⊢ (fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker)
      ((fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ) =
    Φ

Tactic:
ext φ

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
Φ : (Subgroup (G →* Mˣ))ᵒᵈ
this : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ))
φ : G →* Mˣ
⊢ φ ∈
      OrderDual.ofDual
        ((fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker)
          ((fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ)) ↔
    φ ∈ OrderDual.ofDual Φ
Module: Mathlib.GroupTheory.CoprodI

Goal state before:

Tactic:
a i ^ n • X' j ⊆ a i ^ n • (X i)ᶜ :=
          smul_set_mono ((hXdisj hij.symm).union_left (hXYdisj i j).symm).subset_compl_right
        _ ⊆ Y i := by
          clear hnne0 hgt
          induction n, h1n using Int.leInductionDown with
          | base => rw [zpow_neg, zpow_one]; exact hY i
          | pred n hle hi =>
            calc
              a i ^ (n - 1) • (X i)ᶜ = (a i ^ n * (a i)⁻¹) • (X i)ᶜ := by rw [zpow_sub, zpow_one]
              _ = a i ^ n • (a i)⁻¹ • (X i)ᶜ := mul_smul _ _ _
              _ ⊆ a i ^ n • Y i := smul_set_mono <| hY i
              _ ⊆ a i ^ n • (X i)ᶜ := smul_set_mono (hXYdisj i i).symm.subset_compl_right
              _ ⊆ Y i := hi
        _ ⊆ X' i := Set.subset_union_right

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:

Tactic:
_ ≤ #(R * S) := Finset.card_image_le
    _ ≤ #R * #S := Finset.card_mul_le
    _ = H.index * S.card := congr_arg (· * S.card) ?_

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
hR1 : 1 ∈ R
⊢ #R = H.index
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
S : Finset G
hS : closure ↑S = ⊤
⊢ Group.FG ↥H

Tactic:
obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS

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 = ⊤
T : Finset ↥H
hT : closure ↑T = ⊤
⊢ Group.FG ↥H
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ ↑(List.map
          (fun q ↦
            ⟨(Quotient.out q.out)⁻¹ * ↑⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ ↑⟨g, ⋯⟩ • x) q.out * Quotient.out q.out,
              ⋯⟩)
          Finset.univ.toList).prod =
    ↑(List.map (fun i ↦ ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) i.out) Finset.univ.toList).prod

Tactic:
simp only [Subgroup.val_list_prod, List.map_map]

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
inst✝ : H.FiniteIndex
g : G
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
key : ∀ (k : ℕ) (g₀ : G) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑⟨g₀⁻¹ * g ^ k * g₀, hk⟩ = g ^ k
⊢ (List.map
        (Subtype.val ∘ fun q ↦
          ⟨(Quotient.out q.out)⁻¹ * g ^ Function.minimalPeriod (fun x ↦ g • x) q.out * Quotient.out q.out, ⋯⟩)
        Finset.univ.toList).prod =
    (List.map (Subtype.val ∘ fun i ↦ ⟨g, ⋯⟩ ^ Function.minimalPeriod (fun x ↦ g • x) i.out) Finset.univ.toList).prod
Module: Mathlib.Order.Radical

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (Order.radical α) = Order.radical β

Tactic:
unfold Order.radical

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
β : Type u_2
inst✝ : CompleteLattice β
f : α ≃o β
⊢ f (⨅ a ∈ {H | IsCoatom H}, a) = ⨅ a ∈ {H | IsCoatom H}, a
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
x✝ y : G
⊢ x✝ + y + -x✝ = y ↔ y + x✝ = x✝ + y

Tactic:
add_neg_eq_iff_eq_add,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
x✝ y : G
⊢ x✝ + y = y + x✝ ↔ y + x✝ = x✝ + y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤

Tactic:
nilpotencyClass_def,

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ upperCentralSeries G (Nat.find ⋯) = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ nilpotencyClass G' ≤ nilpotencyClass G

Tactic:
nilpotencyClass_def,

Goal state after:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
⊢ Nat.find ⋯ ≤ nilpotencyClass G
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsBlock G B
g : G
⊢ g • B ≠ B → Disjoint (g • B) B

Tactic:
by simpa using hB (g₂ := 1)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ ⦃B_1 : Set X⦄, (B_1 ∈ range fun g ↦ g • B) → IsBlock G B_1

Tactic:
rintro B' ⟨g, rfl⟩; exact hB.translate g

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : x ∈ ofStabilizer G a
y : α
hy : y ∈ ofStabilizer G a
hxy : (conjMap hg) ⟨x, hx⟩ = (conjMap hg) ⟨y, hy⟩
⊢ (fun x ↦ g • x) x = (fun x ↦ g • x) y

Tactic:
rwa [← SetLike.coe_eq_coe, conjMap_apply] at hxy

Goal state after: