[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
src✝ : Inv (WithOne α) := inv
a : WithOne α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a
[PROOFSTEP]
simp_rw [inv_comp_inv, Option.map_id, id]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
src✝ : Inv (WithZero α) := inv
a : WithZero α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a
[PROOFSTEP]
simp_rw [inv_comp_inv, Option.map_id, id]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : InvOneClass α
src✝¹ : One (WithZero α) := one
src✝ : Inv (WithZero α) := inv
⊢ ↑1⁻¹ = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : DivisionMonoid α
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : InvolutiveInv (WithZero α) := involutiveInv
a b✝ : WithZero α
b : α
x✝ : none * some b = 1
⊢ none⁻¹ = some b
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : DivisionMonoid α
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : InvolutiveInv (WithZero α) := involutiveInv
a✝ b : WithZero α
a : α
x✝ : some a * none = 1
⊢ (some a)⁻¹ = none
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Group α
src✝² : MonoidWithZero (WithZero α) := monoidWithZero
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : Nontrivial (WithZero α) := nontrivial
a : WithZero α
ha : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
lift a to α using ha
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝ : Group α
src✝² : MonoidWithZero (WithZero α) := monoidWithZero
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : Nontrivial (WithZero α) := nontrivial
a : α
⊢ ↑a * (↑a)⁻¹ = 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝ : Group α
src✝² : MonoidWithZero (WithZero α) := monoidWithZero
src✝¹ : DivInvMonoid (WithZero α) := divInvMonoid
src✝ : Nontrivial (WithZero α) := nontrivial
a : α
⊢ a * a⁻¹ = 1
[PROOFSTEP]
apply mul_right_inv
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
cases n with
| zero => show (((1 : ℕ) : α) : WithZero α) = 0 + 1; · rw [Nat.cast_one, coe_one, zero_add]
| succ n =>
  show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
  rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
cases n with
| zero => show (((1 : ℕ) : α) : WithZero α) = 0 + 1; · rw [Nat.cast_one, coe_one, zero_add]
| succ n =>
  show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
  rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
⊢ NatCast.natCast (Nat.zero + 1) = NatCast.natCast Nat.zero + 1
[PROOFSTEP]

| zero => show (((1 : ℕ) : α) : WithZero α) = 0 + 1; · rw [Nat.cast_one, coe_one, zero_add]
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
⊢ NatCast.natCast (Nat.zero + 1) = NatCast.natCast Nat.zero + 1
[PROOFSTEP]
show (((1 : ℕ) : α) : WithZero α) = 0 + 1
[GOAL]
case zero
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
⊢ ↑↑1 = 0 + 1
[PROOFSTEP]
rw [Nat.cast_one, coe_one, zero_add]
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (Nat.succ n + 1) = NatCast.natCast (Nat.succ n) + 1
[PROOFSTEP]

| succ n =>
  show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
  rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ NatCast.natCast (Nat.succ n + 1) = NatCast.natCast (Nat.succ n) + 1
[PROOFSTEP]
show (((n + 2 : ℕ) : α) : WithZero α) = ((n + 1 : ℕ) : α) + 1
[GOAL]
case succ
α : Type u
β : Type v
γ : Type w
inst✝ : AddMonoidWithOne α
src✝¹ : AddMonoid (WithZero α) := addMonoid
src✝ : One (WithZero α) := one
n : ℕ
⊢ ↑↑(n + 2) = ↑↑(n + 1) + 1
[PROOFSTEP]
rw [Nat.cast_succ, coe_add, coe_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : WithZero α
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
cases' a with a
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b c : WithZero α
⊢ none * (b + c) = none * b + none * c
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b c : WithZero α
a : α
⊢ some a * (b + c) = some a * b + some a * c
[PROOFSTEP]
cases' b with b
[GOAL]
case some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : WithZero α
a : α
⊢ some a * (none + c) = some a * none + some a * c
[PROOFSTEP]
cases' c with c
[GOAL]
case some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : WithZero α
a b : α
⊢ some a * (some b + c) = some a * some b + some a * c
[PROOFSTEP]
cases' c with c
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a : α
⊢ some a * (none + none) = some a * none + some a * none
[PROOFSTEP]
try rfl
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a : α
⊢ some a * (none + none) = some a * none + some a * none
[PROOFSTEP]
rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a c : α
⊢ some a * (none + some c) = some a * none + some a * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a c : α
⊢ some a * (none + some c) = some a * none + some a * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : α
⊢ some a * (some b + none) = some a * some b + some a * none
[PROOFSTEP]
try rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : α
⊢ some a * (some b + none) = some a * some b + some a * none
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : α
⊢ some a * (some b + some c) = some a * some b + some a * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : α
⊢ some a * (some b + some c) = some a * some b + some a * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : α
⊢ some a * (some b + some c) = some a * some b + some a * some c
[PROOFSTEP]
exact congr_arg some (left_distrib _ _ _)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b c : WithZero α
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
cases' c with c
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : WithZero α
⊢ (a + b) * none = a * none + b * none
[PROOFSTEP]
change (a + b) * 0 = a * 0 + b * 0
[GOAL]
case none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : WithZero α
⊢ (a + b) * 0 = a * 0 + b * 0
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
a b : WithZero α
c : α
⊢ (a + b) * some c = a * some c + b * some c
[PROOFSTEP]
cases' a with a
[GOAL]
case some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b : WithZero α
c : α
⊢ (none + b) * some c = none * some c + b * some c
[PROOFSTEP]
cases' b with b
[GOAL]
case some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
b : WithZero α
c a : α
⊢ (some a + b) * some c = some a * some c + b * some c
[PROOFSTEP]
cases' b with b
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : α
⊢ (none + none) * some c = none * some c + none * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.none.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c : α
⊢ (none + none) * some c = none * some c + none * some c
[PROOFSTEP]
rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c b : α
⊢ (none + some b) * some c = none * some c + some b * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.none.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c b : α
⊢ (none + some b) * some c = none * some c + some b * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a : α
⊢ (some a + none) * some c = some a * some c + none * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.some.none
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a : α
⊢ (some a + none) * some c = some a * some c + none * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a b : α
⊢ (some a + some b) * some c = some a * some c + some b * some c
[PROOFSTEP]
try rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a b : α
⊢ (some a + some b) * some c = some a * some c + some b * some c
[PROOFSTEP]
rfl
[GOAL]
case some.some.some
α : Type u
β : Type v
γ : Type w
inst✝ : Semiring α
src✝³ : AddMonoidWithOne (WithZero α) := addMonoidWithOne
src✝² : AddCommMonoid (WithZero α) := addCommMonoid
src✝¹ : MulZeroClass (WithZero α) := mulZeroClass
src✝ : MonoidWithZero (WithZero α) := monoidWithZero
c a b : α
⊢ (some a + some b) * some c = some a * some c + some b * some c
[PROOFSTEP]
exact congr_arg some (right_distrib _ _ _)
