awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroClass β
zero : Zero α := e.zero
mul : Mul α := e.mul
zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
⊢ MulZeroClass α
have mul₁ : ∀ (a b : α), (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)
Tactic: apply e.injective.mulZeroClass _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
⊢ MulZeroOneClass α
have zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.mulZeroOneClass _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
⊢ MulZeroOneClass α
have one₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.mulZeroOneClass _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MulZeroOneClass β
zero : Zero α := e.zero
one : One α := e.one
mul : Mul α := e.mul
zero₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one₁ : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ MulZeroOneClass α
have mul₁ : ∀ (a b : α), (e : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) a : β) ((e : (a : α) → β) b : β)
Tactic: apply e.injective.mulZeroOneClass _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
⊢ MonoidWithZero α
have zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.monoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
⊢ MonoidWithZero α
have one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.monoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ MonoidWithZero α
have mul : ∀ (x_2 y : α),
  (e : (a : α) → β) (x_2 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_2 : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.monoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : MonoidWithZero β
x : MulZeroOneClass α := e.mulZeroOneClass
x_1 : Pow α ℕ := Equiv.pow ℕ e
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul :
  ∀ (x_2 y : α),
    (e : (a : α) → β) (x_2 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_2 : β) ((e : (a : α) → β) y : β)
⊢ MonoidWithZero α
have npow : ∀ (x : α) (n : ℕ), (e : (a : α) → β) (x ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x : β) n
Tactic: apply e.injective.monoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
⊢ CommMonoidWithZero α
have zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
Tactic: apply e.injective.commMonoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
⊢ CommMonoidWithZero α
have one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
Tactic: apply e.injective.commMonoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
⊢ CommMonoidWithZero α
have mul : ∀ (x_1 y : α),
  (e : (a : α) → β) (x_1 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y : β)
Tactic: apply e.injective.commMonoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.TransferInstance (goal)
Goal:
α : Type u
β : Type v
e : α ≃ β
inst : CommMonoidWithZero β
x : MonoidWithZero α := e.monoidWithZero
zero : Eq.{v + 1} (α := β) ((e : (a : α) → β) 0 : β) (0 : β)
one : Eq.{v + 1} (α := β) ((e : (a : α) → β) 1 : β) (1 : β)
mul :
  ∀ (x_1 y : α),
    (e : (a : α) → β) (x_1 * y) = HMul.hMul (α := β) (β := β) ((e : (a : α) → β) x_1 : β) ((e : (a : α) → β) y : β)
⊢ CommMonoidWithZero α
have npow : ∀ (x_1 : α) (n : ℕ), (e : (a : α) → β) (x_1 ^ n) = HPow.hPow (α := β) ((e : (a : α) → β) x_1 : β) n
Tactic: apply e.injective.commMonoidWithZero _
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
h : IsUnit.{u_2} (M := M₀) 0
a : M₀
a0 : 0 * a = 1
inv_val : a * 0 = 1
⊢ Eq.{u_2 + 1} (α := M₀) 0 1
have rwa : ∀ (a0 : Eq.{u_2 + 1} (α := M₀) 0 1), a * 0 = 1 → Eq.{u_2 + 1} (α := M₀) 0 1
Tactic: rwa [zero_mul] at a0
Cleared hypotheses: a0, inv_val
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u : M₀)⁻¹ʳ = (↑u⁻¹ : M₀)
have rw : (if h : IsUnit (↑u : M₀) then (↑h.unit⁻¹ : M₀) else 0) = (↑u⁻¹ : M₀)
Tactic: rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (if h : IsUnit (↑u : M₀) then (↑h.unit⁻¹ : M₀) else 0) = (↑u⁻¹ : M₀)
⊢ (↑u : M₀)⁻¹ʳ = (↑u⁻¹ : M₀)
have rw₁ : (↑sorry.unit⁻¹ : M₀) = (↑u⁻¹ : M₀)
Tactic: rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (if h : IsUnit (↑u : M₀) then (↑h.unit⁻¹ : M₀) else 0) = (↑u⁻¹ : M₀)
rw₁ : (↑⋯.unit⁻¹ : M₀) = (↑u⁻¹ : M₀)
⊢ (↑u : M₀)⁻¹ʳ = (↑u⁻¹ : M₀)
have rw₂ : (↑u⁻¹ : M₀) = (↑u⁻¹ : M₀)
Tactic: rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x * x⁻¹ʳ = 1
have rcases : ∀ (u : M₀ˣ), (↑u : M₀) * (↑u : M₀)⁻¹ʳ = 1
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u : M₀) * (↑u : M₀)⁻¹ʳ = 1
have rw : (↑u : M₀) * (↑u⁻¹ : M₀) = 1
Tactic: rw [inverse_unit, Units.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (↑u : M₀) * (↑u⁻¹ : M₀) = 1
⊢ (↑u : M₀) * (↑u : M₀)⁻¹ʳ = 1
have rw₁ : Eq.{u_2 + 1} (α := M₀) 1 1
Tactic: rw [inverse_unit, Units.mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : IsUnit x
⊢ x⁻¹ʳ * x = 1
have rcases : ∀ (u : M₀ˣ), (↑u : M₀)⁻¹ʳ * (↑u : M₀) = 1
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u : M₀)⁻¹ʳ * (↑u : M₀) = 1
have rw : (↑u⁻¹ : M₀) * (↑u : M₀) = 1
Tactic: rw [inverse_unit, Units.inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (↑u⁻¹ : M₀) * (↑u : M₀) = 1
⊢ (↑u : M₀)⁻¹ʳ * (↑u : M₀) = 1
have rw₁ : Eq.{u_2 + 1} (α := M₀) 1 1
Tactic: rw [inverse_unit, Units.inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x * x⁻¹ʳ = y
have rw : y * (x * x⁻¹ʳ) = y
Tactic: rw [mul_assoc, mul_inverse_cancel x h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : y * (x * x⁻¹ʳ) = y
⊢ y * x * x⁻¹ʳ = y
have rw₁ : y * 1 = y
Tactic: rw [mul_assoc, mul_inverse_cancel x h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : y * (x * x⁻¹ʳ) = y
rw₁ : y * 1 = y
⊢ y * x * x⁻¹ʳ = y
have rw₂ : y = y
Tactic: rw [mul_assoc, mul_inverse_cancel x h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x⁻¹ʳ * x = y
have rw : y * (x⁻¹ʳ * x) = y
Tactic: rw [mul_assoc, inverse_mul_cancel x h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : y * (x⁻¹ʳ * x) = y
⊢ y * x⁻¹ʳ * x = y
have rw₁ : y * 1 = y
Tactic: rw [mul_assoc, inverse_mul_cancel x h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : y * (x⁻¹ʳ * x) = y
rw₁ : y * 1 = y
⊢ y * x⁻¹ʳ * x = y
have rw₂ : y = y
Tactic: rw [mul_assoc, inverse_mul_cancel x h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ x * (x⁻¹ʳ * y) = y
have rw : x * x⁻¹ʳ * y = y
Tactic: rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : x * x⁻¹ʳ * y = y
⊢ x * (x⁻¹ʳ * y) = y
have rw₁ : 1 * y = y
Tactic: rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : x * x⁻¹ʳ * y = y
rw₁ : 1 * y = y
⊢ x * (x⁻¹ʳ * y) = y
have rw₂ : y = y
Tactic: rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ x⁻¹ʳ * (x * y) = y
have rw : x⁻¹ʳ * x * y = y
Tactic: rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : x⁻¹ʳ * x * y = y
⊢ x⁻¹ʳ * (x * y) = y
have rw₁ : 1 * y = y
Tactic: rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y : M₀
h : IsUnit x
rw : x⁻¹ʳ * x * y = y
rw₁ : 1 * y = y
⊢ x⁻¹ʳ * (x * y) = y
have rw₂ : y = y
Tactic: rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : x⁻¹ʳ * y = z
⊢ y = x * z
have rw : y = x * (x⁻¹ʳ * y)
Tactic: rw [← h1, mul_inverse_cancel_left _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : x⁻¹ʳ * y = z
rw : y = x * (x⁻¹ʳ * y)
⊢ y = x * z
have rw₁ : y = y
Tactic: rw [← h1, mul_inverse_cancel_left _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ x⁻¹ʳ * y = z
have rw : x⁻¹ʳ * (x * z) = z
Tactic: rw [h1, inverse_mul_cancel_left _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
rw : x⁻¹ʳ * (x * z) = z
⊢ x⁻¹ʳ * y = z
have rw₁ : z = z
Tactic: rw [h1, inverse_mul_cancel_left _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
⊢ x * z = y
have rw : y * z⁻¹ʳ * z = y
Tactic: rw [h1, inverse_mul_cancel_right _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x = y * z⁻¹ʳ
rw : y * z⁻¹ʳ * z = y
⊢ x * z = y
have rw₁ : y = y
Tactic: rw [h1, inverse_mul_cancel_right _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
⊢ x = y * z⁻¹ʳ
have rw : x = x * z * z⁻¹ʳ
Tactic: rw [← h1, mul_inverse_cancel_right _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
rw : x = x * z * z⁻¹ʳ
⊢ x = y * z⁻¹ʳ
have rw₁ : x = x
Tactic: rw [← h1, mul_inverse_cancel_right _ _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
⊢ Eq.{u_2 + 1} (α := M₀) 0⁻¹ʳ 0
have a : Nontrivial M₀
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ = a
have obtain : ∀ (u : M₀ˣ), (↑u : M₀)⁻¹ʳ⁻¹ʳ = (↑u : M₀)
Tactic: obtain ⟨u, rfl⟩ := h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u : M₀)⁻¹ʳ⁻¹ʳ = (↑u : M₀)
have rw : (↑u⁻¹ : M₀)⁻¹ʳ = (↑u : M₀)
Tactic: rw [inverse_unit, inverse_unit, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (↑u⁻¹ : M₀)⁻¹ʳ = (↑u : M₀)
⊢ (↑u : M₀)⁻¹ʳ⁻¹ʳ = (↑u : M₀)
have rw₁ : (↑u⁻¹⁻¹ : M₀) = (↑u : M₀)
Tactic: rw [inverse_unit, inverse_unit, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
u : M₀ˣ
rw : (↑u⁻¹ : M₀)⁻¹ʳ = (↑u : M₀)
rw₁ : (↑u⁻¹⁻¹ : M₀) = (↑u : M₀)
⊢ (↑u : M₀)⁻¹ʳ⁻¹ʳ = (↑u : M₀)
have rw₂ : (↑u : M₀) = (↑u : M₀)
Tactic: rw [inverse_unit, inverse_unit, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
⊢ IsUnit a
have inl : Subsingleton M₀ → IsUnit a
Tactic: cases subsingleton_or_nontrivial M₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
inl : Subsingleton M₀ → IsUnit a
⊢ IsUnit a
have inr : Nontrivial M₀ → IsUnit a
Tactic: cases subsingleton_or_nontrivial M₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h_1 : Nontrivial M₀
⊢ IsUnit a
have inr : ∀ (h : ¬IsUnit a), ¬IsUnit a⁻¹ʳ
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h_1 : Nontrivial M₀
h : ¬IsUnit a
⊢ ¬IsUnit a⁻¹ʳ
have inr : ¬IsUnit.{u_2} (M := M₀) 0
Tactic: rw [Ring.inverse_non_unit _ h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have inl : ∀ (ha : IsUnit a) (hb : ¬IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Tactic: obtain (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) :
      (IsUnit a ∧ ¬ IsUnit b) ∨ (¬ IsUnit a ∧ IsUnit b) ∨ (IsUnit a ∧ IsUnit b) := by grind
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
inl : ∀ (ha : IsUnit a) (hb : ¬IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have inr : ∀ (ha : ¬IsUnit a) (hb : IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Tactic: obtain (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) :
      (IsUnit a ∧ ¬ IsUnit b) ∨ (¬ IsUnit a ∧ IsUnit b) ∨ (IsUnit a ∧ IsUnit b) := by grind
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
inl : ∀ (ha : IsUnit a) (hb : ¬IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
inr : ∀ (ha : ¬IsUnit a) (hb : IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have inr₁ : ∀ (ha : IsUnit a) (hb : IsUnit b), (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
Tactic: obtain (⟨ha, hb⟩ | ⟨ha, hb⟩ | ⟨ha, hb⟩) :
      (IsUnit a ∧ ¬ IsUnit b) ∨ (¬ IsUnit a ∧ IsUnit b) ∨ (IsUnit a ∧ IsUnit b) := by grind
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : ¬IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have this : ¬IsUnit (a * b)
Tactic: have : ¬ IsUnit (a * b) := by simpa [ha.mul_left_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have this : ¬IsUnit (a * b)
Tactic: have : ¬ IsUnit (a * b) := by simpa [hb.mul_right_iff]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ
have inr : a * b = (↑(ha.unit * hb.unit) : M₀)
Tactic: simp [Ring.inverse_of_isUnit, ha, hb, ha.mul hb, ← Units.val_mul, ← mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
⊢ IsUnit x ↔ x * x⁻¹ʳ = 1
have a : Nontrivial M₀
Tactic: nontriviality M₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ IsUnit x ↔ x * x⁻¹ʳ = 1
have refine : x * x⁻¹ʳ = 1 → IsUnit x
Tactic: refine ⟨mul_inverse_cancel _, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ x * x⁻¹ʳ = 1 → IsUnit x
have contrapose : ¬IsUnit x → ¬x * x⁻¹ʳ = 1
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
⊢ IsUnit x ↔ x⁻¹ʳ * x = 1
have a : Nontrivial M₀
Tactic: nontriviality M₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ IsUnit x ↔ x⁻¹ʳ * x = 1
have refine : x⁻¹ʳ * x = 1 → IsUnit x
Tactic: refine ⟨Ring.inverse_mul_cancel x, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
x : M₀
h : Nontrivial M₀
⊢ x⁻¹ʳ * x = 1 → IsUnit x
have contrapose : ¬IsUnit x → ¬x⁻¹ʳ * x = 1
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (hypothesis)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
have a₁ : Nontrivial M₀
Tactic: nontriviality M₀
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : Nontrivial M₀
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
have pos : ∀ (h : IsUnit a), a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
Tactic: by_cases h : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h : Nontrivial M₀
pos : ∀ (h : IsUnit a), a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
have neg : ∀ (h : ¬IsUnit a), a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
Tactic: by_cases h : IsUnit a
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
M₀ : Type u_2
inst : MonoidWithZero M₀
a : M₀
h_1 : Nontrivial M₀
h : IsUnit a
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ
have pos : a⁻¹ʳ = a⁻¹ʳ
Tactic: rw [Ring.inverse_inverse h]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
h : Ne.{u_3 + 1} (α := G₀) 1 0
⊢ mk0 1 h = 1
have huv : (↑(mk0 1 h) : G₀) = (↑1 : G₀)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst : MonoidWithZero M₀
inst_1 : GroupWithZero G₀
a_1 b_1 c : G₀
m n : ℕ
a b : G₀
h : a * b = 0
⊢ a = 0 ∨ b = 0
have contrapose! : ∀ (h : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ mk0 (x * y) hxy = mk0 x ⋯ * mk0 y ⋯
have huv : (↑(mk0 (x * y) hxy) : G₀) = (↑(mk0 x sorry * mk0 y sorry) : G₀)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a / b ≠ 0
have rw : a * b⁻¹ ≠ 0
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a : G₀
⊢ a / a = 1 → a ≠ 0
have contrapose! : a = 0 → a / a ≠ 1
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ a * b = c
have rwa : b ≠ 0
Tactic: rwa [← eq_mul_inv_iff_mul_eq₀]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a * b = c
have rwa : a ≠ 0
Tactic: rwa [← eq_inv_mul_iff_mul_eq₀]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
c : G₀
hc : c ≠ 0
a b : G₀
⊢ a / c / (b / c) = a / b
have rw : a / c * c / b = a / b
Tactic: rw [div_div_eq_mul_div, div_mul_cancel₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
c : G₀
hc : c ≠ 0
a b : G₀
rw : a / c * c / b = a / b
⊢ a / c / (b / c) = a / b
have rw₁ : a / b = a / b
Tactic: rw [div_div_eq_mul_div, div_mul_cancel₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
⊢ a / b * (b / c) = a / c
have rw : a / b * b / c = a / c
Tactic: rw [← mul_div_assoc, div_mul_cancel₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
rw : a / b * b / c = a / c
⊢ a / b * (b / c) = a / c
have rw₁ : a / c = a / c
Tactic: rw [← mul_div_assoc, div_mul_cancel₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a / b * b = a
have inl : ∀ (h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0), a / 0 * 0 = a
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
inl : ∀ (h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0), a / 0 * 0 = a
⊢ a / b * b = a
have inr : ∀ (hb : b ≠ 0), a / b * b = a
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.Algebra.GroupWithZero.Units.Basic (goal)
Goal:
G₀ : Type u_3
inst : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
⊢ a * b / b = a
have inl : ∀ (h : Eq.{u_3 + 1} (α := G₀) 0 0 → a = 0), a * 0 / 0 = a
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b, h