mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.MinimalAxioms

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ 1 * (a * a⁻¹) = 1 * (a * a⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a = 0 * a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
⊢ 0 * a + 0 * a = 0 * a + 0 * a

Tactic:
]

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0
⊢ 0 * a = 0

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
a : R
this : 0 * a = 0
⊢ 0 * a = 0
Module: Mathlib.Algebra.Group.MinimalAxioms

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 = a * 0

Tactic:
]

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * 1 = a⁻¹ * a * 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
⊢ a * 0 + a * 0 = a * 0 + a * 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = 0
⊢ a * 0 = 0

Tactic:
]

Goal state after:
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this✝ : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
add_comm : ∀ (a b : R), a + b = b + a
zero_mul : ∀ (a : R), 0 * a = 0
a : R
this : a * 0 = 0
⊢ a * 0 = 0
Module: Mathlib.Algebra.Group.MinimalAxioms

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
a : R
⊢ a = a

Tactic:
]

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
mul_one : ∀ (a : R), a * 1 = a
a b c : R
⊢ a * c + c * b = a * c + c * b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Field.ModEq

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c p : K
hc : c ≠ 0
⊢ a * c ≡ b * c [PMOD p] ↔ a * c ≡ b * c [PMOD p]

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' Icc (a + c) a = f '' Icc (a + c) a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ range f = range f

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocSemiring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (x + ↑n * c) = (-1) ^ n * f x

Tactic:
by
  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
    Int.cast_one] using h.add_nsmul_eq n

Goal state after:
Module: Mathlib.Algebra.Field.ZMod

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ¬↑k = 0

Tactic:
]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ¬↑k = 0
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ x * y = x * y

Tactic:
]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (List.replicate n x) [x] fun hd tl ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x

Tactic:
]

Goal state after:
case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (List.replicate n x) [x] fun hd tl ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeMagma α✝
f : α✝ → FreeMagma β✝
g : β✝ → FreeMagma γ✝
x y : FreeMagma α✝
ih1 : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ih2 : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) * (y >>= fun x ↦ f x >>= g) = (x >>= fun x ↦ f x >>= g) * (y >>= fun x ↦ f x >>= g)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ pure ((fun x2 ↦ x * x2) y) = pure (x * y)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g x <*> traverse g y))

Tactic:
]

Goal state after:
α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g x) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g x <*> traverse g y))
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ β✝ : Type u
f : α✝ → β✝
x✝ x y : FreeMagma α✝
ih1 : traverse (pure ∘ f) x = pure (f <$> x)
ih2 : traverse (pure ∘ f) y = pure (f <$> y)
⊢ pure ((fun x2 ↦ f <$> x * x2) (f <$> y)) = pure (f <$> x * f <$> y)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_1.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
a c d e f : α
⊢ Quot.mk (AssocRel α) (a * (c * (d * (e * f)))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: (L2 ++ (x', b') :: (x', !b') :: L3)
h : x = y ∧ b = !c
H : tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ p
Module: Mathlib.Algebra.Free

Goal state before:
pp: case refine_2.left
α : Type u
inst✝ : Mul α
x y : AssocQuotient α
b c d e f : α
⊢ Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * d * (e * (f * b)))

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
⊢ f x * (lift f) y = f x * (lift f) y

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : id <$> pure x = pure x
ih2 : id <$> y = y
⊢ pure x * y = pure x * y

Tactic:
]

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

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
]

Goal state after:
case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: (L2 ++ (x', b') :: (x', !b') :: L3)
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ L2 ++ (x', b') :: (x', !b') :: L3 = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ β✝ γ✝ : Type u
x✝ : FreeSemigroup α✝
g : α✝ → FreeSemigroup β✝
f : β✝ → FreeSemigroup γ✝
x : α✝
y : FreeSemigroup α✝
ih1 : pure x >>= g >>= f = pure x >>= fun x ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun x ↦ g x >>= f
⊢ (pure x >>= fun x ↦ g x >>= f) * (y >>= fun x ↦ g x >>= f) =
    (pure x >>= fun x ↦ g x >>= f) * (y >>= fun x ↦ g x >>= f)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 ↦ x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }

Tactic:
]

Goal state after:
α β : Type u
m : Type u → Type u
inst✝¹ : Applicative m
F : α → m β
inst✝ : LawfulApplicative m
x✝¹ y✝ : FreeSemigroup α
x✝ : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl } * { head := y, tail := L2 }) =
      (fun x1 x2 ↦ x1 * x2) <$> traverse F { head := x, tail := tl } <*> traverse F { head := y, tail := L2 }
x : α
⊢ (fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun x1 x2 ↦ x1 * x2) <$> traverse F { head := hd, tail := tl } <*> traverse F { head := y, tail := L2 }) =
    (fun x1 x2 ↦ x1 * x2) <$> ((fun x1 x2 ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 }
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
⊢ ∀ (a : M₃), i₃ a = 1 → a = 1

Tactic:
]

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
⊢ ∀ (a : M₃), i₃ a = 1 → a = 1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (mk x.toWord * mk y.toWord).toWord = reduce ((mk x.toWord).toWord ++ (mk y.toWord).toWord)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (mk x.toWord * mk y.toWord).toWord = reduce ((mk x.toWord).toWord ++ (mk y.toWord).toWord)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ pure ((fun x2 ↦ of x * x2) y) = pure (of x * y)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
n : ℕ
⊢ (mk x.toWord ^ n).toWord = reduce (List.replicate n (mk x.toWord).toWord).flatten
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
m : M₃
hm : i₃ m = 1
h : f₃ m = 1
⊢ f₃ m = 1

Tactic:
]

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
m : M₃
hm : i₃ m = 1
h : f₃ m = 1
⊢ f₃ m = 1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ Quot.lift reduce ⋯ (mk (List.replicate n (a, true))) = List.replicate n (a, true)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red w (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red w (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ invRev (reduce L) = invRev (reduce L)

Tactic:
]

Goal state after: