mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝¹ : β
s✝ : Finset β
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : g (s✝.sup' hs✝ f) = s✝.sup' hs✝ (g ∘ f)
⊢ g ((cons a✝¹ s✝ h✝).sup' ⋯ f) = (cons a✝¹ s✝ h✝).sup' ⋯ (g ∘ f)

Tactic:
simp [*]

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

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝ : ι
⊢ f ({a✝}.sup' ⋯ g) = {a✝}.sup' ⋯ (⇑f ∘ g)

Tactic:
simp [*]

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

Goal state before:
pp: case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : f (s✝.sup' hs✝ g) = s✝.sup' hs✝ (⇑f ∘ g)
⊢ f ((cons a✝¹ s✝ h✝).sup' ⋯ g) = (cons a✝¹ s✝ h✝).sup' ⋯ (⇑f ∘ g)

Tactic:
simp [*]

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

Goal state before:
pp: case empty
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ ∅.sup f ↔ ∃ v ∈ ∅, x ∈ f v

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : x ∈ s✝.sup f ↔ ∃ v ∈ s✝, x ∈ f v
⊢ x ∈ (Finset.cons a✝¹ s✝ h✝).sup f ↔ ∃ v ∈ Finset.cons a✝¹ s✝ h✝, x ∈ f v

Tactic:
simp [*]

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

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.sup' ⋯ f ↔ ∃ i ∈ {a✝}, a ∈ f i

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.sup' hs✝ f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup' ⋯ f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
simp [*]

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

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.inf' ⋯ f ↔ ∀ i ∈ {a✝}, a ∈ f i

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.inf' hs✝ f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf' ⋯ f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
simp [*]

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

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
⊢ a ∈ ∅.sup f ↔ ∃ i ∈ ∅, a ∈ f i

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ s✝.sup f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
simp [*]

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

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

Tactic:
by_cases H : p

Goal state after:
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 ∅

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 ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ ⨆ i, OrderDual.toDual (⨅ (_ : i ∈ s), f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯

Tactic:
simp only [toDual_iInf]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
h' : (image f s).Nonempty
⊢ ⨆ i ∈ s, OrderDual.toDual (f i) = (image (⇑OrderDual.toDual) (image f s)).max' ⋯
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h✝ : a = ⊤
⊢ untopD ⊤ (map Subtype.val ⊤) = a

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.Hom.WithTopBot

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : DecidablePred fun x ↦ x = ⊤
a : α
h✝ : ¬a = ⊤
⊢ untopD ⊤ (map Subtype.val ↑⟨a, h✝⟩) = a

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
⊢ ⨅ i, f i = n ↔ (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i

Tactic:
have : OrderBot α := WellFoundedLT.toOrderBot α
  constructor
  · rintro rfl
    exact ⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩
  · rintro ⟨⟨i, rfl⟩, h⟩
    exact le_antisymm (ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : LE α
inst✝ : IsTrans α LE.le
f : ι → α
s : Finset ι
hs : (↑s).Nonempty
⊢ ∃ i, MaximalFor (fun x ↦ x ∈ ↑s) f i

Tactic:
exact s.exists_maximalFor f hs

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Finset.Icc a b = ∅ ↔ ¬a ≤ b

Tactic:
Finset.Icc_eq_empty_iff

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ ¬a ≤ b ↔ ¬a ≤ b
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
⊢ s.WellFoundedOn r ↔ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s

Tactic:
refine ⟨fun h => ?_, f.wellFounded⟩

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
⊢ WellFounded fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := ⋯
f : α → Quotient (orbitRel G α) := ⋯
a : α
⊢ a ∈ ⋃ g, (fun x ↦ g • x) '' U → a ∈ f ⁻¹' f '' U

Tactic:
· intro hx
    rw [Set.mem_iUnion] at hx
    obtain ⟨g, u, hu₁, hu₂⟩ := hx
    rw [Set.mem_preimage, Set.mem_image]
    refine ⟨g⁻¹ • a, ?_, by simp +instances [f, orbitRel, Quotient.eq']⟩
    rw [← hu₂]
    convert! hu₁
    simp only [inv_smul_smul]

Goal state after:
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 : β
⊢ ∀ ⦃x : G⦄, x ∈ stabilizer G a → x ∈ stabilizer G (a • b)

Tactic:
mem_stabilizer_iff,

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.GroupAction.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ ∀ ⦃x : G'⦄, x ∈ stabilizer G' b → x ∈ stabilizer G' (a • b)

Tactic:
mem_stabilizer_iff,

Goal state after:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ ∀ ⦃x : G'⦄, x • b = b → 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)
⊢ g ∈ center G

Tactic:
rw [mem_center_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
s : Set G
x✝¹ : G
x✝ : x✝¹ ∈ s
⊢ x✝¹ * g = g * x✝¹ ↔ ⁅g, x✝¹⁆ = 1

Tactic:
rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul, eq_comm]

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:
exact hg (ϕ h) (Subgroup.characteristic_iff_le_comap.mp hH ϕ hh)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ ⨆ i, S i
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x

Tactic:
rw [iSup_eq_closure] at hx
  induction hx using closure_induction'' with
  | one => exact one
  | mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi
  | inv_mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ (inv_mem hi)
  | mul x y _ _ ihx ihy => exact mul x y ihx ihy

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

Goal state before:
pp: case h.cons.a.inl
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x = a
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
simp [*]

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

Goal state before:
pp: case h.cons.a.inr
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x ∈ tl
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
simp [*]

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

Goal state before:
pp: case h.cons.a.inl
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y = a
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
simp [*]

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

Goal state before:
pp: case h.cons.a.inr
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y ∈ tl
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
simp [*]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : ι → M
⊢ (if p then ∏ x ∈ s, f x else 1) = ∏ x ∈ s, if p then f x else 1

Tactic:
by
  simp only [prod_ite_irrel, prod_const_one]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : ι → M
⊢ (if p then 1 else ∏ x ∈ s, f x) = ∏ x ∈ s, if p then 1 else f x

Tactic:
by
  simp only [prod_ite_irrel, prod_const_one]

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ (Commute on g) x y

Tactic:
dsimp only [Function.onFun]

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
⊢ ∏ i ∈ ∅, f i = 1 ↔ ∀ i ∈ ∅, f i = 1

Tactic:
simp [*]

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, f i = 1 ↔ ∀ i ∈ s✝, f i = 1
⊢ ∏ i ∈ cons a✝¹ s✝ h✝, f i = 1 ↔ ∀ i ∈ cons a✝¹ s✝ h✝, f i = 1

Tactic:
simp [*]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ ∏ x ∈ s.disjUnion t ⋯, f x = ∏ i, f i

Tactic:
classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (rightRel s) a b → (leftRel s) a⁻¹ b⁻¹

Tactic:
rw [leftRel_apply, rightRel_apply]
      exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (leftRel s) a b → (rightRel s) a⁻¹ b⁻¹

Tactic:
rw [leftRel_apply, rightRel_apply]
      exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1 ∈ s, x_1⁻¹ * x ∈ N
y : α
hs : y ∈ s
hN : y⁻¹ * x ∈ N
⊢ x * (y⁻¹ * x)⁻¹ ∈ s

Tactic:
by simpa using hs

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₂ ∩ s₁, g a

Tactic:
inter_comm

Goal state after:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁ ∩ s₂, g a
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)
inst✝ : DecidableEq ι
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P

Tactic:
by
  have := Fintype.ofFinite ι
  refine iSup_map_mulSingle_le.antisymm fun x hx => ?_
  rw [← Finset.noncommProd_mulSingle x]
  exact noncommProd_mem _ _ _ _ fun i _ => mem_iSup_of_mem _ (mem_map_of_mem _ (hx i trivial))

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG

Tactic:
by
  rw [AddSubgroup.fg_iff_addSubmonoid_fg, Subgroup.fg_iff_submonoid_fg]
  exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst✝¹ : G'.Normal
inst✝ : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e) G' = H'
x : H ⧸ H'
⊢ (map H' H' ((↑e).comp ↑e.symm) ⋯) x = x

Tactic:
simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
        MulEquiv.coe_monoidHom_refl, map_id_apply]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ = 1 ↔ q * p = p * q

Tactic:
commutatorElement_eq_one_iff_mul_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ p * q = q * p ↔ q * p = p * q
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ⁅↑p, ↑q⁆ = 1

Tactic:
commutatorElement_eq_one_iff_mul_comm,

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ↑p * ↑q = ↑q * ↑p
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ closure (commutatorSet G)

Tactic:
exact Subgroup.subset_closure (commutator_mem_commutatorSet x y)

Goal state after:
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✝² : PartialOrder β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f g : F
⊢ f = g → ∀ (x : α), f x ≤ g x

Tactic:
by simp +contextual

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
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₁ * ↑a.2 * (↑t₂ * (↑c.2 * b.1)) = ↑t₂ * ↑t₁ * ↑b.2 * (↑a.2 * c.1)

Tactic:
rw [ht₂]

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
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₁ * ↑a.2 * (↑t₂ * (↑b.2 * c.1)) = ↑t₂ * ↑t₁ * ↑b.2 * (↑a.2 * c.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp.mpr
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)
H : Injective ⇑(f.lift hg)
x y : M
h : g x = g y
⊢ f x = f y

Tactic:
← f.lift_eq hg,

Goal state after:
case mp.mpr
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)
H : Injective ⇑(f.lift hg)
x y : M
h : (f.lift hg) (f x) = g 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₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f (↑y₂ * x₁) = f (↑y₁ * x₂)

Tactic:
by
    rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
iterate_succ_apply'

Goal state after:
α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f (f^[n] x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Tactic:
iterate_succ_apply'

Goal state after:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f (f^[k✝] x) ≤ f (f^[k✝] x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Tactic:
iterate_succ_apply'

Goal state after:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f (f^[k✝] x) ≤ f (f^[k✝] x)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ (succ^[n] a) ≤ succ^[m] a

Tactic:
← iterate_succ_apply' succ

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ^[n.succ] a ≤ succ^[m] a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ^[n + 1] b)
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Tactic:
iterate_succ_apply'

Goal state after:
case succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ (succ^[n] b))
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : NoMaxOrder α
⊢ a ⋖ succ a

Tactic:
exact covBy_succ _

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : OrderTop α
⊢ IsMax ⊤

Tactic:
isMax_iff_eq_top

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : OrderTop α
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
⊢ x ⋖ y ↔ y - 1 = x

Tactic:
by
  rw [← pred_eq_sub_one]
  exact pred_eq_iff_covBy.symm

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

Goal state before:
pp: case pos
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
j : ι
v : π j
hs : j ∈ s
⊢ update (s.piecewise f g) j v j = s.piecewise (update f j v) (update g j v) j

Tactic:
simp [*]

Goal state after: