mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case h₁
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (H i) ≤ pi Set.univ H

Tactic:
rw [le_pi_iff]

Goal state after:
case h₁
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ i_1 ∈ Set.univ, map (MonoidHom.mulSingle Gs i) (H i) ≤ comap (Pi.evalMonoidHom Gs i_1) (H i_1)
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)

Tactic:
simp [h, one_mem]

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

Goal state before:
pp: case h₂
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (K i) ≤ pi Set.univ K

Tactic:
rw [le_pi_iff]

Goal state after:
case h₂
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ i_1 ∈ Set.univ, map (MonoidHom.mulSingle Gs i) (K i) ≤ comap (Pi.evalMonoidHom Gs i_1) (K i_1)
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)

Tactic:
simp [h, one_mem]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : x = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

pp: case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
<;>

Goal state after:
case pos
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : x = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
⊢ e.toFun (x * y) = e.toFun x * e.toFun y
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r.r.r
n : ℕ
a b c : ZMod n
⊢ r a * r b * r c = r a * (r b * r c)

pp: case r.r.sr
n : ℕ
a b c : ZMod n
⊢ r a * r b * sr c = r a * (r b * sr c)

pp: case r.sr.r
n : ℕ
a b c : ZMod n
⊢ r a * sr b * r c = r a * (sr b * r c)

pp: case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r a * sr b * sr c = r a * (sr b * sr c)

pp: case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr a * r b * r c = sr a * (r b * r c)

pp: case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ sr a * r b * sr c = sr a * (r b * sr c)

pp: case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * r c = sr a * (sr b * r c)

pp: case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * sr c = sr a * (sr b * sr c)

Tactic:
<;>

Goal state after:
case r.r.r
n : ℕ
a b c : ZMod n
⊢ r a * r b * r c = r a * (r b * r c)

case r.r.sr
n : ℕ
a b c : ZMod n
⊢ r a * r b * sr c = r a * (r b * sr c)

case r.sr.r
n : ℕ
a b c : ZMod n
⊢ r a * sr b * r c = r a * (sr b * r c)

case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r a * sr b * sr c = r a * (sr b * sr c)

case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr a * r b * r c = sr a * (r b * r c)

case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ sr a * r b * sr c = sr a * (r b * sr c)

case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * r c = sr a * (sr b * r c)

case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * sr c = sr a * (sr b * sr c)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r.r.r
n : ℕ
a b c : ZMod n
⊢ r (a + b + c) = r (a + (b + c))

pp: case r.r.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (a + b)) = sr (c - b - a)

pp: case r.sr.r
n : ℕ
a b c : ZMod n
⊢ sr (b - a + c) = sr (b + c - a)

pp: case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (b - a)) = r (a + (c - b))

pp: case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr (a + b + c) = sr (a + (b + c))

pp: case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (a + b)) = r (c - b - a)

pp: case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ r (b - a + c) = r (b + c - a)

pp: case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (b - a)) = sr (a + (c - b))

Tactic:
<;>

Goal state after:
case r.r.r
n : ℕ
a b c : ZMod n
⊢ r (a + b + c) = r (a + (b + c))

case r.r.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (a + b)) = sr (c - b - a)

case r.sr.r
n : ℕ
a b c : ZMod n
⊢ sr (b - a + c) = sr (b + c - a)

case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (b - a)) = r (a + (c - b))

case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr (a + b + c) = sr (a + (b + c))

case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (a + b)) = r (c - b - a)

case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ r (b - a + c) = r (b + c - a)

case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (b - a)) = sr (a + (c - b))
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case ofNat
n : ℕ
i : ZMod n
a✝ : ℕ
⊢ r i ^ Int.ofNat a✝ = r (i * ↑(Int.ofNat a✝))

pp: case negSucc
n : ℕ
i : ZMod n
a✝ : ℕ
⊢ r i ^ Int.negSucc a✝ = r (i * ↑(Int.negSucc a✝))

Tactic:
<;>

Goal state after:
case ofNat
n : ℕ
i : ZMod n
a✝ : ℕ
⊢ r i ^ Int.ofNat a✝ = r (i * ↑(Int.ofNat a✝))

case negSucc
n : ℕ
i : ZMod n
a✝ : ℕ
⊢ r i ^ Int.negSucc a✝ = r (i * ↑(Int.negSucc a✝))
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case ofNat
n : ℕ
i : ZMod n
a✝ : ℕ
⊢ r i ^ Int.ofNat a✝ = r (i * ↑(Int.ofNat a✝))

Tactic:
simp [r_pow, neg_mul_eq_mul_neg]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case negSucc
n : ℕ
i : ZMod n
a✝ : ℕ
⊢ r i ^ Int.negSucc a✝ = r (i * ↑(Int.negSucc a✝))

Tactic:
simp [r_pow, neg_mul_eq_mul_neg]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun x ↦
          match x with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (r x)) =
    r x

pp: case sr
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun x ↦
          match x with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (sr x)) =
    sr x

Tactic:
<;>

Goal state after:
case r
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun x ↦
          match x with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (r x)) =
    r x

case sr
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun x ↦
          match x with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (sr x)) =
    sr x
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inl x)) =
    Sum.inl x

pp: case inr
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inr x)) =
    Sum.inr x

Tactic:
<;>

Goal state after:
case inl
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inl x)) =
    Sum.inl x

case inr
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inr x)) =
    Sum.inr x
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
⊢ IsMulCommutative (DihedralGroup 1)

pp: case inr
⊢ IsMulCommutative (DihedralGroup 2)

Tactic:
<;>

Goal state after:
case inl
⊢ IsMulCommutative (DihedralGroup 1)

case inr
⊢ IsMulCommutative (DihedralGroup 2)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ {x | Commute x.1 x.2} = Set.univ ↔ IsMulCommutative M

pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0

Tactic:
Set.eq_univ_iff_forall

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.1 x.2}) ↔ IsMulCommutative M

M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ 0 = ↑(Nat.card (ConjClasses G)) / 0

Tactic:
div_zero

Goal state after:
case pos
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ 0 = 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Function.Injective fun p ↦ ⟨(↑(↑p).1, ↑(↑p).2), ⋯⟩

Tactic:
exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
n : ℕ
h0 : n = 0
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
h0,

Goal state after:
case pos
n : ℕ
h0 : n = 0
⊢ commProb (Product (reciprocalFactors 0)) = 1 / ↑0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
n : ℕ
h0 : n = 0
⊢ commProb (DihedralGroup 0) = 1 / 0

Tactic:
div_zero

Goal state after:
case pos
n : ℕ
h0 : n = 0
⊢ commProb (DihedralGroup 0) = 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ (↑(n % 4 * n) + 3) * 1 * ↑n = 1 * (4 * ↑(n % 4 * n) * ↑(n / 4 + 1))

pp: case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ 4 * ↑(n % 4 * n) * ↑(n / 4 + 1) ≠ 0

pp: case neg.inr.hd
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ ↑n ≠ 0

Tactic:
<;>

Goal state after:
case neg.inr
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ (↑(n % 4 * n) + 3) * 1 * ↑n = 1 * (4 * ↑(n % 4 * n) * ↑(n / 4 + 1))

case neg.inr.hb
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ 4 * ↑(n % 4 * n) * ↑(n / 4 + 1) ≠ 0

case neg.inr.hd
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
hn : Odd (n % 4)
⊢ ↑n ≠ 0
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case h₁
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inl = toProd.comp inl

pp: case h₂
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inr = toProd.comp inr

Tactic:
<;>

Goal state after:
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inl = toProd.comp inl

case h₂
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inr = toProd.comp inr
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case h₁
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : M
⊢ (((Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e')).comp inl) x✝ = ((MonoidHom.id (M ∗ M')).comp inl) x✝

pp: case h₂
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : M'
⊢ (((Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e')).comp inr) x✝ = ((MonoidHom.id (M ∗ M')).comp inr) x✝

Tactic:
<;>

Goal state after:
case h₁
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : M
⊢ (((Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e')).comp inl) x✝ = ((MonoidHom.id (M ∗ M')).comp inl) x✝

case h₂
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : M'
⊢ (((Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e')).comp inr) x✝ = ((MonoidHom.id (M ∗ M')).comp inr) x✝
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case h₁
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : N
⊢ (((Coprod.map ↑e ↑e').comp (Coprod.map ↑e.symm ↑e'.symm)).comp inl) x✝ = ((MonoidHom.id (N ∗ N')).comp inl) x✝

pp: case h₂
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : N'
⊢ (((Coprod.map ↑e ↑e').comp (Coprod.map ↑e.symm ↑e'.symm)).comp inr) x✝ = ((MonoidHom.id (N ∗ N')).comp inr) x✝

Tactic:
<;>

Goal state after:
case h₁
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : N
⊢ (((Coprod.map ↑e ↑e').comp (Coprod.map ↑e.symm ↑e'.symm)).comp inl) x✝ = ((MonoidHom.id (N ∗ N')).comp inl) x✝

case h₂
M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
x✝ : N'
⊢ (((Coprod.map ↑e ↑e').comp (Coprod.map ↑e.symm ↑e'.symm)).comp inr) x✝ = ((MonoidHom.id (N ∗ N')).comp inr) x✝
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case h₁.h₁
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : M
⊢ ((((Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr))).comp
            inl).comp
        inl)
      x✝ =
    (((MonoidHom.id ((M ∗ N) ∗ P)).comp inl).comp inl) x✝

pp: case h₁.h₂
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : N
⊢ ((((Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr))).comp
            inl).comp
        inr)
      x✝ =
    (((MonoidHom.id ((M ∗ N) ∗ P)).comp inl).comp inr) x✝

pp: case h₂
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : P
⊢ (((Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
            (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr))).comp
        inr)
      x✝ =
    ((MonoidHom.id ((M ∗ N) ∗ P)).comp inr) x✝

Tactic:
<;>

Goal state after:
case h₁.h₁
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : M
⊢ ((((Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr))).comp
            inl).comp
        inl)
      x✝ =
    (((MonoidHom.id ((M ∗ N) ∗ P)).comp inl).comp inl) x✝

case h₁.h₂
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : N
⊢ ((((Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
                (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr))).comp
            inl).comp
        inr)
      x✝ =
    (((MonoidHom.id ((M ∗ N) ∗ P)).comp inl).comp inr) x✝

case h₂
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : P
⊢ (((Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
            (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr))).comp
        inr)
      x✝ =
    ((MonoidHom.id ((M ∗ N) ∗ P)).comp inr) x✝
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: case h₁
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : M
⊢ (((Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
            (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P)))).comp
        inl)
      x✝ =
    ((MonoidHom.id (M ∗ (N ∗ P))).comp inl) x✝

pp: case h₂.h₁
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : N
⊢ ((((Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
                (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P)))).comp
            inr).comp
        inl)
      x✝ =
    (((MonoidHom.id (M ∗ (N ∗ P))).comp inr).comp inl) x✝

pp: case h₂.h₂
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : P
⊢ ((((Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
                (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P)))).comp
            inr).comp
        inr)
      x✝ =
    (((MonoidHom.id (M ∗ (N ∗ P))).comp inr).comp inr) x✝

Tactic:
<;>

Goal state after:
case h₁
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : M
⊢ (((Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
            (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P)))).comp
        inl)
      x✝ =
    ((MonoidHom.id (M ∗ (N ∗ P))).comp inl) x✝

case h₂.h₁
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : N
⊢ ((((Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
                (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P)))).comp
            inr).comp
        inl)
      x✝ =
    (((MonoidHom.id (M ∗ (N ∗ P))).comp inr).comp inl) x✝

case h₂.h₂
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
x✝ : P
⊢ ((((Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
                (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P)))).comp
            inr).comp
        inr)
      x✝ =
    (((MonoidHom.id (M ∗ (N ∗ P))).comp inr).comp inr) x✝
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup α
hr : r ∈ rels₁
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) ((FreeGroup.map Sum.inl) r) = 1

pp: case inr
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup β
hr : r ∈ rels₂
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) ((FreeGroup.map Sum.inr) r) = 1

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup α
hr : r ∈ rels₁
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) ((FreeGroup.map Sum.inl) r) = 1

case inr
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup β
hr : r ∈ rels₂
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) ((FreeGroup.map Sum.inr) r) = 1
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of_one
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
fi : (i : ι) → M i →* N
i : ι
⊢ (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) (FreeMonoid.of ⟨i, 1⟩) = (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) 1

pp: case of_mul
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
fi : (i : ι) → M i →* N
i✝ : ι
x y : M i✝
⊢ (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) (FreeMonoid.of ⟨i✝, x⟩ * FreeMonoid.of ⟨i✝, y⟩) =
    (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) (FreeMonoid.of ⟨i✝, x * y⟩)

Tactic:
<;>

Goal state after:
case of_one
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
fi : (i : ι) → M i →* N
i : ι
⊢ (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) (FreeMonoid.of ⟨i, 1⟩) = (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) 1

case of_mul
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
fi : (i : ι) → M i →* N
i✝ : ι
x y : M i✝
⊢ (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) (FreeMonoid.of ⟨i✝, x⟩ * FreeMonoid.of ⟨i✝, y⟩) =
    (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) (FreeMonoid.of ⟨i✝, x * y⟩)
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ (Units.coeHom G) (restrictUnit ⋯ i) = ↑f i

Tactic:
Units.coeHom_apply,

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
f : { f // M.IsLiftable f }
i : B
⊢ ↑(restrictUnit ⋯ i) = ↑f i
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : m = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : m = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

case neg
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }