mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Max α
inst✝⁴ : Bot α
inst✝³ : Max β
inst✝² : Bot β
inst✝¹ : Max γ
inst✝ : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Max α
inst✝⁴ : Bot α
inst✝³ : Max β
inst✝² : Bot β
inst✝¹ : Max γ
inst✝ : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists' = foldr (fun a r ↦ sublists'Aux a r r) [[]] l

Tactic:
by
  simp only [sublists', sublists'Aux_eq_array_foldl]
  rw [← List.foldr_hom Array.toList]
  · intros; congr

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r₁ x✝ : List (List α)
⊢ sublists'Aux a [] x✝ = x✝ ++ map (cons a) []

Tactic:
by simp [sublists'Aux]

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1, a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
⊢ l'.length = n + 1

Tactic:
rcases h with (h | ⟨l', h, rfl⟩)

Goal state after:
case inl
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1

case inr
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ ++ l₂ ~ []

Tactic:
have : l₁ = [] ∧ l₂ = [] := by simpa using h

Goal state after:
case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
this : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i) ⊔ f (s.sup g) = (⇑f ∘ g) i ⊔ s.sup (⇑f ∘ g)

Tactic:
h,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i) ⊔ s.sup (⇑f ∘ g) = (⇑f ∘ g) i ⊔ s.sup (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f ((cons i s x✝).sup g) = (cons i s x✝).sup (⇑f ∘ g)

Tactic:
by
    rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ (f a✝ \ a ⊔ s✝.sup fun b ↦ f b \ a) = (f a✝ ⊔ s✝.sup f) \ a

Tactic:
h,

Goal state after:
case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ f a✝ \ a ⊔ s✝.sup f \ a = (f a✝ ⊔ s✝.sup f) \ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ (a \ f a✝ ⊔ s✝.sup fun b ↦ a \ f b) = a \ (f a✝ ⊓ s✝.inf f)

Tactic:
h,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ a \ f b) = a \ s✝.inf f
⊢ a \ f a✝ ⊔ a \ s✝.inf f = a \ (f a✝ ⊓ s✝.inf f)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n → ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t

pp: case mpr
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ #t = n

Tactic:
· classical
      intro h
      have : map f (filter (fun x => (f x ∈ t)) s) = t := by grind
      refine ⟨_, ?_, this⟩
      rw [← card_map f, this, h.2]; simp

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ (∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t) → t ⊆ map f s ∧ #t = n
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, ↑a < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b

Tactic:
exact exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite

Tactic:
rw [finite_iUnion_iff (by aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise]))]

Goal state after:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (∀ (i : β), (⋃ (_ : i ∈ s), f i).Finite) ∧ {i | (⋃ (_ : i ∈ s), f i).Nonempty}.Finite ↔
    (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ ¬(a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
h,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬(a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
h,

Goal state after:
α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ ¬(True ∧ ∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
g : β → α
s : Finset α
hgf : LeftInvOn g f ↑s
ginj : InjOn g (g ⁻¹' ↑s)
⊢ image f s = s.preimage g ginj

Tactic:
simp only [SetLike.ext'_iff, coe_preimage, coe_image]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
g : β → α
s : Finset α
hgf : LeftInvOn g f ↑s
ginj : InjOn g (g ⁻¹' ↑s)
⊢ f '' ↑s = g ⁻¹' ↑s
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
h,

Goal state after:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf ∅ + n = sInf {m | p m}
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

pp: case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
· rw [h, Nat.sInf_empty, zero_add]
    obtain hnp | hnp := hn.eq_or_lt
    · exact hnp
    suffices hp : p (sInf { m | p m } - n + n) from (h.subset hp).elim
    rw [Nat.sub_add_cancel hn]
    exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)

Goal state after:
case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | ∀ m ≥ x, P m}

Tactic:
rintro ⟨b, hb⟩

Goal state after:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n b : ℕ
hb : b ∈ upperBounds {x | ∀ m ≥ x, P m}
⊢ False
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) →
    ∀ (f : ℕ → { x // x ∈ s }), ∃ g, ∀ (m n : ℕ), m ≤ n → Subrel r (fun x ↦ x ∈ s) (f (g m)) (f (g n))

Tactic:
exact fun H f ↦ H _ fun n ↦ (f n).2

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Set α
⊢ (WellQuasiOrdered fun x1 x2 ↦ x1 ≤ x2) ↔ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
rw [← wellQuasiOrderedLE_def, ← isWellFounded_iff, wellQuasiOrderedLE_iff_wellFoundedLT]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨m, n, hmn, hr⟩ := hs (fun n ↦ f (φ n)) hφs

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
m n : ℕ
hmn : m < n
hr : r (f (φ m)) (f (φ n))
⊢ ∃ m n, m < n ∧ r (f m) (f n)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ orbit ⟦a⟧
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq']
       at hb
    rw [orbitRel.Quotient.mem_subgroup_orbit_iff]
    convert! hb using 1
    rw [orbit_eq_iff, ← orbitRel_apply, ← Quotient.eq'', Quotient.out_eq', @Quotient.mk''_eq_mk]

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

Goal state before:
pp: case e'_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ Quotient.mk'' b = ⟦a⟧

Tactic:
h,

Goal state after:
case e'_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
⊢ Quotient.mk'' b = ⟦b⟧
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
⊢ center (M × N) = center M ×ˢ center N

Tactic:
aesop (add simp [forall_and, commute_iff_eq, isMulCentral_iff, mem_center_iff])

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
⊢ orbit (ConjAct G) g = (ConjClasses.mk g).carrier

Tactic:
by
  ext h
  rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
⊢ map f (centralizer s) ≤ centralizer (⇑f '' s)

Tactic:
rintro - ⟨g, hg, rfl⟩ - ⟨h, hh, rfl⟩

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f h * f g = f g * f h
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ centralizer Set.univ = ⨅ g ∈ s, centralizer {g}

Tactic:
← coe_top,

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ centralizer ↑⊤ = ⨅ g ∈ s, centralizer {g}
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ normalizer {g} = centralizer {g}

Tactic:
by
  refine ext fun h ↦ ⟨?_, ?_⟩
  · rintro hh g rfl
    exact mul_eq_of_eq_mul_inv (hh g |>.mp rfl).symm
  · refine fun hh g ↦ ⟨?_, ?_⟩ <;> rintro rfl
    · exact (eq_mul_inv_of_mul_eq <| hh g rfl).symm
    · simpa using hh _ rfl

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)

Tactic:
exact (comm_gf hy hx h.symm).symm

Goal state after:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
H : r ≤ ker f
g : Quotient r → β
Hg : f = g ∘ Quotient.mk''
⊢ Quotient.lift f H = g

Tactic:
ext ⟨x⟩
  rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]

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

Goal state before:
pp: α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
h' : [] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ False

Tactic:
simp at h'

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = f (of x)⁻¹ * (f (of x) * g (of x)⁻¹)

Tactic:
h,

Goal state after:
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = f (of x)⁻¹ * (g (of x) * g (of x)⁻¹)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ x ∈ range n, f (x + 1)) * f 0 * f (n + 1)

Tactic:
← prod_range_succ' _ n,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f k) * f (n + 1)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ ⨆ i, closure (⇑(MonoidHom.mulSingle M i) '' ↑(s i)) = Submonoid.pi Set.univ P

Tactic:
← MonoidHom.map_mclosure,

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (closure ↑(s i)) = Submonoid.pi Set.univ P
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure (⇑f '' ↑s) = ⊤

Tactic:
← MonoidHom.map_mclosure,

Goal state after:
case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.map f (Submonoid.closure ↑s) = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
⊢ (∏ x ∈ s \ {x, g x hx}, f x) * ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
h,

Goal state after:
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
⊢ 1 * ∏ x ∈ {x, g x hx}, f x = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s.erase a, f a) * (f a * b₁) = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
h,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s.erase a, f a) * (f a * b₂) = (f a * ∏ a ∈ s.erase a, f a) * b₂
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ f (of x) = 0

Tactic:
h,

Goal state after:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ f 0 = 0
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
⊢ FreeAbelianGroup α →+ FreeAbelianGroup β

Tactic:
by
  refine .mk' (f <*> ·) fun x y ↦ ?_
  change lift (· <$> (x + y)) _ = lift (· <$> x) _ + lift (· <$> y) _
  simp [← Pi.add_def]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
⊢ ∏ j, ∏ i, f ↑i = ∏ i, f i

Tactic:
rw [← Finset.prod_fiberwise _ g f]
  congr with j
  exact (prod_subtype _ (by simp) _).symm

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk p <$> y = (fun b a ↦ (a, b)) <$> y <*> pure p

Tactic:
induction y using FreeAbelianGroup.induction_on' with

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

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K

Tactic:
exact (mul_mem_cancel_right <| inv_mem hk).mp <| hH <| commutator_mem_commutator hh hk

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
z : FreeAbelianGroup T
⊢ (fun n ↦ n • of default) ((lift fun x ↦ 1) (of default)) = of default

Tactic:
by simp only [one_smul, lift_apply_of]

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

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ (↑s' * v') • r₂ = r' • v • r₁

Tactic:
h,

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ (r' * ↑u) • r₂ = r' • v • r₁
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' * (↑u' * ↑s₃) = r' * (v * ↑s₁)

Tactic:
hs₂u,

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' * (v' * ↑s₂) = r' * (v * ↑s₁)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' * v' * ↑s₂ = r' * (v * ↑s₁)

Tactic:
h,

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ r' * ↑u * ↑s₂ = r' * (v * ↑s₁)
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f✝ g✝ : F
x✝ : α
f g : F
x : α
hfg : f x⁻¹ ≤ g x⁻¹
⊢ g x = f x * (f x⁻¹ * g x)

Tactic:
simp [← mul_assoc, ← map_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₂) a = g (f₂ a)
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ (g₁.trans f) a = f (g₂ a)

Tactic:
h,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ (g₂.trans f) a = f (g₂ a)