[GOAL]
⊢ ∀ (a b c : PUnit), a * b * c = a * (b * c)
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ c✝ : PUnit
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), 1 * a = a
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ 1 * a✝ = a✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), a * 1 = a
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ a✝ * 1 = a✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), a⁻¹ * a = 1
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ a✝⁻¹ * a✝ = 1
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a b : PUnit), a * b = b * a
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : PUnit
⊢ a✝ * b✝ = b✝ * a✝
[PROOFSTEP]
rfl
  -- shortcut instances
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a b c : PUnit), a * (b + c) = a * b + a * c
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ b✝ c✝ : PUnit
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a b c : PUnit), (a + b) * c = a * c + b * c
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ b✝ c✝ : PUnit
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a : PUnit), 0 * a = 0
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ : PUnit
⊢ 0 * a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
⊢ ∀ (a : PUnit), a * 0 = 0
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CommGroup PUnit := commGroup
src✝ : AddCommGroup PUnit := addCommGroup
a✝ : PUnit
⊢ a✝ * 0 = 0
[PROOFSTEP]
rfl
[GOAL]
⊢ CancelCommMonoidWithZero PUnit
[PROOFSTEP]
refine' { PUnit.commRing with .. }
[GOAL]
src✝ : CommRing PUnit := commRing
⊢ ∀ {a b c : PUnit}, a ≠ 0 → a * b = a * c → b = c
[PROOFSTEP]
intros
[GOAL]
src✝ : CommRing PUnit := commRing
a✝² b✝ c✝ : PUnit
a✝¹ : a✝² ≠ 0
a✝ : a✝² * b✝ = a✝² * c✝
⊢ b✝ = c✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
⊢ ∀ {a b : PUnit}, a ≠ 0 → b ≠ 0 → (fun x => 1) (a * b) = (fun x => 1) a * (fun x => 1) b
[PROOFSTEP]
intros
[GOAL]
a✝² b✝ : PUnit
a✝¹ : a✝² ≠ 0
a✝ : b✝ ≠ 0
⊢ (fun x => 1) (a✝² * b✝) = (fun x => 1) a✝² * (fun x => 1) b✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (u : PUnitˣ), (fun x => 1) ↑u = u⁻¹
[PROOFSTEP]
intros
[GOAL]
u✝ : PUnitˣ
⊢ (fun x => 1) ↑u✝ = u✝⁻¹
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), (fun x x => unit) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ (fun x x => unit) 0 a✝ = 0
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a : PUnit), (fun x x => unit) a 0 = 0
[PROOFSTEP]
intros
[GOAL]
a✝ : PUnit
⊢ (fun x x => unit) a✝ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a b : PUnit), ↑normalize (gcd a b) = gcd a b
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : PUnit
⊢ ↑normalize (gcd a✝ b✝) = gcd a✝ b✝
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (a b : PUnit), ↑normalize (lcm a b) = lcm a b
[PROOFSTEP]
intros
[GOAL]
a✝ b✝ : PUnit
⊢ ↑normalize (lcm a✝ b✝) = lcm a✝ b✝
[PROOFSTEP]
rfl
  --porting notes: simpNF lint: simp can prove this @[simp]
[GOAL]
⊢ CanonicallyOrderedAddMonoid PUnit
[PROOFSTEP]
refine'
  { PUnit.commRing, PUnit.completeBooleanAlgebra with
    exists_add_of_le := fun {_ _} _ => ⟨unit, Subsingleton.elim _ _⟩ .. }
[GOAL]
case refine'_1
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
⊢ ∀ (a b : PUnit), a ≤ b → ∀ (c : PUnit), c + a ≤ c + b
[PROOFSTEP]
intros
[GOAL]
case refine'_2
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
⊢ ∀ (a b : PUnit), a ≤ a + b
[PROOFSTEP]
intros
[GOAL]
case refine'_1
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
a✝¹ b✝ : PUnit
a✝ : a✝¹ ≤ b✝
c✝ : PUnit
⊢ c✝ + a✝¹ ≤ c✝ + b✝
[PROOFSTEP]
trivial
[GOAL]
case refine'_2
src✝¹ : CommRing PUnit := commRing
src✝ : CompleteBooleanAlgebra PUnit := completeBooleanAlgebra
a✝ b✝ : PUnit
⊢ a✝ ≤ a✝ + b✝
[PROOFSTEP]
trivial
[GOAL]
src✝¹ : CanonicallyOrderedAddMonoid PUnit := canonicallyOrderedAddMonoid
src✝ : LinearOrder PUnit := linearOrder
⊢ ∀ (a b : PUnit), a ≤ b → ∀ (c : PUnit), c + a ≤ c + b
[PROOFSTEP]
intros
[GOAL]
src✝¹ : CanonicallyOrderedAddMonoid PUnit := canonicallyOrderedAddMonoid
src✝ : LinearOrder PUnit := linearOrder
a✝¹ b✝ : PUnit
a✝ : a✝¹ ≤ b✝
c✝ : PUnit
⊢ c✝ + a✝¹ ≤ c✝ + b✝
[PROOFSTEP]
rfl
[GOAL]
R : Type ?u.10038
inst✝ : Zero R
⊢ SMulWithZero R PUnit
[PROOFSTEP]
refine' { PUnit.smul with .. }
[GOAL]
case refine'_1
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
⊢ ∀ (m : PUnit), 0 • m = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
a✝ : R
⊢ a✝ • 0 = 0
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.10038
inst✝ : Zero R
src✝ : SMul R PUnit := smul
m✝ : PUnit
⊢ 0 • m✝ = 0
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.10319
inst✝ : Monoid R
⊢ MulAction R PUnit
[PROOFSTEP]
refine' { PUnit.smul with .. }
[GOAL]
case refine'_1
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
⊢ ∀ (b : PUnit), 1 • b = b
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
⊢ ∀ (x y : R) (b : PUnit), (x * y) • b = x • y • b
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
b✝ : PUnit
⊢ 1 • b✝ = b✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.10319
inst✝ : Monoid R
src✝ : SMul R PUnit := smul
x✝ y✝ : R
b✝ : PUnit
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.10545
inst✝ : Monoid R
⊢ DistribMulAction R PUnit
[PROOFSTEP]
refine' { PUnit.mulAction with .. }
[GOAL]
case refine'_1
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (a : R) (x y : PUnit), a • (x + y) = a • x + a • y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
a✝ : R
⊢ a✝ • 0 = 0
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.10545
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
a✝ : R
x✝ y✝ : PUnit
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.11055
inst✝ : Monoid R
⊢ MulDistribMulAction R PUnit
[PROOFSTEP]
refine' { PUnit.mulAction with .. }
[GOAL]
case refine'_1
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (r : R) (x y : PUnit), r • (x * y) = r • x * r • y
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
⊢ ∀ (r : R), r • 1 = 1
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
r✝ : R
x✝ y✝ : PUnit
⊢ r✝ • (x✝ * y✝) = r✝ • x✝ * r✝ • y✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.11055
inst✝ : Monoid R
src✝ : MulAction R PUnit := mulAction
r✝ : R
⊢ r✝ • 1 = 1
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
R : Type ?u.13538
inst✝ : Semiring R
⊢ Module R PUnit
[PROOFSTEP]
refine' { PUnit.distribMulAction with .. }
[GOAL]
case refine'_1
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
⊢ ∀ (r s : R) (x : PUnit), (r + s) • x = r • x + s • x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
⊢ ∀ (x : PUnit), 0 • x = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
r✝ s✝ : R
x✝ : PUnit
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
case refine'_2
R : Type ?u.13538
inst✝ : Semiring R
src✝ : DistribMulAction R PUnit := distribMulAction
x✝ : PUnit
⊢ 0 • x✝ = 0
[PROOFSTEP]
exact Subsingleton.elim _ _
