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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ f (a ⊔ b) ⊔ g (a ⊔ b) = (⇑f ⊔ ⇑g) a ⊔ (⇑f ⊔ ⇑g) b

Tactic:
map_sup,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ f a ⊔ f b ⊔ g (a ⊔ b) = (⇑f ⊔ ⇑g) a ⊔ (⇑f ⊔ ⇑g) b
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b ⊔ b \ a) = f a \ f b ⊔ f b \ f a

Tactic:
map_sup,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) ⊔ f (b \ a) = f a \ f b ⊔ f b \ f a
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).min' h = f (s.min' ⋯)

Tactic:
by
  simp only [min', inf'_image]
  exact .symm <| apply_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ ∀ (a b : List α), ⟦a⟧ ∈ powerset ⟦b⟧ ↔ ⟦a⟧ ≤ ⟦b⟧

Tactic:
simp [Subperm, and_comm]

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

Goal state before:
pp: case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Tactic:
· rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH

Goal state after:
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 ⊔ s.sup g) = (⇑f ∘ g) i ⊔ s.sup (⇑f ∘ g)

Tactic:
map_sup,

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) ⊔ f (s.sup g) = (⇑f ∘ g) i ⊔ s.sup (⇑f ∘ g)
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 : α
⊢ a < s.sup' H f ↔ ∃ b ∈ s, a < f b

Tactic:
rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]

Goal state after:
α : 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
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : ConditionallyCompletePartialOrderSup α
p : Prop
inst✝ : Decidable p
f : p → α
H : p
⊢ ⨆ (h : p), f h = if h : p then f h else sSup ∅

Tactic:
simp [ciSup_neg, H]

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : ConditionallyCompletePartialOrderSup α
p : Prop
inst✝ : Decidable p
f : p → α
H : ¬p
⊢ ⨆ (h : p), f h = if h : p then f h else sSup ∅

Tactic:
simp [ciSup_neg, H]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∈ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f

Tactic:
simp [h, le_sup]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddBelow s
h : sInf s ≤ sInf ∅
⊢ ⨅ i, ↑i ≤ sInf ∅

Tactic:
· convert! h
    rw [← sInf_range, Subtype.range_coe]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : DecidableEq ι
f : ι → α
s t st : Finset ι
a : α
x✝ : a ∈ Set.range fun x ↦ ⨆ (_ : x ∈ st), f x
i : ι
ha : (fun x ↦ ⨆ (_ : x ∈ st), f x) i = a
h : i ∉ st
⊢ (fun x ↦ ⨆ (_ : x ∈ st), f x) i ≤ st.sup f

Tactic:
simp [h, le_sup]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) × α i → Prop
inst✝ : DecidablePred p
i : ι
a : α i
⊢ ⟨i, a⟩ ∈ filter p (s.sigma t) ↔ ⟨i, a⟩ ∈ s.sigma fun i ↦ {x ∈ t i | p ⟨i, x⟩}

Tactic:
simp [Finset.mem_filter, Finset.mem_sigma, and_assoc]

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

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
⊢ (t.preimage Subtype.val ⋯).sup id = ⟨t.sup id, ⋯⟩

Tactic:
let : OrderBot (Subtype P) := Subtype.orderBot Pbot
  ext
  simp only [sup_coe, id_eq]
  apply sup_preimage_self
  refine ⟨mapsTo_preimage _ _, injOn_of_injective Subtype.val_injective, ?_⟩
  intro x hx; simpa using ⟨hx, ht x hx⟩

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b

Tactic:
rw [Iic, ← Finset.mem_def, Finset.mem_Iic]

Goal state after:
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:
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:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ Ico a b.succ ↔ x ∈ insert b (Ico a b)

Tactic:
mem_insert,

Goal state after:
a b : ℕ
h : a ≤ b
x : ℕ
⊢ x ∈ Ico a b.succ ↔ x = b ∨ x ∈ Ico a b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inl
n : ℕ
⊢ image (fun x ↦ x % 0) (Ico n n) = ∅

Tactic:
Ico_self,

Goal state after:
case inl
n : ℕ
⊢ image (fun x ↦ x % 0) ∅ = ∅
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
⊢ Finite α

Tactic:
by
  apply Finite.of_not_infinite
  intro
  obtain ⟨f, hStrictMono | hStrictAnti⟩ := Infinite.exists_strictMono_or_strictAnti α
  · exact not_strictMono_of_wellFoundedGT f hStrictMono
  · exact not_strictAnti_of_wellFoundedLT f hStrictAnti

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
hr : WellQuasiOrdered r
⊢ s.Finite

Tactic:
by_contra! hi
  obtain ⟨m, n, hmn, h⟩ := hr fun n => hi.natEmbedding _ n
  exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    hs.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
contrapose!; exact Iio_eq_empty

Goal state after:
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 ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ (orbitRel ↥H ↑x.orbit) a ⟦a⟧.out

Tactic:
← Quotient.eq'',

Goal state after:
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 ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ Quotient.mk'' a = Quotient.mk'' ⟦a⟧.out
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ stabilizer G a ≤ stabilizer G (a • b)

Tactic:
simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : G
⊢ ϕ h * ϕ g = ϕ (g * h)

Tactic:
map_mul

Goal state after:
G : Type u_1
inst✝ : Group G
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (center G)
h : G
⊢ ϕ h * ϕ g = ϕ g * ϕ h
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ center G ≤ normalizer s

Tactic:
intro x hx y
  simp [← mem_center_iff.mp hx y]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
g h : M
H : IsConj g h
Hg : g ∈ Set.center M
⊢ g = h

Tactic:
rcases H with ⟨u, hu⟩; rwa [← u.mul_left_inj, Hg.comm u]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S T : Set M
inst✝ : Mul M
⊢ (S ∪ T).centralizer = S.centralizer ∩ T.centralizer

Tactic:
by
  simp [centralizer, or_imp, forall_and, ofPred_and]

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'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer ↑H)
h : G
hh : h ∈ ↑H
⊢ ϕ h * ϕ g = ϕ (g * h)

Tactic:
map_mul

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer ↑H)
h : G
hh : h ∈ ↑H
⊢ ϕ h * ϕ g = ϕ g * ϕ h
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, a • ↑(closure s) = ↑(closure s)

Tactic:
have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
    smul_coe_set <| subset_closure ha

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
h : ∀ a ∈ s, a • ↑(closure s) = ↑(closure s)
⊢ ⋃ a ∈ s, a • ↑(closure s) = ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : map (↑(MulAut.conj g)) H = H ∧ map (↑(MulAut.conj g)) K = K
⊢ map (↑(MulAut.conj g)) (H ⊔ K) = H ⊔ K

Tactic:
map_sup,

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
hg : map (↑(MulAut.conj g)) H = H ∧ map (↑(MulAut.conj g)) K = K
⊢ map (↑(MulAut.conj g)) H ⊔ map (↑(MulAut.conj g)) K = H ⊔ K
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
G : Type u_7
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
⊢ g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)

Tactic:
by
  simp only [Finset.prod_eq_multiset_prod, map_multiset_prod, Multiset.map_map]; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : g ∈ closure s
x : X
hx : x ∈ t
⊢ g • x ∈ t

Tactic:
by
  induction hg using Subgroup.closure_induction'' generalizing x with
  | one => simpa
  | mem g' hg' => exact hst g' hg' x hx
  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : ι → κ
hi : ∀ a ∈ s, i a ∈ t
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
h : ∀ a ∈ s, f a = g (i a)
⊢ ∀ b ∈ t, ∃ a, ∃ (_ : a ∈ s), i a = b

Tactic:
simpa using! i_surj

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

Goal state before:
pp: α : Type u_1
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk' a = y) ↔ ∀ {y : α}, ⊤ → s a y

Tactic:
refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)

Goal state after:
α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ ⊤ → s a b
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d : Con M
f : M → N
H : ∀ (x y : M), f (x * y) = f x * f y
c : Con N
w x y z : M
h1 : (Setoid.comap f c.toSetoid) w x
h2 : (Setoid.comap f c.toSetoid) y z
⊢ c (f w * f y) (f x * f z)

Tactic:
exact c.mul h1 h2

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

Goal state before:
pp: case head
α : Type u
LL₁ c✝ L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
h₁₂ : Step ((a, b) :: L₁) c✝
⊢ Red L₁ L₂

Tactic:
Step.cons_left_iff

Goal state after:
case head
α : Type u
LL₁ c✝ L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
h₁₂ : (∃ L, Step L₁ L ∧ c✝ = (a, b) :: L) ∨ L₁ = (a, !b) :: c✝
⊢ Red L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case head.inr
α : Type u
LL₁ c✝ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red ((a, !b) :: c✝) L₂

Tactic:
· exact (cons_cons h).tail Step.cons_not_rev

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
w✝ x✝ y✝ z✝ : M
h1 : f w✝ = f x✝
h2 : f y✝ = f z✝
⊢ f x✝ * f z✝ = f (x✝ * z✝)

Tactic:
map_mul

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
w✝ x✝ y✝ z✝ : M
h1 : f w✝ = f x✝
h2 : f y✝ = f z✝
⊢ f x✝ * f z✝ = f x✝ * f z✝
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
⊢ f (m * n) = f m * f n

Tactic:
map_mul

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
⊢ f m * f n = f m * f n
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x : FreeGroup α
⊢ (map _root_.id) x = x

Tactic:
by rcases x with ⟨L⟩; simp [List.map_id']

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
p : ι → Prop
s : Finset { x // p x }
f : { x // p x } → M
g : ι → M
h : ∀ x ∈ s, g ↑x = f x
⊢ ∏ x ∈ map (Embedding.subtype fun x ↦ p x) s, g x = ∏ x ∈ s, f x

Tactic:
Finset.prod_map

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
p : ι → Prop
s : Finset { x // p x }
f : { x // p x } → M
g : ι → M
h : ∀ x ∈ s, g ↑x = f x
⊢ ∏ x ∈ s, g ((Embedding.subtype fun x ↦ p x) x) = ∏ x ∈ s, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∏ x ∈ s, f x = ∏ x ∈ t, g x

Tactic:
calc
    ∏ x ∈ s, f x = ∏ x ∈ s with f x ≠ 1, f x := by rw [prod_filter_ne_one]
    _ = ∏ x ∈ t with g x ≠ 1, g x :=
      prod_bij (fun a ha => i a (mem_filter.mp ha).1 <| by simpa using (mem_filter.mp ha).2)
        ?_ ?_ ?_ ?_
    _ = ∏ x ∈ t, g x := prod_filter_ne_one _

Goal state after:
case calc_1
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ ∈ {x ∈ t | g x ≠ 1}

case calc_2
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a₁ : ι) (ha₁ : a₁ ∈ {x ∈ s | f x ≠ 1}) (a₂ : ι) (ha₂ : a₂ ∈ {x ∈ s | f x ≠ 1}), i a₁ ⋯ ⋯ = i a₂ ⋯ ⋯ → a₁ = a₂

case calc_3
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ b ∈ {x ∈ t | g x ≠ 1}, ∃ a, ∃ (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ = b

case calc_4
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g (i a ⋯ ⋯)
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:

Tactic:
c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
      _ = (a * c)⁻¹ * (b * d) := by
        simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure ↑Finset.univ = ⊤

Tactic:
rw [Finset.coe_univ]

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure Set.univ = ⊤
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
N : Submonoid M
⊢ FG ↥N ↔ N.FG

Tactic:
by
  conv_rhs => rw [← N.mrange_subtype, MonoidHom.mrange_eq_map]
  exact ⟨fun h ↦ h.fg_top.map N.subtype, fun h => ⟨h.map_injective N.subtype Subtype.coe_injective⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : Monoid M
⊢ (∃ α, ∃ (_ : Finite α), ∃ φ, Function.Surjective ⇑φ) → FG M

Tactic:
· intro ⟨α, _, φ, hφ⟩
    exact Monoid.fg_of_surjective _ hφ

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure ↑Finset.univ = ⊤

Tactic:
rw [Finset.coe_univ]

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure Set.univ = ⊤
Module: Mathlib.GroupTheory.Abelianization.Defs

Goal state before:
pp: G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutator G ≤ f.ker

Tactic:
rw [commutator_eq_closure, Subgroup.closure_le]

Goal state after:
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑f.ker
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ f ↑(f.sec (f x)).2 * f x = f (↑(f.sec (f x)).2 * x)

Tactic:
map_mul

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ f ↑(f.sec (f x)).2 * f x = f ↑(f.sec (f x)).2 * f x
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
j : N →* P
x✝ : N
⊢ j (f (f.sec x✝).1) = j (f ↑(f.sec x✝).2 * x✝)

Tactic:
sec_spec'

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f ↑c * f x = f (↑c * y)
⊢ f x = f y

Tactic:
map_mul

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f ↑c * f x = f ↑c * f y
⊢ f x = f y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f ↑c * f x = f (↑c * y)
⊢ f x = f y

Tactic:
map_mul

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f ↑c * f x = f ↑c * f y
⊢ f x = f y
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f g : α →+*o β
h : (fun f ↦ (↑↑f.toRingHom).toFun) f = (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ f = g

Tactic:
cases f; cases g; congr
    exact DFunLike.coe_injective h

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ 0 = untopD 0 a * 0

Tactic:
mul_zero

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ 0 = untopD 0 ↑a✝ * 0

Tactic:
mul_zero

Goal state after:
case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ 0 = 0