mathlib-initiative/mathlib-tactics huggingface dataset:
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
c : Con P
g : N → P
f : M → N
hg : ∀ (x y : N), g (x * y) = g x * g y
hf : ∀ (x y : M), f (x * y) = f x * f y
⊢ ∀ (x y : M), (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y

Tactic:
grind

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

Goal state before:
pp: α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length

Tactic:
rfl

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∈ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
grind

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∉ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
grind

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

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

Tactic:
exact ⟨_, Red.Step.not, Red.Step.cons_not⟩

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f : ι → M
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x1 x2 ↦ x1 * x2) 1 (fun x ↦ f x) (s₁.disjUnion s₂ h)

Tactic:
rfl

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ x✝ b✝ c b : List (α × Bool)
hab hac : Step x✝ b
⊢ ReflGen Step b b

Tactic:
rfl

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ x✝ b✝ c b : List (α × Bool)
hab hac : Step x✝ b
⊢ ReflTransGen Step b b

Tactic:
rfl

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 ∈ ⊤, f x = ∏ i, f i

Tactic:
rfl

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

Goal state before:
pp: α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₁ L₁

Tactic:
rfl

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

Goal state before:
pp: α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₂ L₂

Tactic:
rfl

Goal state after:
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
⊢ (∏ x ∈ s, f (Embedding.inl x)) * ∏ x ∈ t, f (Embedding.inr x) = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
rfl

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

Goal state before:
pp: case cons.refl
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
⊢ Red (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)

Tactic:
apply append_append _ h₂

Goal state after:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
⊢ Red L₃ [(x1, !b1), (x2, b2)]
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_4
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
⊢ mapGen ⇑f = conGen ⇑(mapOfSurjective f h hf)

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
c : Con M
f : N →* M
x y : N
⊢ ↑(f x) = ↑(f y) ↔ c.mk' (f x) = c.mk' (f y)

Tactic:
rfl

Goal state after:
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
⊢ Con.liftOn 1 ⇑f ⋯ = f 1

Tactic:
rfl

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

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ((c.lift f H).comp c.mk') x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: case mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)

Tactic:
rfl

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 g : ι → M
⊢ ∏ x ∈ s, f x * g x = fold (fun x1 x2 ↦ x1 * x2) 1 (fun x ↦ f x * g x) s

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
| cons hd tl ih =>

Goal state after:
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
⊢ ∃ n, L₁.length = c✝.length + 2 * n

Tactic:
exists 1 + n

Goal state after:
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)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflGen Red.Step b b

Tactic:
rfl

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

Goal state before:
pp: α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflTransGen Red.Step b b

Tactic:
rfl

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

Goal state before:
pp: case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ 1 * Quot.mk Red.Step L = Quot.mk Red.Step L

Tactic:
rfl

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

Goal state before:
pp: case e_s
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {a | a ∈ s} = s

Tactic:
grind

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✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∀ b ∈ s, f b = 1

Tactic:
grind

Goal state after:
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
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
⊢ s' ⊆ s

Tactic:
grind

Goal state after:
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
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
⊢ ∀ c ∈ s, c ∉ s' → f c = 1

Tactic:
grind

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

Goal state before:
pp: case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ (of ())⁻¹ * mk tl = mk ((PUnit.unit, false) :: tl)

Tactic:
rfl

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

Goal state before:
pp: case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () * mk tl = mk ((PUnit.unit, true) :: tl)

Tactic:
rfl

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

Goal state before:
pp: case succ
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℕ
hx : (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) ↑x) = ↑x
⊢ (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) (↑x + 1)) = ↑x + 1

Tactic:
| succ x hx =>

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

Goal state before:
pp: 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}

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ leftRel N = ⊤ ↔ N = ⊤

Tactic:
by
  simpa [leftRel, MulAction.orbitRel, funext_iff, MulAction.mem_orbit_iff,
    MulAction.subgroup_smul_def, ← eq_inv_mul_iff_mul_eq]
    using ⟨fun h ↦ by ext; simpa using h _ 1, fun h ↦ by simp [h]⟩

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

Goal state before:
pp: case mk
G : Type u_1
inst✝¹ : Group G
G' : Subgroup G
inst✝ : G'.Normal
he : Subgroup.map (↑(MulEquiv.refl G)) G' = G'
x✝ : G ⧸ G'
x : G
⊢ (congr G' G' (MulEquiv.refl G) he) (Quot.mk (⇑(leftRel G')) x) = (MulEquiv.refl (G ⧸ G')) (Quot.mk (⇑(leftRel G')) x)

Tactic:
rfl

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

Goal state before:
pp: case inr
ι : 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
hx' : g x hx ≠ x
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
grind

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

Goal state before:
pp: case mk
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : CommGroup H
x✝ : Abelianization H
a : H
⊢ of ((lift (MonoidHom.id H)) (Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a)) =
    Quot.mk (⇑(QuotientGroup.leftRel (commutator H))) a

Tactic:
rfl

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

Goal state before:
pp: case H.inr
ι : 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
⊢ ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}

Tactic:
grind

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
R : Setoid ι
inst✝ : DecidableRel ⇑R
x : ι
_hx : x ∈ s
⊢ ∏ y ∈ s with ⟦y⟧ = ⟦x⟧, f y = ∏ j ∈ s with ⟦j⟧ = ⟦x⟧, f j

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
⊢ x ∈ P → x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
intro hx₁

Goal state after:
case mpr
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
⊢ x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
hc0 : ¬#s = 0
h1 : ∃ a, s = {a}
⊢ f x = b

Tactic:
grind

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✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
x : ι
hx : x ∈ s
hnx : x ∉ s \ {a}
⊢ f x = 1

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
⊢ s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
hs : 1 ∈ ⊥
⊢ ↑⟨1, hs⟩ * x✝ = ↑⟨1, hs⟩ * x✝

Tactic:
rfl

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

Goal state before:
pp: R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ ↑s * m = ↑s * n

Tactic:
rw [mul_comm (s : R) n, mul_comm (s : R) m, h]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
hij : i ≠ j
a : Finset ι
hai : a ⊆ t' i
haj : a ⊆ t' j
k : ι
hk : k ∈ a
hki : k ∈ t i ∧ ¬f k = 1
hkj : k ∈ t j ∧ ¬f k = 1
⊢ k ∈ t i ∩ t j

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
h : ∀ j ∈ {i ∈ I | f i = f n}.erase n, g (f j) = 1
⊢ f n = f n

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a) + #(s.biUnion t) ≤ ∑ a ∈ insert a s, #(t a)

Tactic:
grind

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

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_4
a : M
m : ι → Multiset M
⊢ a ∈ ∑ i ∈ ∅, m i ↔ ∃ i ∈ ∅, a ∈ m i

Tactic:
grind

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_4
a : M
m : ι → Multiset M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : a ∈ ∑ i ∈ s✝, m i ↔ ∃ i ∈ s✝, a ∈ m i
⊢ a ∈ ∑ i ∈ Finset.cons a✝¹ s✝ h✝, m i ↔ ∃ i ∈ Finset.cons a✝¹ s✝ h✝, a ∈ m i

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : FreeAbelianGroup α
⊢ (AddMonoidHom.id (FreeAbelianGroup α)) x = x

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ((map g).comp (map f)) x = (map g) ((map f) x)

Tactic:
rfl

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

Goal state before:
pp: case empty
M : Type u_4
ι : Type u_5
inst✝ : CommMonoid M
f : ι → Multiset M
⊢ (∑ x ∈ ∅, f x).prod = ∏ x ∈ ∅, (f x).prod

Tactic:
grind

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

Goal state before:
pp: case cons
M : Type u_4
ι : Type u_5
inst✝ : CommMonoid M
f : ι → Multiset M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : (∑ x ∈ s✝, f x).prod = ∏ x ∈ s✝, (f x).prod
⊢ (∑ x ∈ Finset.cons a✝¹ s✝ h✝, f x).prod = ∏ x ∈ Finset.cons a✝¹ s✝ h✝, (f x).prod

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ ≤ H ↔ H.Normal

Tactic:
refine ⟨fun hle ↦ ⟨fun h hh g ↦ ?_⟩, fun h ↦ commutator_le_right ⊤ H⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hle : ⁅⊤, H⁆ ≤ H
h : G
hh : h ∈ H
g : G
⊢ g * h * g⁻¹ ∈ H
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
⊢ IsUnit (∏ a ∈ ∅, f a) ↔ ∀ a ∈ ∅, IsUnit (f a)

Tactic:
grind

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
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : IsUnit (∏ a ∈ s✝, f a) ↔ ∀ a ∈ s✝, IsUnit (f a)
⊢ IsUnit (∏ a ∈ Finset.cons a✝¹ s✝ h✝, f a) ↔ ∀ a ∈ Finset.cons a✝¹ s✝ h✝, IsUnit (f a)

Tactic:
grind

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

Goal state before:
pp: case empty
ι : Type u_1
f : ι → ℤ
⊢ (∑ i ∈ ∅, f i).natAbs ≤ ∑ i ∈ ∅, (f i).natAbs

Tactic:
grind

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

Goal state before:
pp: case cons
ι : Type u_1
f : ι → ℤ
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : (∑ i ∈ s✝, f i).natAbs ≤ ∑ i ∈ s✝, (f i).natAbs
⊢ (∑ i ∈ Finset.cons a✝¹ s✝ h✝, f i).natAbs ≤ ∑ i ∈ Finset.cons a✝¹ s✝ h✝, (f i).natAbs

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
⊢ (lift fun x₂ ↦ of (1 * x₂)) 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
⊢ (lift fun x₁ ↦ of (x₁ * 1)) 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case h₂
G : Type u_1
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)

Tactic:
exact fun g hg ↦
      ⟨_, ⟨⟨_, subset_closure <| .inl ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩,
          ⟨_, subset_closure <| .inr ⟨_, ⟨⟨g, hg⟩, rfl⟩, rfl⟩⟩, rfl⟩,
        hg.choose_spec.choose_spec⟩

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

Goal state before:
pp: case 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' u : ↥S
v : R
hru : u • (r', s').fst = v • (r, s).fst
hsu : ↑u * ↑(r', s').snd = v * ↑(r, s).snd
⊢ ∃ u v, u • (r, s).fst = v • (r', s').fst ∧ ↑u * ↑(r, s).snd = v * ↑(r', s').snd

Tactic:
dsimp only at *

Goal state after:
case 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' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
⊢ ∃ u v, u • r = v • r' ∧ ↑u * ↑s = v * ↑s'
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
F : FreeAbelianGroup α →+* R
⊢ ↑{ toFun := ⇑(lift ⇑((↑F).comp ofMulHom)), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } =
    lift (lift.symm ↑F)

Tactic:
rfl

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

Goal state before:
pp: case 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₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : ↑u * ↑(r₂, s₂).snd = v * ↑(r₁, s₁).snd
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : ↑u' * ↑(r₃, s₃).snd = v' * ↑(r₂, s₂).snd
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ∃ u v, u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ ↑u * ↑(r₃, s₃).snd = v * ↑(r₁, s₁).snd

Tactic:
dsimp only at *

Goal state after:
case 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
⊢ ∃ u v, u • r₃ = v • r₁ ∧ ↑u * ↑s₃ = v * ↑s₁
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk (m₁ * ↑s₂) (s₁ * ⟨m₂, ⋯⟩) = mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ { toMonoidHom := ↑f, monotone' := h } a✝ = f a✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ P (u • r₂) (u * s₂) = P (↑u • r₂) ⟨↑u * ↑s₂, ⋯⟩

Tactic:
rfl

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✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
⊢ g₁.trans f = g₁.trans f

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀o β
⊢ f.toMonoidWithZeroHom = MonoidWithZeroHom.ofClass f

Tactic:
rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀ β
hf : Monotone ⇑f
⊢ MonoidWithZeroHom.ofClass { toMonoidWithZeroHom := f, monotone' := hf } = f

Tactic:
rfl

Goal state after: