awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
inst_2 : DecidableEq M
⊢ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = if a = 1 then ∅ else {i}
have pos : ∀ (h : a = 1), mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
inst_2 : DecidableEq M
pos : ∀ (h : a = 1), mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = ∅
⊢ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = if a = 1 then ∅ else {i}
have neg : ∀ (h : ¬a = 1), mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = {i}
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
⊢ (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a)).Subsingleton
have rw : Set.Subsingleton (α := ι) (if a = 1 then ∅ else {i})
Tactic: rw [mulSupport_mulSingle]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
⊢ Set.Subsingleton (α := ι) (if a = 1 then ∅ else {i})
have pos : ∀ (h : a = 1), Set.Subsingleton.{u_1} (α := ι) ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
pos : ∀ (h : a = 1), Set.Subsingleton.{u_1} (α := ι) ∅
⊢ Set.Subsingleton (α := ι) (if a = 1 then ∅ else {i})
have neg : ∀ (h : ¬a = 1), Set.Subsingleton (α := ι) {i}
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
⊢ (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a)).Subsingleton
have rw : Set.Subsingleton (α := ι) (if a = 1 then ∅ else {i})
Tactic: classical
  rw [mulSupport_mulSingle]
  split_ifs with h <;> simp
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a))
      (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔
    i ≠ j
have rw : Disjoint {i} (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔ i ≠ j
Tactic: rw [mulSupport_mulSingle_of_ne ha, mulSupport_mulSingle_of_ne hb, disjoint_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
rw : Disjoint {i} (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔ i ≠ j
⊢ Disjoint (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a))
      (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔
    i ≠ j
have rw₁ : Disjoint (α := Set ι) {i} {j} ↔ i ≠ j
Tactic: rw [mulSupport_mulSingle_of_ne ha, mulSupport_mulSingle_of_ne hb, disjoint_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Support (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
rw : Disjoint {i} (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔ i ≠ j
rw₁ : Disjoint (α := Set ι) {i} {j} ↔ i ≠ j
⊢ Disjoint (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a))
      (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔
    i ≠ j
have rw₂ : i ≠ j ↔ i ≠ j
Tactic: rw [mulSupport_mulSingle_of_ne ha, mulSupport_mulSingle_of_ne hb, disjoint_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Opposites (goal)
Goal:
α : Type u_1
inst : Add α
⊢ IsCancelAdd.{u_1} αᵐᵒᵖ ↔ IsCancelAdd α
have simp_rw : IsLeftCancelAdd.{u_1} αᵐᵒᵖ ∧ IsRightCancelAdd.{u_1} αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α
Tactic: simp_rw [isCancelAdd_iff, isLeftCancelAdd_iff, isRightCancelAdd_iff]
-- Lean 4 proof step from Mathlib.Algebra.Opposites (goal)
Goal:
α : Type u_1
inst : Add α
simp_rw : IsLeftCancelAdd.{u_1} αᵐᵒᵖ ∧ IsRightCancelAdd.{u_1} αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α
⊢ IsCancelAdd.{u_1} αᵐᵒᵖ ↔ IsCancelAdd α
have simp_rw₁ : IsLeftCancelAdd α ∧ IsRightCancelAdd.{u_1} αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α
Tactic: simp_rw [isCancelAdd_iff, isLeftCancelAdd_iff, isRightCancelAdd_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv f g : AbsoluteValue R S
h : Eq (α := (a : R) → S) ((fun (f : AbsoluteValue R S) ↦ f.toFun) f) ((fun (f : AbsoluteValue R S) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : R → S) (map_mul' : ∀ (x y : R), toFun (x * y) = toFun x * toFun y)
  (nonneg' : ∀ (x : R), 0 ≤ { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x)
  (eq_zero' : ∀ (x : R), { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x = 0 ↔ x = 0)
  (add_le' :
    ∀ (x y : R),
      { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun (x + y) ≤
        { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x +
          { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun y)
  (h :
    Eq (α := (a : R) → S)
      ((fun (f : AbsoluteValue R S) ↦ f.toFun)
        { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' })
      ((fun (f : AbsoluteValue R S) ↦ f.toFun) g)),
  { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' :
      AbsoluteValue R S } =
    g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv g : AbsoluteValue R S
toFun : R → S
map_mul' : ∀ (x y : R), toFun (x * y) = toFun x * toFun y
nonneg' : ∀ (x : R), 0 ≤ { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x
eq_zero' : ∀ (x : R), { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x = 0 ↔ x = 0
add_le' :
  ∀ (x y : R),
    { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun (x + y) ≤
      { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x +
        { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun y
h :
  Eq (α := (a : R) → S)
    ((fun (f : AbsoluteValue R S) ↦ f.toFun)
      { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' })
    ((fun (f : AbsoluteValue R S) ↦ f.toFun) g)
⊢ { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' :
      AbsoluteValue R S } =
    g
have obtain : ∀ (toFun_1 : R → S) (map_mul'_1 : ∀ (x y : R), toFun_1 (x * y) = toFun_1 x * toFun_1 y)
  (nonneg'_1 : ∀ (x : R), 0 ≤ { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x)
  (eq_zero'_1 : ∀ (x : R), { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x = 0 ↔ x = 0)
  (add_le'_1 :
    ∀ (x y : R),
      { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun (x + y) ≤
        { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun x +
          { toFun := toFun_1, map_mul' := map_mul'_1 : R →ₙ* S }.toFun y)
  (h :
    Eq (α := (a : R) → S)
      ((fun (f : AbsoluteValue R S) ↦ f.toFun)
        { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' })
      ((fun (f : AbsoluteValue R S) ↦ f.toFun)
        { toFun := toFun_1, map_mul' := map_mul'_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1,
          add_le' := add_le'_1 })),
  { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' :
      AbsoluteValue R S } =
    { toFun := toFun_1, map_mul' := map_mul'_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1, add_le' := add_le'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : AddLeftMono S
l : List R
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) l.sum : S) (List.sum (List.map (⇑abv : (a : R) → S) l) : S)
have nil : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (List.sum []) : S)
  (List.sum (List.map.{u_5, u_6} (α := R) (⇑abv : (a : R) → S) []) : S)
Tactic: induction l with
  | nil => simp
  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_right ih (abv head)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : AddLeftMono S
l : List R
nil :
  LE.le.{u_6} (α := S) ((abv : (a : R) → S) (List.sum []) : S)
    (List.sum (List.map.{u_5, u_6} (α := R) (⇑abv : (a : R) → S) []) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) l.sum : S) (List.sum (List.map (⇑abv : (a : R) → S) l) : S)
have cons : ∀ (head : R) (tail : List R)
  (ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) tail.sum : S) (List.sum (List.map (⇑abv : (a : R) → S) tail) : S)),
  LE.le.{u_6} (α := S) ((abv : (a : R) → S) (head :: tail).sum : S)
    (List.sum (List.map (⇑abv : (a : R) → S) (head :: tail)) : S)
Tactic: induction l with
  | nil => simp
  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_right ih (abv head)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
n : ℕ
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
have inl : Subsingleton R → LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
n : ℕ
inl : Subsingleton R → LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
have inr : Nontrivial R → LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
h : Nontrivial R
n : ℕ
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)
have inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) : S) ((↑(n + 1) : S) : S)
Tactic: grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
h : Nontrivial R
n : ℕ
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) : S) ((↑(n + 1) : S) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)
have inr₁ : (abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) ≤ HAdd.hAdd (α := S) (↑n : S) 1
Tactic: grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
h : Nontrivial R
n : ℕ
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) : S) ((↑(n + 1) : S) : S)
inr₁ : (abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) ≤ HAdd.hAdd (α := S) (↑n : S) 1
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)
have inr₂ : HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (↑n : R) : S) ((abv : (a : R) → S) 1 : S) ≤
  HAdd.hAdd (α := S) (↑n : S) 1
Tactic: grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
h : Nontrivial R
n : ℕ
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) : S) ((↑(n + 1) : S) : S)
inr₁ : (abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) ≤ HAdd.hAdd (α := S) (↑n : S) 1
inr₂ :
  HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (↑n : R) : S) ((abv : (a : R) → S) 1 : S) ≤
    HAdd.hAdd (α := S) (↑n : S) 1
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)
have inr₃ : HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (↑n : R) : S) (1 : S) ≤ HAdd.hAdd (α := S) (↑n : S) 1
Tactic: grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
h : Nontrivial R
n : ℕ
ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) : S) ((↑(n + 1) : S) : S)
inr₁ : (abv : (a : R) → S) (HAdd.hAdd (α := R) (↑n : R) 1) ≤ HAdd.hAdd (α := S) (↑n : S) 1
inr₂ :
  HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (↑n : R) : S) ((abv : (a : R) → S) 1 : S) ≤
    HAdd.hAdd (α := S) (↑n : S) 1
inr₃ : HAdd.hAdd (α := S) (β := S) ((abv : (a : R) → S) (↑n : R) : S) (1 : S) ≤ HAdd.hAdd (α := S) (↑n : S) 1
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)
have inr₄ : HAdd.hAdd (α := S) (↑n : S) 1 ≤ HAdd.hAdd (α := S) (↑n : S) 1
Tactic: grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
n : ℕ
h : Nontrivial R
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
have inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑0 : R) : S) ((↑0 : S) : S)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
  · grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : IsOrderedRing S
n : ℕ
h : Nontrivial R
inr : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑0 : R) : S) ((↑0 : S) : S)
⊢ LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)
have inr₁ : ∀ (n : ℕ) (ih : LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑n : R) : S) ((↑n : S) : S)),
  LE.le.{u_6} (α := S) ((abv : (a : R) → S) (↑(n + 1) : R) : S) ((↑(n + 1) : S) : S)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
  · grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
