awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ (↑n : R)
inl : 0 = ⌈a⌉₊ - n
inl₁ : ⌈a⌉₊ - n = 0
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
have inl₂ : ⌈a⌉₊ ≤ n
Tactic: rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
hna : (↑n : R) ≤ a
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
have inr : ⌈a - (↑n : R)⌉₊ + n = ⌈a⌉₊
Tactic: refine eq_tsub_of_add_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
hna : (↑n : R) ≤ a
⊢ ⌈a - (↑n : R)⌉₊ + n = ⌈a⌉₊
have inr : 0 ≤ a - (↑n : R)
Tactic: rw [← ceil_add_natCast, tsub_add_cancel_of_le hna]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - (↑⌊a⌋₊ : R)| ≤ 1
have refine_1 : -1 ≤ a - (↑⌊a⌋₊ : R)
Tactic: refine abs_le.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
refine_1 : -1 ≤ a - (↑⌊a⌋₊ : R)
⊢ |a - (↑⌊a⌋₊ : R)| ≤ 1
have refine_2 : a - (↑⌊a⌋₊ : R) ≤ 1
Tactic: refine abs_le.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - (↑⌈a⌉₊ : R)| ≤ 1
have refine_1 : -1 ≤ a - (↑⌈a⌉₊ : R)
Tactic: refine abs_le.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : FloorSemiring R
a : R
ha : 0 ≤ a
refine_1 : -1 ≤ a - (↑⌈a⌉₊ : R)
⊢ |a - (↑⌈a⌉₊ : R)| ≤ 1
have refine_2 : a - (↑⌈a⌉₊ : R) ≤ 1
Tactic: refine abs_le.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊
have h₀ : 0 ≤ a ↔ 0 ≤ b
Tactic: have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊
have inl : ∀ (ha : a < 0), ⌊a⌋₊ = ⌊b⌋₊
Tactic: obtain ha | ha := lt_or_ge a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
inl : ∀ (ha : a < 0), ⌊a⌋₊ = ⌊b⌋₊
⊢ ⌊a⌋₊ = ⌊b⌋₊
have inr : ∀ (ha : 0 ≤ a), ⌊a⌋₊ = ⌊b⌋₊
Tactic: obtain ha | ha := lt_or_ge a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊
have inl : 0 = ⌊b⌋₊
Tactic: rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_ge <| h₀.not.mp ha.not_ge)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
b : S
inst_6 : IsStrictOrderedRing R
inst_7 : IsStrictOrderedRing S
h : ∀ (n : ℕ), (↑n : R) ≤ a ↔ (↑n : S) ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
inl : 0 = ⌊b⌋₊
⊢ ⌊a⌋₊ = ⌊b⌋₊
have inl₁ : Eq (α := ℕ) 0 0
Tactic: rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_ge <| h₀.not.mp ha.not_ge)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
F : Type u_4
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
inst_8 : IsStrictOrderedRing R
inst_9 : IsStrictOrderedRing S
f : F
hf : StrictMono.{u_1, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℕ
⊢ LE.le.{u_3} (α := S) ((↑n : S) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
have rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
Tactic: rw [← map_natCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
F : Type u_4
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
inst_8 : IsStrictOrderedRing R
inst_9 : IsStrictOrderedRing S
f : F
hf : StrictMono.{u_1, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℕ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) (↑n : R) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
⊢ LE.le.{u_3} (α := S) ((↑n : S) : S) ((f : (a : R) → S) a : S) ↔ (↑n : R) ≤ a
have rw₁ : (↑n : R) ≤ a ↔ (↑n : R) ≤ a
Tactic: rw [← map_natCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
F : Type u_4
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_1, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℕ
⊢ LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((↑n : S) : S) ↔ a ≤ (↑n : R)
have rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑n : R) : S) ↔ a ≤ (↑n : R)
Tactic: rw [← map_natCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
S : Type u_3
inst_3 : Semiring S
inst_4 : LinearOrder S
inst_5 : FloorSemiring S
F : Type u_4
inst_6 : FunLike F R S
inst_7 : RingHomClass F R S
f : F
hf : StrictMono.{u_1, u_3} (α := R) (β := S) (⇑f : (a : R) → S)
a : R
n : ℕ
rw : LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) (↑n : R) : S) ↔ a ≤ (↑n : R)
⊢ LE.le.{u_3} (α := S) ((f : (a : R) → S) a : S) ((↑n : S) : S) ↔ a ≤ (↑n : R)
have rw₁ : a ≤ (↑n : R) ↔ a ≤ (↑n : R)
Tactic: rw [← map_natCast f, hf.le_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
⊢ Subsingleton.{u_3 + 1} (FloorSemiring R)
have refine : ∀ (H₁ H₂ : FloorSemiring R), H₁ = H₂
Tactic: refine ⟨fun H₁ H₂ => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
⊢ H₁ = H₂
have this : Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
  (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
Tactic: have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil.l_unique H₂.gc_ceil) fun n => rfl
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
⊢ Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
have h : ∀ (a : R),
  @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
⊢ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
have h : ∀ (h : a < 0),
  @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
Tactic: rcases lt_or_ge a 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h :
  ∀ (h : a < 0),
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
      @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
⊢ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
have h₁ : ∀ (h : 0 ≤ a),
  @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
Tactic: rcases lt_or_ge a 0 with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
a : R
h : 0 ≤ a
⊢ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a =
    @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
have h₁ : ∀ (n : ℕ),
  n ≤ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a ↔
    n ≤ @FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _ a
Tactic: refine eq_of_forall_le_iff fun n => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (hypothesis)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
⊢ H₁ = H₂
have this₁ : Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
  (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
Tactic: have : H₁.floor = H₂.floor := by
    ext a
    rcases lt_or_ge a 0 with h | h
    · rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h
    · refine eq_of_forall_le_iff fun n => ?_
      rw [H₁.gc_floor, H₂.gc_floor] <;> exact h
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₁ H₂ : FloorSemiring R
this_1 :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
⊢ H₁ = H₂
have mk : ∀ (floor ceil : R → ℕ) (floor_of_neg : ∀ {a : R} (ha : a < 0), floor a = 0)
  (gc_floor : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor a ↔ (↑n : R) ≤ a) (gc_ceil : GaloisConnection ceil Nat.cast)
  (this :
    Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
      (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _))
  (this :
    Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
      (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)),
  { floor := floor, ceil := ceil, floor_of_neg := @floor_of_neg, gc_floor := @gc_floor, gc_ceil := gc_ceil :
      FloorSemiring R } =
    H₂
Tactic: cases H₁
Cleared hypotheses: H₁, this_1, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
H₂ : FloorSemiring R
floor ceil : R → ℕ
floor_of_neg : ∀ {a : R} (ha : a < 0), floor a = 0
gc_floor : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor a ↔ (↑n : R) ≤ a
gc_ceil : GaloisConnection ceil Nat.cast
this_1 :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
this :
  Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
    (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
⊢ { floor := floor, ceil := ceil, floor_of_neg := @floor_of_neg, gc_floor := @gc_floor, gc_ceil := gc_ceil :
      FloorSemiring R } =
    H₂
have mk : ∀ (floor_1 ceil_1 : R → ℕ) (floor_of_neg_1 : ∀ {a : R} (ha : a < 0), floor_1 a = 0)
  (gc_floor_1 : ∀ {a : R} {n : ℕ} (ha : 0 ≤ a), n ≤ floor_1 a ↔ (↑n : R) ≤ a)
  (gc_ceil_1 : GaloisConnection ceil_1 Nat.cast)
  (this :
    Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _)
      (@FloorSemiring.ceil _ inst SemilatticeInf.toPartialOrder _))
  (this :
    Eq.{u_3 + 1} (α := R → ℕ) (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)
      (@FloorSemiring.floor _ inst SemilatticeInf.toPartialOrder _)),
  { floor := floor, ceil := ceil, floor_of_neg := @floor_of_neg, gc_floor := @gc_floor, gc_ceil := gc_ceil :
      FloorSemiring R } =
    { floor := floor_1, ceil := ceil_1, floor_of_neg := @floor_of_neg_1, gc_floor := @gc_floor_1, gc_ceil := gc_ceil_1 }
Tactic: cases H₂
Cleared hypotheses: H₂, this_1, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
⊢ |a ^ n|ₘ = |a|ₘ ^ n
have inl : ∀ (ha : a ≤ 1), |a ^ n|ₘ = |a|ₘ ^ n
Tactic: obtain ha | ha := le_total a 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
inl : ∀ (ha : a ≤ 1), |a ^ n|ₘ = |a|ₘ ^ n
⊢ |a ^ n|ₘ = |a|ₘ ^ n
have inr : ∀ (ha : 1 ≤ a), |a ^ n|ₘ = |a|ₘ ^ n
Tactic: obtain ha | ha := le_total a 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ |a ^ n|ₘ = |a|ₘ ^ n
have inl : 1 ≤ a⁻¹ ^ n
Tactic: rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
⊢ |a ^ n|ₘ = |a|ₘ ^ n
have inr : |a ^ n|ₘ = a ^ n
Tactic: rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
n : ℕ
a : G
ha : 1 ≤ a
inr : |a ^ n|ₘ = a ^ n
⊢ |a ^ n|ₘ = |a|ₘ ^ n
have inr₁ : a ^ n = a ^ n
Tactic: rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inl : ∀ (ha : 1 ≤ a), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain ha | ha := le_or_gt 1 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
inl : ∀ (ha : 1 ≤ a), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inr : ∀ (ha : a < 1), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain ha | ha := le_or_gt 1 a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inl : ∀ (hb : 1 ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain hb | hb := le_or_gt 1 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : 1 ≤ a
inl : ∀ (hb : 1 ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inl₁ : ∀ (hb : b < 1), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain hb | hb := le_or_gt 1 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inr : ∀ (hb : 1 ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain hb | hb := le_or_gt 1 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
inr : ∀ (hb : 1 ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inr₁ : ∀ (hb : b < 1), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain hb | hb := le_or_gt 1 b
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
Tactic: have : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔
    (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1) := by
    simp [ha.le, ha.not_ge, hb, mabs_of_le_one, mabs_of_one_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inr : ∀ (h : |a * b|ₘ = a⁻¹ * b), b ≤ 1
Tactic: refine this.mp ⟨fun h ↦ ?_, fun h ↦ by simp only [h.antisymm hb, mabs_of_lt_one ha, mul_one]⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
⊢ b ≤ 1
have inr : ∀ (ab : a * b ≤ 1), b ≤ 1
Tactic: obtain ab | ab := le_or_gt (a * b) 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
inr : ∀ (ab : a * b ≤ 1), b ≤ 1
⊢ b ≤ 1
have inr₁ : ∀ (ab : 1 < a * b), b ≤ 1
Tactic: obtain ab | ab := le_or_gt (a * b) 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b ≤ 1
have inr : b⁻¹ = b
Tactic: refine (eq_one_of_inv_eq' ?_).le
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b
have inr : ∀ (h : (a * b)⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
Tactic: rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h
Cleared hypotheses: h, ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
inr : ∀ (h : (a * b)⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
⊢ b⁻¹ = b
have inr₁ : ∀ (h : b⁻¹ * a⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
Tactic: rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h
Cleared hypotheses: h, ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
inr : ∀ (h : (a * b)⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
inr₁ : ∀ (h : b⁻¹ * a⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
⊢ b⁻¹ = b
have inr₂ : ∀ (h : a⁻¹ * b⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
Tactic: rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h
Cleared hypotheses: h, ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
inr : ∀ (h : (a * b)⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
inr₁ : ∀ (h : b⁻¹ * a⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
inr₂ : ∀ (h : a⁻¹ * b⁻¹ = a⁻¹ * b) (ab : a * b ≤ 1), b⁻¹ = b
⊢ b⁻¹ = b
have inr₃ : ∀ (h : b⁻¹ = b) (ab : a * b ≤ 1), b⁻¹ = b
Tactic: rwa [mabs_of_le_one ab, mul_inv_rev, mul_comm, mul_right_inj] at h
Cleared hypotheses: h, ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : 1 < a * b
⊢ b ≤ 1
have h₁ : a = a⁻¹
Tactic: rw [mabs_of_one_lt ab, mul_left_inj] at h
Cleared hypotheses: h, ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : a = a⁻¹
ab : 1 < a * b
⊢ b ≤ 1
have ha₁ : LT.lt.{u_1} (α := G) 1 1
Tactic: rw [eq_one_of_inv_eq' h.symm] at ha
Cleared hypotheses: ha, hb, this, h, ab
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Abs (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
a b : G
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
have inl : ∀ (ab : a ≤ b), |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1
Tactic: obtain ab | ab := le_total a b