awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
this_1 : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
this : x + 1 / 2 < HAdd.hAdd (α := α) (↑⌊x + 1 / 2⌋ : α) 1
linarith : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
linarith₁ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
linarith₂ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → GT.gt.{u_2} (α := α) 2 0
linarith₃ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
linarith₄ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
linarith₅ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → GT.gt.{u_2} (α := α) 2 0
linarith₆ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → 2 / 2 = 1
linarith₇ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → HMul.hMul (α := α) 1 2 = 2
linarith₈ : 1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) → GT.gt.{u_2} (α := α) 2 0
linarith₉ :
  1 / 2 < x - (↑⌊x + 1 / 2⌋ : α) →
    2 * x + HMul.hMul (α := α) 1 1 - (HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α) + HMul.hMul (α := α) 2 1) +
        (HMul.hMul (α := α) 1 1 - (2 * x - HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α))) =
      0
⊢ x - (↑⌊x + 1 / 2⌋ : α) ≤ 1 / 2

Tactic:
linarith
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
this_1 : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
this : x + 1 / 2 < HAdd.hAdd (α := α) (↑⌊x + 1 / 2⌋ : α) 1
linarith : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
linarith₁ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
linarith₂ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → GT.gt.{u_2} (α := α) 2 0
linarith₃ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
linarith₄ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
linarith₅ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → GT.gt.{u_2} (α := α) 2 0
linarith₆ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → 2 / 2 = 1
linarith₇ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → HMul.hMul (α := α) 1 2 = 2
linarith₈ : 1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x → GT.gt.{u_2} (α := α) 2 0
linarith₉ :
  1 / 2 < (↑⌊x + 1 / 2⌋ : α) - x →
    HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α) - (2 * x + HMul.hMul (α := α) 1 1) +
        (HMul.hMul (α := α) 1 1 - (HMul.hMul (α := α) 2 (↑⌊x + 1 / 2⌋ : α) - 2 * x)) =
      0
⊢ (↑⌊x + 1 / 2⌋ : α) - x ≤ 1 / 2

Tactic:
linarith
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
inl :
  |HDiv.hDiv (α := α) (↑m : α) (↑0 : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑0 : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % 0) (0 - m % 0)) : α) (↑0 : α)
inr :
  ∀ (hn : n > 0),
    |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
      HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m : ℕ
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑0 : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑0 : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % 0) (0 - m % 0)) : α) (↑0 : α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ LT.lt.{u_2} (α := α) 0 (↑n : α)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
⊢ LT.lt.{u_2} (α := α) 0 (↑n : α)

Tactic:
have hn' : 0 < (n : α) := by
    norm_cast
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
m n : ℕ
hn : n > 0
hn' : LT.lt.{u_2} (α := α) 0 (↑n : α)
inr :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)
inr₁ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    HDiv.hDiv (α := α) (min (↑(m % n) : α) (↑(n - m % n) : α)) (↑n : α)
inr₂ :
  min (fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) (1 - fract (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
inr₃ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HDiv.hDiv (α := α) (↑(n - m % n) : α) (↑n : α))
inr₄ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (HSub.hSub (α := α) (↑n : α) (↑(m % n) : α) / (↑n : α))
inr₅ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
      (HDiv.hDiv (α := α) (↑n : α) (↑n : α) - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
inr₆ inr₇ :
  min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) =
    min (HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α)) (1 - HDiv.hDiv (α := α) (↑(m % n) : α) (↑n : α))
⊢ |HDiv.hDiv (α := α) (↑m : α) (↑n : α) - (↑(round (HDiv.hDiv (α := α) (↑m : α) (↑n : α))) : α)| =
    HDiv.hDiv (α := α) (↑(min (m % n) (n - m % n)) : α) (↑n : α)

Tactic:
rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le,
    fract_div_natCast_eq_div_natCast_mod, Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']

Premises used: Nat.cast_sub, abs_sub_round_eq_min, LT.lt.le, sub_div, Nat.mod_lt, Nat.cast_min, LT.lt.ne', min_div_div_right, Int.fract_div_natCast_eq_div_natCast_mod, div_self
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
linarith : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₁ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₂ : x - 1 / 2 < x + 1 / 2 - 1 → 2 / 2 = 1
linarith₃ : x - 1 / 2 < x + 1 / 2 - 1 → HMul.hMul (α := α) 1 2 = 2
linarith₄ : x - 1 / 2 < x + 1 / 2 - 1 → GT.gt.{u_2} (α := α) 2 0
linarith₅ :
  x - 1 / 2 < x + 1 / 2 - 1 →
    2 * x - HMul.hMul (α := α) 1 1 - (2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1) = 0