have pos : ∀ (ha : a = 0), Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
pos : ∀ (ha : a = 0), Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
have neg : ∀ (ha : ¬a = 0), Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) (-a) : S) =
    HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
have rw : (abv : (a : R) → S) (-a * -a) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
Tactic: rw [← abv.map_mul, neg_mul_neg, abv.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
rw : (abv : (a : R) → S) (-a * -a) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
⊢ HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) (-a) : S) =
    HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
have rw₁ : (abv : (a : R) → S) (a * a) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
Tactic: rw [← abv.map_mul, neg_mul_neg, abv.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
rw : (abv : (a : R) → S) (-a * -a) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
rw₁ : (abv : (a : R) → S) (a * a) = HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
⊢ HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) (-a) : S) =
    HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
have rw₂ : HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S) =
  HMul.hMul (α := S) (β := S) ((abv : (a : R) → S) a : S) ((abv : (a : R) → S) a : S)
Tactic: rw [← abv.map_mul, neg_mul_neg, abv.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) ((abv : (a : R) → S) a : S)
have neg : ¬Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-a) : S) (-(abv : (a : R) → S) a : S)
Tactic: refine
    (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a b : R
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (a - b) : S) ((abv : (a : R) → S) (b - a) : S)
have rw : Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-(b - a)) : S) ((abv : (a : R) → S) (b - a) : S)
Tactic: rw [← neg_sub, abv.map_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
a b : R
rw : Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (-(b - a)) : S) ((abv : (a : R) → S) (b - a) : S)
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (a - b) : S) ((abv : (a : R) → S) (b - a) : S)
have rw₁ : Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (b - a) : S) ((abv : (a : R) → S) (b - a) : S)
Tactic: rw [← neg_sub, abv.map_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
x : ℤ
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑x.natAbs : R) : S) ((abv : (a : R) → S) (↑x : R) : S)
have inl : ∀ (w : ℕ),
  Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑(natAbs (↑w : ℤ)) : R) : S) ((abv : (a : R) → S) (↑(↑w : ℤ) : R) : S)
