mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ (a + a_n / ↑q.succ * ↑q.succ) * ↑p.succ + b_n * ↑q.succ = ↑n

Tactic:
Int.emod_add_ediv_mul,

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
⊢ a_n * ↑p.succ + b_n * ↑q.succ = ↑n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case ofNat
M : Type u_1
inst✝ : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1

pp: case negSucc
M : Type u_1
inst✝ : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1

Tactic:
<;>

Goal state after:
case ofNat
M : Type u_1
inst✝ : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.ofNat m).gcd n = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ n = 1

case negSucc
M : Type u_1
inst✝ : Group M
a : M
n : ℤ
m : ℕ
⊢ a ^ (Int.negSucc m).gcd n = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ n = 1
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case ha
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ 0 ≤ ↑p.succ

pp: case hbc
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ a ≤ ↑q

pp: case ha
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ 0 ≤ ↑q.succ

Tactic:
<;>

Goal state after:
case ha
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ 0 ≤ ↑p.succ

case hbc
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ a ≤ ↑q

case ha
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := ⋯
b : ℤ := ⋯
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ 0 ≤ ↑q.succ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case ofNat.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1

pp: case ofNat.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1

pp: case negSucc.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1

pp: case negSucc.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1

Tactic:
<;>

Goal state after:
case ofNat.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1

case ofNat.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1

case negSucc.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1

case negSucc.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : b = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m

Tactic:
· exact ⟨0, by simp_all⟩

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
⊢ ∃ c, a = c ^ n ∧ b = c ^ m
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

pp: case neg.refine_2
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m

Tactic:
<;>

Goal state after:
case neg.refine_1
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ a = (a ^ m.gcdB n * b ^ m.gcdA n) ^ n

case neg.refine_2
α : Type u_1
inst✝ : GroupWithZero α
a b : α
m n : ℕ
hab : Commute a b
hmn : m.Coprime n
h : a ^ m = b ^ n
h✝¹ : ¬m = 0
h✝ : ¬n = 0
hb : ¬b = 0
ha : ¬a = 0
⊢ b = (a ^ m.gcdB n * b ^ m.gcdA n) ^ m
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: case none
α β γ : Type u
f : α → β → γ
b : Option β
⊢ map₂ f none b = f <$> none <*> b

pp: case some
α β γ : Type u
f : α → β → γ
b : Option β
val✝ : α
⊢ map₂ f (some val✝) b = f <$> some val✝ <*> b

Tactic:
<;>

Goal state after:
case none
α β γ : Type u
f : α → β → γ
b : Option β
⊢ map₂ f none b = f <$> none <*> b

case some
α β γ : Type u
f : α → β → γ
b : Option β
val✝ : α
⊢ map₂ f (some val✝) b = f <$> some val✝ <*> b
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f none none = none

pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
val✝ : α
⊢ map₂ f (some val✝) none = none

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f none none = none

case some
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
val✝ : α
⊢ map₂ f (some val✝) none = none
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f 1 1 = 1

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a✝ : α
⊢ map₂ f (↑a✝) 1 = 1

Tactic:
<;>

Goal state after:
case one
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f 1 1 = 1

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a✝ : α
⊢ map₂ f (↑a✝) 1 = 1
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f 1 ↑b = map (fun x ↦ f x b) 1

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a✝ : α
⊢ map₂ f ↑a✝ ↑b = map (fun x ↦ f x b) ↑a✝

Tactic:
<;>

Goal state after:
case one
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f 1 ↑b = map (fun x ↦ f x b) 1

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a✝ : α
⊢ map₂ f ↑a✝ ↑b = map (fun x ↦ f x b) ↑a✝
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: case one
α : Type u
d y : α
⊢ unoneD d 1 = y ↔ 1 = ↑y ∨ 1 = 1 ∧ y = d

pp: case coe
α : Type u
d y a✝ : α
⊢ unoneD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = 1 ∧ y = d

Tactic:
<;>

Goal state after:
case one
α : Type u
d y : α
⊢ unoneD d 1 = y ↔ 1 = ↑y ∨ 1 = 1 ∧ y = d

case coe
α : Type u
d y a✝ : α
⊢ unoneD d ↑a✝ = y ↔ ↑a✝ = ↑y ∨ ↑a✝ = 1 ∧ y = d
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: case one
α : Type u
d : α
x : WithOne α
⊢ unoneD d x = unoneD d 1 ↔ x = 1 ∨ x = ↑d ∧ 1 = 1 ∨ x = 1 ∧ 1 = ↑d

