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

Goal state before:
pp: case inr.refine_1
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
⊢ (if g 0 < g 0 then f (g 0) else (f (g (g 0 - g 0))).tail).length < (f (g 0)).length

Tactic:
simp only [if_neg (lt_irrefl (g 0)), Nat.sub_self]
    rw [List.length_tail, ← Nat.pred_eq_sub_one]
    exact Nat.pred_lt fun con => hnil _ (List.length_eq_zero_iff.1 con)

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

Goal state before:
pp: M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
⊢ c • r • v = r • c • v

Tactic:
have := Semigroup.mem_center_iff.1 c.2

Goal state after:
M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
this : ∀ (g : M), g * ↑c = ↑c * g
⊢ c • r • v = r • c • v
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
x✝ : e x ∈ Set.center N
⊢ x ∈ Set.center M

Tactic:
simpa using

Goal state after:
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e : F
x : M
x✝ : e x ∈ Set.center N
⊢ x ∈ Set.center M
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a : A i
⊢ x i * a = a * x i

Tactic:
simpa using

Goal state after:
ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a : A i
⊢ x i * a = a * x i
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
b c : A i
⊢ x i * (b * c) = x i * b * c

Tactic:
simpa using

Goal state after:
ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
b c : A i
⊢ x i * (b * c) = x i * b * c
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a b : A i
⊢ a * b * x i = a * (b * x i)

Tactic:
simpa using

Goal state after:
ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a b : A i
⊢ a * b * x i = a * (b * x i)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
⊢ a / b ∈ S.centralizer

Tactic:
simpa using

Goal state after:
M : Type u_1
S : Set M
inst✝ : Group M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
⊢ a * b⁻¹ ∈ S.centralizer
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: case succ
α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x ↦ f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x ↦ f x ^ (n + 1)) ⊆ mulSupport f

Tactic:
simpa using

Goal state after:
case succ
α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x ↦ f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x ↦ f x * f x ^ n) ⊆ mulSupport f
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
inst✝ : H.Normal
g : G
hg : g ∈ centralizer ↑H
i h : G
hh : h ∈ ↑H
⊢ h * (i * g * i⁻¹) = i * g * i⁻¹ * h

Tactic:
simpa using

Goal state after:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
H K : Subgroup G
inst✝ : H.Normal
g : G
hg : g ∈ centralizer ↑H
i h : G
hh : h ∈ ↑H
⊢ h * (i * (g * i⁻¹)) = i * (g * (i⁻¹ * h))
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h = g * h * g⁻¹

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h = g * h * g⁻¹
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2.refine_2
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {h * g * h⁻¹}
⊢ g ∈ {h * g * h⁻¹}

Tactic:
simpa using

Goal state after:
case refine_2.refine_2
G : Type u_1
inst✝ : Group G
h g : G
hh : h ∈ centralizer {h * g * h⁻¹}
⊢ g = h * g * h⁻¹
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy (f a) (f x) (f y)

Tactic:
simpa using

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ f a * f x = f y * f a
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : SemiconjBy (f a) (f x) (f y)
⊢ f (a * x) = f (y * a)

Tactic:
simpa using

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : SemiconjBy (f a) (f x) (f y)
⊢ f a * f x = f y * f a
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : Commute (f x) (f y)
⊢ f (x * y) = f (y * x)

Tactic:
simpa using

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hf : Function.Injective ⇑f
h : Commute (f x) (f y)
⊢ f x * f y = f y * f x
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul_left.inr
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x✝ : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
x y : G
hy : y ∈ Submonoid.closure (s ∪ s⁻¹)
ih : p y ⋯
hx : x ∈ s⁻¹
⊢ p (x * y) ⋯

Tactic:
simpa using

Goal state after:
case mul_left.inr
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x✝ : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
x y : G
hy : y ∈ Submonoid.closure (s ∪ s⁻¹)
ih : p y ⋯
hx : x ∈ s⁻¹
⊢ p (x * y) ⋯
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case inv_mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
⊢ ((fun x1 x2 ↦ x1 * x2) x y)⁻¹ ∈ ↑H * ↑N

Tactic:
simpa using

Goal state after:
case inv_mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
⊢ y⁻¹ * x⁻¹ ∈ ↑H * ↑N
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
⊢ f (noncommProd ⟦a✝⟧ comm) = (map ⇑f ⟦a✝⟧).noncommProd ⋯

Tactic:
simpa using

Goal state after:
case h
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
⊢ f a✝.prod = (List.map (⇑f) a✝).prod
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ ?m.28

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ ?m.28
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b

Tactic:
simpa using

Goal state after:
α : Type u_6
a : Multiset α
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ x ∈ Multiset.map f s.val, x = m

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ a ∈ s, f a = m
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
⊢ Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b

Tactic:
simpa using

Goal state after:
α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
⊢ Disjoint i.sum a ↔ ∀ b ∈ i, Disjoint b a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List (Additive M)
⊢ toMul s.sum = (List.map (⇑toMul) s).prod

Tactic:
simp [toMul, ofMul]; rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset (Additive M)
⊢ toMul s.sum = (Multiset.map (⇑toMul) s).prod

Tactic:
simp [toMul, ofMul]; rfl

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

Goal state before:
pp: case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ univ.erase i, Pi.mulSingle x_1 (x x_1) i = 1

Tactic:
simpa using

Goal state after:
case convert_8.h
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ (x_1 : ι), ¬x_1 = i → Pi.mulSingle x_1 (x x_1) i = 1
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Finset M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ ↑s
hf : Function.support f ⊆ ↑t
⊢ ∃ f_1, Function.support f_1 ⊆ ↑s ∧ ∏ a ∈ s, a ^ f_1 a = ∏ a ∈ t, a ^ f a

Tactic:
refine ⟨f, hf.trans hts, .symm <| Finset.prod_subset hts ?_⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Finset M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ ↑s
hf : Function.support f ⊆ ↑t
⊢ ∀ x ∈ s, x ∉ t → x ^ f x = 1
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ (Quotient.mk'' x.1, Quotient.mk'' x.2).1 = (Quotient.mk'' y.1, Quotient.mk'' y.2).1

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ r x.1 y.1
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ (Quotient.mk'' x.1, Quotient.mk'' x.2).2 = (Quotient.mk'' y.1, Quotient.mk'' y.2).2

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ s x.2 y.2
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
x y : (i : ι) → α i
hxy : piSetoid x y
i : ι
⊢ Quotient.mk'' (x i) = Quotient.mk'' (y i)

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
x y : (i : ι) → α i
hxy : piSetoid x y
i : ι
⊢ (r i) (x i) (y i)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Setoid α
⊢ Subsingleton (Quotient s) ↔ s = ⊤

Tactic:
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply]

Goal state after:
α : Type u_1
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → s x y
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Setoid α
a b : α
⊢ Quotient.mk' a = Quotient.mk' b ↔ True → s a b

Tactic:
true_implies,

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
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ s x y

Tactic:
apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy

Goal state after:
case of
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x y : M), r x y → s x y

case refl
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ (x : M), s x x

case symm
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y : M}, ConGen.Rel r x y → s x y → s y x

case trans
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {x y z : M}, ConGen.Rel r x y → ConGen.Rel r y z → s x y → s y z → s x z

case mul
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ ∀ {w x y z : M}, ConGen.Rel r w x → ConGen.Rel r y z → s w x → s y z → s (w * y) (x * z)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
c : Con M
w x : M
x✝ : c w x
⊢ c (w ^ 0) (x ^ 0)

Tactic:
simpa using

Goal state after:
M : Type u_4
inst✝ : Monoid M
c : Con M
w x : M
x✝ : c w x
⊢ c 1 1
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ n.succ) (x ^ n.succ)

Tactic:
simpa using

Goal state after:
M : Type u_4
inst✝ : Monoid M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ n * w) (x ^ n * x)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Group M
c : Con M
w x y z : M
h1 : c w x
h2 : c y z
⊢ c (w / y) (x / z)

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : Group M
c : Con M
w x y z : M
h1 : c w x
h2 : c y z
⊢ c (w * y⁻¹) (x * z⁻¹)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ Int.ofNat n) (x ^ Int.ofNat n)

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ n) (x ^ n)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ Int.negSucc n) (x ^ Int.negSucc n)

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ (n + 1))⁻¹ (x ^ (n + 1))⁻¹
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ ∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴) L₅ ∧ Step ([] ++ tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴)) L₅

Tactic:
simpa using

Goal state after:
α : Type u
tl x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
⊢ ∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: (tl ++ x✝⁴)) L₅ ∧ Step (tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴) L₅
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = tl2.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
H3 : tl ++ x✝⁵ = tl2 ++ x✝⁴
⊢ (x3, b3) :: tl ++ x✝⁵ = (x4, b4) :: tl2 ++ x✝⁴

Tactic:
by simp [H1, H3]

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

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = tl2.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
L₅ : List (α × Bool)
H3 : Step (tl ++ x✝⁵) L₅
H4 : Step (tl2 ++ x✝⁴) L₅
⊢ Step ((x4, b4) :: tl2 ++ x✝⁴) ((x3, b3) :: L₅)

Tactic:
simpa using

Goal state after:
α : Type u
x3 : α
b3 : Bool
tl x✝⁵ : List (α × Bool)
x4 : α
b4 : Bool
tl2 x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
H1 : (x3, b3) = (x4, b4)
H2 : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = tl2.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)
L₅ : List (α × Bool)
H3 : Step (tl ++ x✝⁵) L₅
H4 : Step (tl2 ++ x✝⁴) L₅
⊢ Step ((x4, b4) :: (tl2 ++ x✝⁴)) ((x4, b4) :: L₅)
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
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∀ x ∈ t, x ∉ image e s → g x = 1

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∀ x ∈ t, (∀ x_1 ∈ s, ¬e x_1 = x) → g x = 1
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail
α : Type u
L₁ L₂ b✝ c✝ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ b✝
h₂₃ : Step b✝ c✝
n : ℕ
eq : L₁.length = b✝.length + 2 * n
⊢ L₁.length = c✝.length + 2 * (1 + n)

Tactic:
simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]

Goal state after:
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
p : ι → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
h₁ : x ∈ s
h₂ : ¬f x = 1
⊢ p x

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
h₁ : x ∈ s
h₂ : ¬f x = 1
⊢ p x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case hc
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ p a

Tactic:
simpa using

Goal state after:
case hc
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ p a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ ¬p x

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ ¬p x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
⊢ Step L₁ L₂

Tactic:
simpa using

Goal state after:
α : Type u
L₁ L₂ : List (α × Bool)
h : Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
⊢ Step L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red (invRev L₁) (invRev L₂)
⊢ Red L₁ L₂

Tactic:
simpa using

Goal state after:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red (invRev L₁) (invRev L₂)
⊢ Red L₁ L₂