Tactic: obtain ⟨_, rfl | rfl⟩ := Int.eq_nat_or_neg x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
abv : AbsoluteValue R S
inst_4 : NoZeroDivisors S
x : ℤ
inl :
  ∀ (w : ℕ),
    Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑(natAbs (↑w : ℤ)) : R) : S) ((abv : (a : R) → S) (↑(↑w : ℤ) : R) : S)
⊢ Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑x.natAbs : R) : S) ((abv : (a : R) → S) (↑x : R) : S)
have inr : ∀ (w : ℕ),
  Eq.{u_4 + 1} (α := S) ((abv : (a : R) → S) (↑(natAbs (-(↑w : ℤ))) : R) : S)
    ((abv : (a : R) → S) (↑(-(↑w : ℤ)) : R) : S)
Tactic: obtain ⟨_, rfl | rfl⟩ := Int.eq_nat_or_neg x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
inst_4 : NoZeroDivisors S
f g : AbsoluteValue R S
⊢ (∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)) ↔
    ∀ (n : ℤ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)
have refine : ∀ (h : ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)) (z : ℤ),
  Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑z : R) : S) ((g : (a : R) → S) (↑z : R) : S)
Tactic: refine ⟨fun h z ↦ ?_, fun a n ↦ mod_cast a n⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.AbsoluteValue.Basic (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing S
inst_1 : PartialOrder S
inst_2 : IsOrderedRing S
inst_3 : Ring R
inst_4 : NoZeroDivisors S
f g : AbsoluteValue R S
h : ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((g : (a : R) → S) (↑n : R) : S)
z : ℤ
⊢ Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑z : R) : S) ((g : (a : R) → S) (↑z : R) : S)
have inl : ∀ (n : ℕ), Eq.{u_4 + 1} (α := S) ((f : (a : R) → S) (↑(↑n : ℤ) : R) : S) ((g : (a : R) → S) (↑(↑n : ℤ) : R) : S)
Tactic: obtain ⟨n, rfl | rfl⟩ := Int.eq_nat_or_neg z
Cleared hypotheses: z