pp: case coe
α : Type u
d : α
x : WithOne α
a✝ : α
⊢ unoneD d x = unoneD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = 1 ∨ x = 1 ∧ ↑a✝ = ↑d

Tactic:
<;>

Goal state after:
case one
α : Type u
d : α
x : WithOne α
⊢ unoneD d x = unoneD d 1 ↔ x = 1 ∨ x = ↑d ∧ 1 = 1 ∨ x = 1 ∧ 1 = ↑d

case coe
α : Type u
d : α
x : WithOne α
a✝ : α
⊢ unoneD d x = unoneD d ↑a✝ ↔ x = ↑a✝ ∨ x = ↑d ∧ ↑a✝ = 1 ∨ x = 1 ∧ ↑a✝ = ↑d
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case bot
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
⊢ ⊥ < 0 ↔ ⊥ = ⊥

pp: case coe
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
⊢ ↑a✝ < 0 ↔ ↑a✝ = ⊥

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
⊢ ⊥ < 0 ↔ ⊥ = ⊥

case coe
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
⊢ ↑a✝ < 0 ↔ ↑a✝ = ⊥
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) 0 = (MonoidHom.id (WithZero β)) 0

pp: case coe
β : Type u_2
inst✝ : MulOneClass β
a✝ : β
⊢ ↑(map' (MonoidHom.id β)) ↑a✝ = (MonoidHom.id (WithZero β)) ↑a✝

Tactic:
<;>

Goal state after:
case zero
β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) 0 = (MonoidHom.id (WithZero β)) 0

case coe
β : Type u_2
inst✝ : MulOneClass β
a✝ : β
⊢ ↑(map' (MonoidHom.id β)) ↑a✝ = (MonoidHom.id (WithZero β)) ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
⊢ (map' g) ((map' f) 0) = (map' (g.comp f)) 0

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
a✝ : α
⊢ (map' g) ((map' f) ↑a✝) = (map' (g.comp f)) ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
⊢ (map' g) ((map' f) 0) = (map' (g.comp f)) 0

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
a✝ : α
⊢ (map' g) ((map' f) ↑a✝) = (map' (g.comp f)) ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case refine_1.zero
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
hab : (map' f) 0 = ↑b
⊢ ∃ a, f a = b

pp: case refine_1.coe
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a✝ : α
hab : (map' f) ↑a✝ = ↑b
⊢ ∃ a, f a = b

Tactic:
<;>

Goal state after:
case refine_1.zero
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
hab : (map' f) 0 = ↑b
⊢ ∃ a, f a = b

case refine_1.coe
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a✝ : α
hab : (map' f) ↑a✝ = ↑b
⊢ ∃ a, f a = b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr.hba
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a + -a = 0

pp: case inr.hac
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
<;>

Goal state after:
case inr.hba
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ - -a + -a = 0

case inr.hac
G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
ha : a ≠ ⊤
⊢ -a + a = 0
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
⊢ (fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) ((fun n ↦ recZeroCoe 0 Units.val n) 0) = 0

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : Gˣ
⊢ (fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) ((fun n ↦ recZeroCoe 0 Units.val n) ↑a✝) = ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
⊢ (fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) ((fun n ↦ recZeroCoe 0 Units.val n) 0) = 0

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : Gˣ
⊢ (fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) ((fun n ↦ recZeroCoe 0 Units.val n) ↑a✝) = ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
h✝ : x✝ = 0
⊢ recZeroCoe 0 Units.val 0 = x✝

pp: case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
h✝ : ¬x✝ = 0
⊢ recZeroCoe 0 Units.val ↑(Units.mk0 x✝ h✝) = x✝

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
h✝ : x✝ = 0
⊢ recZeroCoe 0 Units.val 0 = x✝

case isFalse
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
h✝ : ¬x✝ = 0
⊢ recZeroCoe 0 Units.val ↑(Units.mk0 x✝ h✝) = x✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x2✝ : WithZero Gˣ
⊢ recZeroCoe 0 Units.val (0 * x2✝) = recZeroCoe 0 Units.val 0 * recZeroCoe 0 Units.val x2✝

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x2✝ : WithZero Gˣ
a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (↑a✝ * x2✝) = recZeroCoe 0 Units.val ↑a✝ * recZeroCoe 0 Units.val x2✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x2✝ : WithZero Gˣ
⊢ recZeroCoe 0 Units.val (0 * x2✝) = recZeroCoe 0 Units.val 0 * recZeroCoe 0 Units.val x2✝

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x2✝ : WithZero Gˣ
a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (↑a✝ * x2✝) = recZeroCoe 0 Units.val ↑a✝ * recZeroCoe 0 Units.val x2✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
⊢ recZeroCoe 0 Units.val (0 * 0) = recZeroCoe 0 Units.val 0 * recZeroCoe 0 Units.val 0

pp: case zero.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (0 * ↑a✝) = recZeroCoe 0 Units.val 0 * recZeroCoe 0 Units.val ↑a✝

pp: case coe.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (↑a✝ * 0) = recZeroCoe 0 Units.val ↑a✝ * recZeroCoe 0 Units.val 0

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝¹ a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (↑a✝¹ * ↑a✝) = recZeroCoe 0 Units.val ↑a✝¹ * recZeroCoe 0 Units.val ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
⊢ recZeroCoe 0 Units.val (0 * 0) = recZeroCoe 0 Units.val 0 * recZeroCoe 0 Units.val 0

case zero.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (0 * ↑a✝) = recZeroCoe 0 Units.val 0 * recZeroCoe 0 Units.val ↑a✝

case coe.zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (↑a✝ * 0) = recZeroCoe 0 Units.val ↑a✝ * recZeroCoe 0 Units.val 0

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a✝¹ a✝ : Gˣ
⊢ recZeroCoe 0 Units.val (↑a✝¹ * ↑a✝) = recZeroCoe 0 Units.val ↑a✝¹ * recZeroCoe 0 Units.val ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
⊢ (map' ↑e.symm) ((map' ↑e) 0) = 0

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : α
⊢ (map' ↑e.symm) ((map' ↑e) ↑a✝) = ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
⊢ (map' ↑e.symm) ((map' ↑e) 0) = 0

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : α
⊢ (map' ↑e.symm) ((map' ↑e) ↑a✝) = ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
⊢ (map' ↑e) ((map' ↑e.symm) 0) = 0

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : β
⊢ (map' ↑e) ((map' ↑e.symm) ↑a✝) = ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
⊢ (map' ↑e) ((map' ↑e.symm) 0) = 0

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
a✝ : β
⊢ (map' ↑e) ((map' ↑e.symm) ↑a✝) = ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
x2✝ : WithZero α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (0 * x2✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0 *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun x2✝

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
x2✝ : WithZero α
a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (↑a✝ * x2✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝ *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun x2✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
x2✝ : WithZero α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (0 * x2✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun 0 *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun x2✝

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
x2✝ : WithZero α
a✝ : α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (↑a✝ * x2✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun ↑a✝ *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun x2✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      0 =
    x✝ 0

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
a✝ : α
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      ↑a✝ =
    x✝ ↑a✝

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      0 =
    x✝ 0

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
a✝ : α
⊢ ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        ((fun e ↦
            { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          x✝))
      ↑a✝ =
    x✝ ↑a✝
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
⊢ (if 0 + 1 = 0 then 0 else ↑↑(0 + 1)) = (if 0 = 0 then 0 else ↑↑0) + 1

pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
n✝ : ℕ
⊢ (if n✝ + 1 + 1 = 0 then 0 else ↑↑(n✝ + 1 + 1)) = (if n✝ + 1 = 0 then 0 else ↑↑(n✝ + 1)) + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
⊢ (if 0 + 1 = 0 then 0 else ↑↑(0 + 1)) = (if 0 = 0 then 0 else ↑↑0) + 1

case succ
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
n✝ : ℕ
⊢ (if n✝ + 1 + 1 = 0 then 0 else ↑↑(n✝ + 1 + 1)) = (if n✝ + 1 = 0 then 0 else ↑↑(n✝ + 1)) + 1
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤

pp: case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤

Tactic:
<;>

Goal state after:
case top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤

case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤

pp: case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ↑a✝ - ⊤ = ⊤

Tactic:
<;>

Goal state after:
case top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤

case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ↑a✝ - ⊤ = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
⊢ ⊤ - y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

pp: case coe
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
a✝ : G
⊢ ↑a✝ - y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤

Tactic:
<;>

Goal state after:
case top
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
⊢ ⊤ - y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

case coe
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
a✝ : G
⊢ ↑a✝ - y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