awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Div α
a b : α
⊢ (↑(a / b) : WithZero α) = (↑a : WithZero α) / (↑b : WithZero α)

Tactic:
rfl

Premises used: WithZero.coe, rfl, Option.map₂
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : One α
inst_1 : Pow α ℤ
a : α
n : ℤ
⊢ (↑(a ^ n) : WithZero α) = (↑a : WithZero α) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DivInvMonoid α
n : ℕ
change : HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n.succ : ℤ) = HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n : ℤ) * 0
⊢ HPow.hPow (α := WithZero α) (β := ℤ) none (↑n.succ : ℤ) = HPow.hPow (α := WithZero α) (β := ℤ) none (↑n : ℤ) * none

Tactic:
change 0 ^ _ = 0 ^ _ * 0
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DivInvMonoid α
n : ℕ
simp : HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n.succ : ℤ) = 0
⊢ HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n.succ : ℤ) = HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n : ℤ) * 0

Tactic:
simp only [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DivInvMonoid α
n : ℕ
⊢ HPow.hPow (α := WithZero α) (β := ℤ) 0 (↑n.succ : ℤ) = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : InvolutiveInv α
a : WithZero α
⊢ Option.map ((fun (x : α) ↦ x⁻¹) ∘ fun (x : α) ↦ x⁻¹) a = a

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
a : WithZero α
ha : a ≠ 0
⊢ a ≠ 0

Tactic:
ha
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
a : WithZero α
ha : a ≠ 0
lift : ∀ (a : α), (↑a : WithZero α) * (↑a : WithZero α)⁻¹ = 1
⊢ a * a⁻¹ = 1

Tactic:
lift a to α using ha
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
a : α
norm_cast : a * a⁻¹ = 1
⊢ (↑a : WithZero α) * (↑a : WithZero α)⁻¹ = 1

Tactic:
norm_cast
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
a : α
⊢ a * a⁻¹ = 1

Tactic:
apply mul_inv_cancel

Premises used: mul_inv_cancel
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
x : (WithZero α)ˣ
⊢ (↑((fun (a : α) ↦ (Units.mk0 (↑a : WithZero α) ⋯ : (WithZero α)ˣ)) ((fun (a : (WithZero α)ˣ) ↦ unzero ⋯) x)) :
      WithZero α) =
    (↑x : WithZero α)

Tactic:
simp only [coe_unzero, Units.mk0_val]

Premises used: WithZero.coe_unzero, Units.mk0_val
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
x x_1 : (WithZero α)ˣ
⊢ (↑(unzero ⋯) : WithZero α) = (↑(unzero ⋯ * unzero ⋯) : WithZero α)

Tactic:
simp only [Units.val_mul, coe_unzero, coe_mul]

Premises used: WithZero.coe_unzero, WithZero.coe_mul, Units.val_mul
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Nontrivial α
⊢ Nontrivial.{u_1} (WithZero α)ˣ

Tactic:
unitsWithZeroEquiv.toEquiv.surjective.nontrivial

Premises used: Function.Surjective.nontrivial, MulEquiv.toEquiv, WithZero.unitsWithZeroEquiv, Equiv.surjective
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
inst : Group α
γ : (WithZero α)ˣ
⊢ (↑((unitsWithZeroEquiv : (a : (WithZero α)ˣ) → α) γ) : WithZero α) = (↑γ : WithZero α)

Tactic:
simp only [WithZero.unitsWithZeroEquiv, MulEquiv.coe_mk, Equiv.coe_fn_mk, WithZero.coe_unzero]

Premises used: WithZero.coe_unzero, MulEquiv.coe_mk, WithZero.unitsWithZeroEquiv, Equiv.coe_fn_mk
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
G : Type u_4
inst_1 : GroupWithZero G
inst_2 : DecidablePred fun (a : G) ↦ a = 0
x : G
simp :
  recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val
      (if h : x = 0 then 0 else (↑(Units.mk0 x h) : WithZero Gˣ)) =
    x
⊢ (fun (n : WithZero Gˣ) ↦ (recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val n : G))
      ((fun (a : G) ↦ (if h : a = 0 then 0 else (↑(Units.mk0 a h) : WithZero Gˣ) : WithZero Gˣ)) x) =
    x

Tactic:
simp only
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
G : Type u_4
inst_1 : GroupWithZero G
inst_2 : DecidablePred fun (a : G) ↦ a = 0
x : G
isTrue : x = 0 → recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val 0 = x
isFalse :
  ∀ (h : ¬x = 0), recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val (↑(Units.mk0 x h) : WithZero Gˣ) = x
⊢ recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val
      (if h : x = 0 then 0 else (↑(Units.mk0 x h) : WithZero Gˣ)) =
    x

Tactic:
split
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
G : Type u_4
inst_1 : GroupWithZero G
inst_2 : DecidablePred fun (a : G) ↦ a = 0
x : G
h : x = 0
⊢ recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val 0 = x

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
G : Type u_4
inst_1 : GroupWithZero G
inst_2 : DecidablePred fun (a : G) ↦ a = 0
x : G
h : ¬x = 0
⊢ recZeroCoe (motive := fun (x : WithZero Gˣ) ↦ G) 0 Units.val (↑(Units.mk0 x h) : WithZero Gˣ) = x

Tactic:
simp_all
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_4
inst : GroupWithZero G
inst_1 : DecidablePred fun (a : G) ↦ a = 0
a : Gˣ
⊢ (MulEquiv.symm withZeroUnitsEquiv : (a : G) → WithZero Gˣ) (↑a : G) = (↑a : WithZero Gˣ)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : α
⊢ Ne.{u_2 + 1} (α := WithZero β) ((e : (a : WithZero α) → WithZero β) (↑x : WithZero α) : WithZero β) (0 : WithZero β)

Tactic:
simp [ne_eq, ← e.eq_symm_apply]

Premises used: MulEquiv.eq_symm_apply, ne_eq
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : β
⊢ Ne.{u_1 + 1} (α := WithZero α) ((e.symm : (a : WithZero β) → WithZero α) (↑x : WithZero β) : WithZero α)
    (0 : WithZero α)

Tactic:
simp [e.symm_apply_eq]

Premises used: MulEquiv.symm_apply_eq
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : α
⊢ (fun (x : β) ↦ unzero ⋯) ((fun (x : α) ↦ unzero ⋯) x) = x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : β
⊢ (fun (x : α) ↦ unzero ⋯) ((fun (x : β) ↦ unzero ⋯) x) = x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : α
⊢ ∀ (y : α),
    { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ : α ≃ β }.toFun
        (x * y) =
      { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ : α ≃ β }.toFun
          x *
        { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ :
              α ≃ β }.toFun
          y

Tactic:
simp [← coe_inj]

Premises used: WithZero.coe_inj
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
x : α ≃* β
h :
  ∀ (x_1 : α),
    Eq.{u_2 + 1} (α := β)
      (((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ : α ≃* β })
              ((fun (e : α ≃* β) ↦
                  ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                      invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯,
                      right_inv := ⋯, map_mul' := ⋯ } :
                    MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
                x) :
            (a : α) → β)
          x_1 :
        β)
      ((x : (a : α) → β) x_1 : β)
⊢ (fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
        { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ : α ≃* β })
      ((fun (e : α ≃* β) ↦
          ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
              invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯, right_inv := ⋯,
              map_mul' := ⋯ } :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
x : α ≃* β
x_1 : α
⊢ Eq.{u_2 + 1} (α := β)
    (((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
              { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                map_mul' := ⋯ : α ≃* β })
            ((fun (e : α ≃* β) ↦
                ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                    invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯,
                    right_inv := ⋯, map_mul' := ⋯ } :
                  MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
              x) :
          (a : α) → β)
        x_1 :
      β)
    ((x : (a : α) → β) x_1 : β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
x : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
h :
  ∀ (x_1 : WithZero α),
    Eq.{u_2 + 1} (α := WithZero β)
      ((((fun (e : α ≃* β) ↦
                  ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                      invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯,
                      right_inv := ⋯, map_mul' := ⋯ } :
                    MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
                ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                    { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                      map_mul' := ⋯ : α ≃* β })
                  x) :
              MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
            (a : WithZero α) → WithZero β)
          x_1 :
        WithZero β)
      ((x : (a : WithZero α) → WithZero β) x_1 : WithZero β)
⊢ (fun (e : α ≃* β) ↦
        ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
            invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯, right_inv := ⋯,
            map_mul' := ⋯ } :
          MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
      ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
          { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
            map_mul' := ⋯ : α ≃* β })
        x) =
    x

Tactic:
ext x
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
x_1 : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
x : WithZero α
h :
  Eq.{u_2 + 1} (α := WithZero β)
    ((((fun (e : α ≃* β) ↦
              ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                  invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ } :
                MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
            ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ : α ≃* β })
              x_1) :
          MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
        (a : WithZero α) → WithZero β)
      0)
    ((x_1 : (a : WithZero α) → WithZero β) 0)
h₁ :
  ∀ (a : α),
    Eq.{u_2 + 1} (α := WithZero β)
      ((((fun (e : α ≃* β) ↦
                  ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                      invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯,
                      right_inv := ⋯, map_mul' := ⋯ } :
                    MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
                ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                    { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                      map_mul' := ⋯ : α ≃* β })
                  x_1) :
              MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
            (a : WithZero α) → WithZero β)
          (↑a : WithZero α) :
        WithZero β)
      ((x_1 : (a : WithZero α) → WithZero β) (↑a : WithZero α) : WithZero β)
⊢ Eq.{u_2 + 1} (α := WithZero β)
    ((((fun (e : α ≃* β) ↦
                ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                    invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯,
                    right_inv := ⋯, map_mul' := ⋯ } :
                  MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
              ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                  { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                    map_mul' := ⋯ : α ≃* β })
                x_1) :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
          (a : WithZero α) → WithZero β)
        x :
      WithZero β)
    ((x_1 : (a : WithZero α) → WithZero β) x : WithZero β)

Tactic:
cases x
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
x : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
⊢ Eq.{u_2 + 1} (α := WithZero β)
    ((((fun (e : α ≃* β) ↦
              ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                  invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ } :
                MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
            ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                  map_mul' := ⋯ : α ≃* β })
              x) :
          MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
        (a : WithZero α) → WithZero β)
      0)
    ((x : (a : WithZero α) → WithZero β) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Group α
inst_1 : Group β
x : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)
a : α
⊢ Eq.{u_2 + 1} (α := WithZero β)
    ((((fun (e : α ≃* β) ↦
                ({ toFun := (⇑(map' (↑e : α →* β)) : (a : WithZero α) → WithZero β),
                    invFun := (⇑(map' (↑e.symm : β →* α)) : (a : WithZero β) → WithZero α), left_inv := ⋯,
                    right_inv := ⋯, map_mul' := ⋯ } :
                  MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)))
              ((fun (e : MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) ↦
                  { toFun := fun (x : α) ↦ unzero ⋯, invFun := fun (x : β) ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯,
                    map_mul' := ⋯ : α ≃* β })
                x) :
            MulEquiv.{u_1, u_2} (WithZero α) (WithZero β)) :
          (a : WithZero α) → WithZero β)
        (↑a : WithZero α) :
      WithZero β)
    ((x : (a : WithZero α) → WithZero β) (↑a : WithZero α) : WithZero β)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : AddMonoidWithOne α
n : ℕ
zero :
  (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else (↑(↑(HAdd.hAdd (α := ℕ) 0 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if Eq (α := ℕ) 0 0 then 0 else (↑(↑0 : α) : WithZero α)) 1
succ :
  ∀ (n : ℕ),
    (if n + 1 + 1 = 0 then 0 else (↑(↑(n + 1 + 1) : α) : WithZero α)) =
      HAdd.hAdd (α := WithZero α) (if n + 1 = 0 then 0 else (↑(↑(n + 1) : α) : WithZero α)) 1
⊢ (if n + 1 = 0 then 0 else (↑(↑(n + 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if n = 0 then 0 else (↑(↑n : α) : WithZero α)) 1

Tactic:
cases n
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : AddMonoidWithOne α
⊢ (if HAdd.hAdd (α := ℕ) 0 1 = 0 then 0 else (↑(↑(HAdd.hAdd (α := ℕ) 0 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if Eq (α := ℕ) 0 0 then 0 else (↑(↑0 : α) : WithZero α)) 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : AddMonoidWithOne α
n : ℕ
⊢ (if n + 1 + 1 = 0 then 0 else (↑(↑(n + 1 + 1) : α) : WithZero α)) =
    HAdd.hAdd (α := WithZero α) (if n + 1 = 0 then 0 else (↑(↑(n + 1) : α) : WithZero α)) 1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
a : M
⊢ exp a ≠ 0

Tactic:
simp [exp]

Premises used: WithZero.exp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
a : M
⊢ exp a = (↑((Multiplicative.ofAdd : (a : M) → Multiplicative M) a) : WithZero (Multiplicative M))

Tactic:
rfl

Premises used: WithZero.exp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
⊢ Injective.{u_4 + 1, u_4 + 1} (α := M) exp

Tactic:
Multiplicative.ofAdd.injective.comp WithZero.coe_injective

Premises used: Function.Injective.comp, WithZero, WithZero.coe, WithZero.exp, Equiv.injective, WithZero.coe_injective, Multiplicative.ofAdd
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
x y : M
⊢ exp x = exp y ↔ x = y

Tactic:
exp_injective.eq_iff

Premises used: Function.Injective.eq_iff, WithZero.exp_injective
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
motive : WithZero (Multiplicative M) → Sort u_6
zero : motive 0
exp : (a : M) → motive (WithZero.exp a)
⊢ expRecOn (motive := fun (x : WithZero (Multiplicative M)) ↦ motive x) 0 zero exp = zero

Tactic:
rfl

Premises used: WithZero.expRecOn, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
motive : WithZero (Multiplicative M) → Sort u_6
x : M
zero : motive 0
exp : (a : M) → motive (WithZero.exp a)
⊢ expRecOn (motive := motive) (WithZero.exp x) zero exp = exp x

Tactic:
rfl

Premises used: WithZero.expRecOn, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
a : M
⊢ (exp a).log = a

Tactic:
rfl

Premises used: WithZero.log, WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
x : WithZero (Multiplicative M)
hx : x ≠ 0
⊢ x ≠ 0

Tactic:
hx
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
x : WithZero (Multiplicative M)
hx : x ≠ 0
lift : ∀ (x : Multiplicative M), exp (↑x : WithZero (Multiplicative M)).log = (↑x : WithZero (Multiplicative M))
⊢ exp x.log = x

Tactic:
lift x to Multiplicative M using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
x : Multiplicative M
⊢ exp (↑x : WithZero (Multiplicative M)).log = (↑x : WithZero (Multiplicative M))

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
⊢ Eq.{u_4 + 1} (α := M) (log 0) 0

Tactic:
rfl

Premises used: WithZero.log, WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
⊢ Eq.{u_4 + 1} (α := WithZero (Multiplicative M)) (exp 0) 1

Tactic:
rfl

Premises used: WithZero.exp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
x : M
rw : exp x = exp 0 ↔ x = 0
rw₁ rw₂ : x = 0 ↔ x = 0
⊢ exp x = 1 ↔ x = 0

Tactic:
rw [← exp_zero, exp_inj]

Premises used: WithZero.exp_inj, WithZero.exp_zero
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
⊢ Eq.{u_4 + 1} (α := M) (log 1) 0

Tactic:
rfl

Premises used: WithZero.log, WithZero.recZeroCoe, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
a b : M
⊢ exp (a + b) = exp a * exp b

Tactic:
rfl

Premises used: WithZero.coe, WithZero.exp, rfl, Option.map₂
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
x y : WithZero (Multiplicative M)
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0

Tactic:
hx
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
x y : WithZero (Multiplicative M)
hx : x ≠ 0
hy : y ≠ 0
lift :
  ∀ (x : Multiplicative M),
    ((↑x : WithZero (Multiplicative M)) * y).log = (↑x : WithZero (Multiplicative M)).log + y.log
⊢ (x * y).log = x.log + y.log

Tactic:
lift x to Multiplicative M using hx

Premises used: Multiplicative
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
y : WithZero (Multiplicative M)
hy : y ≠ 0
x : Multiplicative M
⊢ y ≠ 0

Tactic:
hy
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
y : WithZero (Multiplicative M)
hy : y ≠ 0
x : Multiplicative M
lift :
  ∀ (y : Multiplicative M),
    ((↑x : WithZero (Multiplicative M)) * (↑y : WithZero (Multiplicative M))).log =
      (↑x : WithZero (Multiplicative M)).log + (↑y : WithZero (Multiplicative M)).log
⊢ ((↑x : WithZero (Multiplicative M)) * y).log = (↑x : WithZero (Multiplicative M)).log + y.log

Tactic:
lift y to Multiplicative M using hy

Premises used: Multiplicative
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
x y : Multiplicative M
⊢ ((↑x : WithZero (Multiplicative M)) * (↑y : WithZero (Multiplicative M))).log =
    (↑x : WithZero (Multiplicative M)).log + (↑y : WithZero (Multiplicative M)).log

Tactic:
rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
n : ℕ
a : M
⊢ exp (n • a) = exp a ^ n

Tactic:
rfl

Premises used: WithZero.exp, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
⊢ (HPow.hPow (α := WithZero (Multiplicative M)) (β := ℕ) 0 0).log = HSMul.hSMul (α := ℕ) (β := M) 0 (log 0)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
M : Type u_4
inst : AddMonoid M
n : ℕ
⊢ (HPow.hPow (α := WithZero (Multiplicative M)) 0 (n + 1)).log = HSMul.hSMul (β := M) (n + 1) (log 0)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
⊢ Eq.{u_5 + 1} (α := G ≃ (WithZero (Multiplicative G))ˣ) (Equiv.symm logEquiv) expEquiv

Tactic:
rfl

Premises used: Equiv.trans, Equiv.symm, rfl, WithZero.expEquiv
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
⊢ Eq.{u_5 + 1} (α := (WithZero (Multiplicative G))ˣ ≃ G) (Equiv.symm expEquiv) logEquiv

Tactic:
rfl

Premises used: WithZero.logEquiv, Equiv.trans, WithZero.unzero, Units.mk0, Equiv.symm, rfl
-- Module: Mathlib.Algebra.GroupWithZero.WithZero
Goal:
G : Type u_5
inst : AddGroup G
a : G
⊢ (↑((expEquiv : (a : G) → (WithZero (Multiplicative G))ˣ) a) : WithZero (Multiplicative G)) = exp a

Tactic:
rfl

Premises used: WithZero.coe, WithZero.exp, rfl