linarith₆ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
linarith₇ : x + 1 / 2 - 1 < x - 1 / 2 → HMul.hMul (α := α) 1 2 = 2
linarith₈ : x + 1 / 2 - 1 < x - 1 / 2 → 2 / 2 = 1
linarith₉ : x + 1 / 2 - 1 < x - 1 / 2 → HMul.hMul (α := α) 1 2 = 2
linarith₁₀ : x + 1 / 2 - 1 < x - 1 / 2 → GT.gt.{u_2} (α := α) 2 0
linarith₁₁ :
  x + 1 / 2 - 1 < x - 1 / 2 →
    2 * x + HMul.hMul (α := α) 1 1 - HMul.hMul (α := α) 2 1 - (2 * x - HMul.hMul (α := α) 1 1) = 0
⊢ x - 1 / 2 = x + 1 / 2 - 1

Tactic:
linarith
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
rw : x + 1 / 2 - 1 < (↑⌊x + 1 / 2⌋ : α)
⊢ x - 1 / 2 < (↑(round x) : α)

Tactic:
rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]

Premises used: round_eq
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ x + 1 / 2 - 1 < (↑⌊x + 1 / 2⌋ : α)

Tactic:
Int.sub_one_lt_floor (x + 1 / 2)

Premises used: Int.sub_one_lt_floor, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ x + 1 / 2 - 1 < (↑⌊x + 1 / 2⌋ : α)

Tactic:
exact Int.sub_one_lt_floor (x + 1 / 2)

Premises used: Int.sub_one_lt_floor, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
rw : (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2
⊢ (↑(round x) : α) ≤ x + 1 / 2

Tactic:
rw [round_eq x]

Premises used: round_eq
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2

Tactic:
Int.floor_le (x + 1 / 2)

Premises used: HDiv.hDiv, HAdd.hAdd, Int.floor_le, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Round
Goal:
α : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
x : α
⊢ (↑⌊x + 1 / 2⌋ : α) ≤ x + 1 / 2

Tactic:
exact Int.floor_le (x + 1 / 2)

Premises used: HDiv.hDiv, HAdd.hAdd, Int.floor_le, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Round
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : LinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : FloorRing α
inst_7 : FloorRing β
inst_8 : FunLike F α β
inst_9 : RingHomClass F α β
f : F
hf : StrictMono.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
a : α
simp_rw : ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = ⌊a + 1 / 2⌋
simp_rw₁ :
  ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ = floor.{u_3} (α := β) ((f : (a : α) → β) (a + 1 / 2) : β)
simp_rw₂ :
  ⌊HAdd.hAdd (α := β) ((f : (a : α) → β) a : β) (1 / 2)⌋ =
    ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (1 / 2) : β)⌋
simp_rw₃ :
  ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) (2⁻¹ : β)⌋ =
    ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) 2⁻¹ : β)⌋
simp_rw₄ :
  ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) (2⁻¹ : β)⌋ =
    ⌊HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) (((f : (a : α) → β) 2)⁻¹ : β)⌋
⊢ round.{u_3} (α := β) ((f : (a : α) → β) a : β) = round a

Tactic:
simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]

Premises used: map_ofNat, map_inv₀, map_add, round_eq, Int.map_floor, one_div
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r : R
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 a)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r : R
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r₁ r₂ : R
hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₁
hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₂
hr₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₁ • a)
hr₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₂ • a)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) ((r₁ + r₂) • a)

Tactic:
simpa [add_smul] using add_mem hr₁ hr₂

Premises used: add_smul, AddMemClass.add_mem
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a : A
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul (β := A) r 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a : A
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
a₁ a₂ : A
hx : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₁
hy : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₂
ha₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₁)
ha₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₂)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • (a₁ + a₂))

Tactic:
simpa [smul_add] using add_mem ha₁ ha₂

Premises used: AddMemClass.add_mem, smul_add
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a_1 : A
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
a : A
ha : Membership.mem (γ := Set A) (range fun (s : A) ↦ star s * s) a
mem :
  ∀ (r : R),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (s : R) ↦ star s * s) r) a)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)

Tactic:
obtain ⟨r, rfl⟩ := hr

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a_1 a : A
ha : Membership.mem (γ := Set A) (range fun (s : A) ↦ star s * s) a
r : R
mem :
  ∀ (a : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((fun (s : R) ↦ star s * s) r) ((fun (s : A) ↦ star s * s) a))
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((fun (s : R) ↦ star s * s) r) a)

Tactic:
obtain ⟨a, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a_1 : A
r : R
a : A
⊢ (fun (s : A) ↦ star s * s) (r • a) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((fun (s : R) ↦ star s * s) r) ((fun (s : A) ↦ star s * s) a)

Tactic:
simp [star_smul, smul_mul_smul_comm]

Premises used: StarModule.star_smul, smul_mul_smul_comm
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a_1 : A
r : R
a : A
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((fun (s : R) ↦ star s * s) r) ((fun (s : A) ↦ star s * s) a))

Tactic:
exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r_1 : R
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
r : R
hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r
mem :
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul (β := A) r 0)
mem₁ :
  ∀ (a₁ a₂ : A),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₁ →
      Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a₂ →
        ∀ (ha₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₁))
          (ha₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a₂)),
          Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • (a₁ + a₂))
mem₂ :
  ∀ (a : A) (ha : Membership.mem (γ := Set A) (range fun (s : A) ↦ star s * s) a),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)

Tactic:
induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩

Premises used: smul_add, rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : IsScalarTower R A A
inst_7 : SMulCommClass R A A
r : R
hr : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r
a : A
ha : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) a
zero :
  Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 a)
add :
  ∀ (r₁ r₂ : R),
    Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₁ →
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) r₂ →
        ∀ (hr₁ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₁ • a))
          (hr₂ : Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r₂ • a)),
          Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) ((r₁ + r₂) • a)
mem :
  ∀ (r : R) (hr : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) r),
    Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)
⊢ Membership.mem (γ := AddSubmonoid A) (AddSubmonoid.closure (range fun (s : A) ↦ star s * s)) (r • a)

Tactic:
induction hr using AddSubmonoid.closure_induction with
  | zero => simp
  | add r₁ r₂ _ _ hr₁ hr₂ => simpa [add_smul] using add_mem hr₁ hr₂
  | mem r hr =>
  induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩

Premises used: add_smul, smul_add, rfl
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y : R
⊢ x ≤ y ↔
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y : R
refine_1 :
  ∀ (h : x ≤ y),
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
refine_2 :
  (∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p) →
    x ≤ y
⊢ x ≤ y ↔
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
refine ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y : R
h : x ≤ y
refine_1 :
  ∀ (p : R) (hp : y = x + star p * p),
    ∃ (p : R),
      Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p
⊢ ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
obtain ⟨p, hp⟩ := (h_le_iff x y).mp h

Premises used: Iff.mp
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y : R
h : x ≤ y
p : R
hp : y = x + star p * p
⊢ ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩

Premises used: HMul.hMul, AddSubmonoid.subset_closure, And.intro, Exists.intro, rfl, Star.star
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y : R
h : x ≤ y
p : R
hp : y = x + star p * p
⊢ ∃ (p : R), Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p ∧ y = x + p

Tactic:
exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
x y p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
hpxy : y = x + p
refine_2 : ∀ (x y : R) (hpxy : y = x + p), x ≤ y
⊢ x ≤ y

Tactic:
revert x y hpxy
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
⊢ ∀ (x y : R) (hpxy : y = x + p), x ≤ y

Tactic:
AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp

Premises used: AddSubmonoid.closure_induction
-- Module: Mathlib.Algebra.Order.Star.Basic
Goal:
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : PartialOrder R
inst_2 : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ (s : R), y = x + star s * s
p : R
hp : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) p
refine_2 :
  ∀ (x : R) (h : Membership.mem (γ := Set R) (range fun (s : R) ↦ star s * s) x) (x_1 y : R) (hpxy : y = x_1 + x),
    x_1 ≤ y
refine_2₁ :
  ∀ (x y : R) (hx : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) x)
    (hy : Membership.mem (γ := AddSubmonoid R) (AddSubmonoid.closure (range fun (s : R) ↦ star s * s)) y),
    (∀ (x_1 y : R) (hpxy : y = x_1 + x), x_1 ≤ y) →
      (∀ (x y_1 : R) (hpxy : y_1 = x + y), x ≤ y_1) → ∀ (x_1 y_1 : R) (hpxy : y_1 = x_1 + (x + y)), x_1 ≤ y_1
⊢ ∀ (x y : R) (hpxy : y = x + p), x ≤ y

Tactic:
refine AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp