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

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).1 = (x✝ * x✝¹).1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).2 = (x✝ * x✝¹).2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).1 = (x✝ * x✝¹).1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMagma M
inst✝ : CommMagma N
x✝¹ x✝ : M × N
⊢ (x✝¹ * x✝).2 = (x✝ * x✝¹).2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ (x✝² * x✝¹ * x✝).1 = (x✝² * (x✝¹ * x✝)).1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ (x✝² * x✝¹ * x✝).2 = (x✝² * (x✝¹ * x✝)).2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ (x✝² * x✝¹ * x✝).1 = (x✝² * (x✝¹ * x✝)).1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Semigroup M
inst✝ : Semigroup N
x✝² x✝¹ x✝ : M × N
⊢ (x✝² * x✝¹ * x✝).2 = (x✝² * (x✝¹ * x✝)).2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (1 * x✝).1 = x✝.1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (1 * x✝).2 = x✝.2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (1 * x✝).1 = x✝.1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (1 * x✝).2 = x✝.2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (x✝ * 1).1 = x✝.1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (x✝ * 1).2 = x✝.2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (x✝ * 1).1 = x✝.1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ (x✝ * 1).2 = x✝.2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a.1 = b.1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a.2 = b.2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a.1 = b.1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : IsMulTorsionFree M
inst✝ : IsMulTorsionFree N
n : ℕ
hn : n ≠ 0
a b : M × N
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
⊢ a.2 = b.2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ x✝ : G × H
⊢ (x✝¹ / x✝).1 = (x✝¹ * x✝⁻¹).1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ x✝ : G × H
⊢ (x✝¹ / x✝).2 = (x✝¹ * x✝⁻¹).2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ x✝ : G × H
⊢ (x✝¹ / x✝).1 = (x✝¹ * x✝⁻¹).1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ x✝ : G × H
⊢ (x✝¹ / x✝).2 = (x✝¹ * x✝⁻¹).2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ (x✝ ^ 0).1 = 1.1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ (x✝ ^ 0).2 = 1.2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ (x✝ ^ 0).1 = 1.1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝ : G × H
⊢ (x✝ ^ 0).2 = 1.2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ ↑x✝¹.succ).1 = (x✝ ^ ↑x✝¹ * x✝).1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ ↑x✝¹.succ).2 = (x✝ ^ ↑x✝¹ * x✝).2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ ↑x✝¹.succ).1 = (x✝ ^ ↑x✝¹ * x✝).1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ ↑x✝¹.succ).2 = (x✝ ^ ↑x✝¹ * x✝).2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ Int.negSucc x✝¹).1 = (x✝ ^ ↑x✝¹.succ)⁻¹.1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ Int.negSucc x✝¹).2 = (x✝ ^ ↑x✝¹.succ)⁻¹.2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ Int.negSucc x✝¹).1 = (x✝ ^ ↑x✝¹.succ)⁻¹.1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivInvMonoid G
inst✝ : DivInvMonoid H
x✝¹ : ℕ
x✝ : G × H
⊢ (x✝ ^ Int.negSucc x✝¹).2 = (x✝ ^ ↑x✝¹.succ)⁻¹.2
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ (x✝⁻¹ * x✝).1 = 1.1

pp: case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ (x✝⁻¹ * x✝).2 = 1.2

Tactic:
<;>

Goal state after:
case fst
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ (x✝⁻¹ * x✝).1 = 1.1

case snd
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ (x✝⁻¹ * x✝).2 = 1.2
Module: Mathlib.Control.Basic

Goal state before:
pp: case map_const
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

pp: case id_map
α β γ : Type u
e : Type v
⊢ ∀ {α : Type u} (x : e ⊕ α), id <$> x = x

pp: case comp_map
α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : e ⊕ α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
<;>

Goal state after:
case map_const
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

case id_map
α β γ : Type u
e : Type v
⊢ ∀ {α : Type u} (x : e ⊕ α), id <$> x = x

case comp_map
α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : e ⊕ α), (h ∘ g) <$> x = h <$> g <$> x
Module: Mathlib.Control.Basic

Goal state before:
pp: case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

pp: case id_map
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝

pp: case comp_map
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝

Tactic:
<;>

Goal state after:
case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

case id_map
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝

case comp_map
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

pp: case id_map.inl
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e
⊢ id <$> inl x✝ = inl x✝

pp: case id_map.inr
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : α✝
⊢ id <$> inr x✝ = inr x✝

pp: case comp_map.inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e
⊢ (h✝ ∘ g✝) <$> inl x✝ = h✝ <$> g✝ <$> inl x✝

pp: case comp_map.inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : α✝
⊢ (h✝ ∘ g✝) <$> inr x✝ = h✝ <$> g✝ <$> inr x✝

Tactic:
<;>

Goal state after:
case map_const
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

case id_map.inl
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e
⊢ id <$> inl x✝ = inl x✝

case id_map.inr
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : α✝
⊢ id <$> inr x✝ = inr x✝

case comp_map.inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e
⊢ (h✝ ∘ g✝) <$> inl x✝ = h✝ <$> g✝ <$> inl x✝

case comp_map.inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : α✝
⊢ (h✝ ∘ g✝) <$> inr x✝ = h✝ <$> g✝ <$> inr x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : e
⊢ inl x✝ <* y✝ = Function.const β✝ <$> inl x✝ <*> y✝

pp: case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : α✝
⊢ inr x✝ <* y✝ = Function.const β✝ <$> inr x✝ <*> y✝

Tactic:
<;>

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : e
⊢ inl x✝ <* y✝ = Function.const β✝ <$> inl x✝ <*> y✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : α✝
⊢ inr x✝ <* y✝ = Function.const β✝ <$> inr x✝ <*> y✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : e
⊢ inl x✝ *> y✝ = Function.const α✝ id <$> inl x✝ <*> y✝

pp: case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : α✝
⊢ inr x✝ *> y✝ = Function.const α✝ id <$> inr x✝ <*> y✝

Tactic:
<;>

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : e
⊢ inl x✝ *> y✝ = Function.const α✝ id <$> inl x✝ <*> y✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
x✝ : α✝
⊢ inr x✝ *> y✝ = Function.const α✝ id <$> inr x✝ <*> y✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inl.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ y✝ : e
⊢ inl x✝ *> inl y✝ = Function.const α✝ id <$> inl x✝ <*> inl y✝

pp: case inl.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e
y✝ : β✝
⊢ inl x✝ *> inr y✝ = Function.const α✝ id <$> inl x✝ <*> inr y✝

pp: case inr.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
y✝ : e
⊢ inr x✝ *> inl y✝ = Function.const α✝ id <$> inr x✝ <*> inl y✝

pp: case inr.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
y✝ : β✝
⊢ inr x✝ *> inr y✝ = Function.const α✝ id <$> inr x✝ <*> inr y✝

Tactic:
<;>

Goal state after:
case inl.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ y✝ : e
⊢ inl x✝ *> inl y✝ = Function.const α✝ id <$> inl x✝ <*> inl y✝

case inl.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e
y✝ : β✝
⊢ inl x✝ *> inr y✝ = Function.const α✝ id <$> inl x✝ <*> inr y✝

case inr.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
y✝ : e
⊢ inr x✝ *> inl y✝ = Function.const α✝ id <$> inr x✝ <*> inl y✝

case inr.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
y✝ : β✝
⊢ inr x✝ *> inr y✝ = Function.const α✝ id <$> inr x✝ <*> inr y✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : e
⊢ (do
      let a ← inl x✝
      pure (f✝ a)) =
    f✝ <$> inl x✝

pp: case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : α✝
⊢ (do
      let a ← inr x✝
      pure (f✝ a)) =
    f✝ <$> inr x✝

Tactic:
<;>

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : e
⊢ (do
      let a ← inl x✝
      pure (f✝ a)) =
    f✝ <$> inl x✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : α✝
⊢ (do
      let a ← inr x✝
      pure (f✝ a)) =
    f✝ <$> inr x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
f✝ : e
⊢ (do
      let x ← inl f✝
      x <$> x✝) =
    inl f✝ <*> x✝

pp: case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
f✝ : α✝ → β✝
⊢ (do
      let x ← inr f✝
      x <$> x✝) =
    inr f✝ <*> x✝

Tactic:
<;>

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
f✝ : e
⊢ (do
      let x ← inl f✝
      x <$> x✝) =
    inl f✝ <*> x✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
f✝ : α✝ → β✝
⊢ (do
      let x ← inr f✝
      x <$> x✝) =
    inr f✝ <*> x✝
Module: Mathlib.Control.Basic

Goal state before:
pp: case inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
x✝ : e
⊢ inl x✝ >>= f✝ >>= g✝ = inl x✝ >>= fun x ↦ f✝ x >>= g✝

pp: case inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
x✝ : α✝
⊢ inr x✝ >>= f✝ >>= g✝ = inr x✝ >>= fun x ↦ f✝ x >>= g✝

Tactic:
<;>

Goal state after:
case inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
x✝ : e
⊢ inl x✝ >>= f✝ >>= g✝ = inl x✝ >>= fun x ↦ f✝ x >>= g✝

case inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
x✝ : α✝
⊢ inr x✝ >>= f✝ >>= g✝ = inr x✝ >>= fun x ↦ f✝ x >>= g✝
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsRightCancelMulZero M₀
a b c : M₀
⊢ a * c = b * c ↔ a = b ∨ c = 0

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsRightCancelMulZero M₀
a b c : M₀
hc : c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0

case neg
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : IsRightCancelMulZero M₀
a b c : M₀
hc : ¬c = 0
⊢ a * c = b * c ↔ a = b ∨ c = 0
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

pp: case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ snd✝¹ = snd✝

Tactic:
<;>

Goal state after:
case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
⊢ snd✝¹ = snd✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

pp: case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ snd✝¹ = snd✝

Tactic:
<;>

Goal state after:
case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ snd✝¹ = snd✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // p a }
⊢ ↑(fst✝¹ i) = ↑(fst✝ i)

pp: case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // ¬p a }
⊢ ↑(snd✝¹ i) = ↑(snd✝ i)

Tactic:
<;>

Goal state after:
case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // p a }
⊢ ↑(fst✝¹ i) = ↑(fst✝ i)

case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
i : { a // ¬p a }
⊢ ↑(snd✝¹ i) = ↑(snd✝ i)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : ¬a = 0
⊢ a * b = 0

Tactic:
by rw [h ha, mul_zero]

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

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝¹ : f z = x
h✝ : z = f⁻¹ x
⊢ y = f (f⁻¹ y)

pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ y = f (f⁻¹ x)

pp: case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ y = f z

pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : f z = y
h✝ : z = f⁻¹ x
⊢ x = f (f⁻¹ y)

pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ x = f (f⁻¹ x)

pp: case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ x = f z

pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : ¬f z = y
h✝ : z = f⁻¹ x
⊢ f z = f (f⁻¹ y)

pp: case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ f z = f (f⁻¹ x)

pp: case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ f z = f z

Tactic:
<;>

Goal state after:
case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝¹ : f z = x
h✝ : z = f⁻¹ x
⊢ y = f (f⁻¹ y)

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ y = f (f⁻¹ x)

case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : f z = x
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ y = f z

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : f z = y
h✝ : z = f⁻¹ x
⊢ x = f (f⁻¹ y)

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ x = f (f⁻¹ x)

case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ x = f z

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝² : ¬f z = x
h✝¹ : ¬f z = y
h✝ : z = f⁻¹ x
⊢ f z = f (f⁻¹ y)

case pos
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : z = f⁻¹ y
⊢ f z = f (f⁻¹ x)

case neg
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
h✝³ : ¬f z = x
h✝² : ¬f z = y
h✝¹ : ¬z = f⁻¹ x
h✝ : ¬z = f⁻¹ y
⊢ f z = f z
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case inl
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
a : M₀
inst✝¹ : IsReduced M₀
inst✝ : Nontrivial M₀
⊢ a ^ 0 = 0 ↔ a = 0 ∧ 0 ≠ 0

pp: case inr
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
a : M₀
n : ℕ
inst✝¹ : IsReduced M₀
inst✝ : Nontrivial M₀
hn : n ≠ 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Tactic:
<;>

Goal state after:
case inl
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
a : M₀
inst✝¹ : IsReduced M₀
inst✝ : Nontrivial M₀
⊢ a ^ 0 = 0 ↔ a = 0 ∧ 0 ≠ 0

case inr
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
a : M₀
n : ℕ
inst✝¹ : IsReduced M₀
inst✝ : Nontrivial M₀
hn : n ≠ 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 0 = 0

pp: case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 1 = 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 0 = 0

case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 1 = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsLeftCancelMulZero M₀
ha : a ≠ 0
⊢ a = a * b ↔ b = 1

Tactic:
rw [eq_comm, mul_eq_left₀ ha]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 1 = 1

pp: case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 0 = 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 1 = 1

case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 0 = 0