awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
R : Type u_1
inst : Ring R
toSubsemiring : Subsemiring R
eq_zero_of_mem_of_neg_mem : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0
⊢ (↑{ toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := @eq_zero_of_mem_of_neg_mem : RingCone R } : Set R) =
    (↑toSubsemiring : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
T : Type u_1
inst : Ring T
inst_1 : PartialOrder T
inst_2 : IsOrderedRing T
a_1 a : T
⊢ a ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subsemiring.nonneg T))) →
    -a ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subsemiring.nonneg T))) → a = 0

Tactic:
simpa using ge_antisymm

Premises used: ge_antisymm
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
T : Type u_1
inst : Ring T
inst_1 : PartialOrder T
inst_2 : IsOrderedRing T
⊢ Eq (α := Subsemiring T) (toSubsemiring (nonneg T)) (Subsemiring.nonneg T)

Tactic:
rfl

Premises used: Subsemiring.nonneg, rfl
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
T : Type u_1
inst : Ring T
inst_1 : PartialOrder T
inst_2 : IsOrderedRing T
⊢ Eq (α := AddGroupCone T) (toAddGroupCone (nonneg T)) (AddGroupCone.nonneg T)

Tactic:
rfl

Premises used: Set.Ici, setOf, AddSubmonoid.nonneg, rfl, AddGroupCone.nonneg
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
T : Type u_1
inst : Ring T
inst_1 : PartialOrder T
inst_2 : IsOrderedRing T
a : T
⊢ Membership.mem (γ := RingCone T) (nonneg T) a ↔ 0 ≤ a

Tactic:
Iff.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
T : Type u_1
inst : Ring T
inst_1 : PartialOrder T
inst_2 : IsOrderedRing T
⊢ (↑(nonneg T) : Set T) = {x : T | 0 ≤ x}

Tactic:
rfl

Premises used: Set.Ici, setOf, rfl
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
S : Type u_1
R : Type u_2
inst : Ring R
inst_1 : SetLike S R
C : S
inst_2 : RingConeClass S R
x : PartialOrder R := PartialOrder.mkOfAddGroupCone C
this : IsOrderedAddMonoid R
⊢ HSub.hSub (α := R) 1 0 ∈ C

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Cone
Goal:
S : Type u_1
R : Type u_2
inst : Ring R
inst_1 : SetLike S R
C : S
inst_2 : RingConeClass S R
x_1 : PartialOrder R := PartialOrder.mkOfAddGroupCone C
this_1 : IsOrderedAddMonoid R
this : ZeroLEOneClass R
x y : R
xnn : 0 ≤ x
ynn : 0 ≤ y
⊢ x * y - 0 ∈ C

Tactic:
simpa using mul_mem xnn ynn

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
simpa only [mul_sub, sub_nonneg] using mul_nonneg _ _ ha (sub_nonneg.2 hbc)

Premises used: Iff.mpr, mul_sub, sub_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : ZeroLEOneClass R
mul_nonneg : ∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
a : R
ha : 0 ≤ a
b c : R
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
simpa only [sub_mul, sub_nonneg] using mul_nonneg _ _ (sub_nonneg.2 hbc) ha

Premises used: Iff.mpr, sub_mul, sub_nonneg
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : ZeroLEOneClass R
inst_4 : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ a * b < a * c

Tactic:
simpa only [mul_sub, sub_pos] using mul_pos _ _ ha (sub_pos.2 hbc)

Premises used: Iff.mpr, sub_pos, mul_sub
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : ZeroLEOneClass R
inst_4 : Nontrivial R
mul_pos : ∀ (a b : R), 0 < a → 0 < b → 0 < a * b
a : R
ha : 0 < a
b c : R
hbc : b < c
⊢ b * a < c * a

Tactic:
simpa only [sub_mul, sub_pos] using mul_pos _ _ (sub_pos.2 hbc) ha

Premises used: Iff.mpr, sub_pos, sub_mul
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R_1 : Type u
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
⊢ IsStrictOrderedRing R

Tactic:
.of_mul_pos fun _ _ ap bp ↦ (mul_nonneg ap.le bp.le).lt_of_ne' (mul_ne_zero ap.ne' bp.ne')

Premises used: mul_nonneg, LT.lt.le, LT.lt.ne', IsStrictOrderedRing.of_mul_pos, mul_ne_zero, LE.le.lt_of_ne'
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u_1} (R := R) 1
inst_4 : AddLeftStrictMono R
n : ℕ
rw : (↑n : R) < HAdd.hAdd (α := R) (↑n : R) 1
⊢ LT.lt.{u_1} (α := R) (↑n : R) (↑(n + 1) : R)

Tactic:
rw [Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u_1
inst : AddMonoidWithOne R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : NeZero.{u_1} (R := R) 1
inst_4 : AddLeftStrictMono R
n : ℕ
⊢ (↑n : R) < HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
apply lt_add_one

Premises used: lt_add_one
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
⊢ CharZero R

Tactic:
AddMonoidWithOne.toCharZero

Premises used: AddMonoidWithOne.toCharZero
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
⊢ NoMaxOrder R

Tactic:
⟨fun a => ⟨a + 1, lt_add_of_pos_right _ one_pos⟩⟩

Premises used: lt_add_of_pos_right, NoMaxOrder.mk, HAdd.hAdd, Exists.intro, OfNat.ofNat, one_pos
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a * b = 0
contrapose! : ∀ (hab : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! hab
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
inl : ∀ (ha : a < 0), a * b ≠ 0
inr : ∀ (ha : 0 < a), a * b ≠ 0
⊢ a * b ≠ 0

Tactic:
obtain ha | ha := hab.1.lt_or_gt

Premises used: And.left, Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
inl : ∀ (hb : b < 0), a * b ≠ 0
inl₁ : ∀ (hb : 0 < b), a * b ≠ 0
⊢ a * b ≠ 0

Tactic:
obtain hb | hb := hab.2.lt_or_gt

Premises used: And.right, Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
inr : ∀ (hb : b < 0), a * b ≠ 0
inr₁ : ∀ (hb : 0 < b), a * b ≠ 0
⊢ a * b ≠ 0

Tactic:
obtain hb | hb := hab.2.lt_or_gt

Premises used: And.right, Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
hb : b < 0
⊢ a * b ≠ 0

Tactic:
(mul_pos_of_neg_of_neg ha hb).ne'

Premises used: LT.lt.ne', mul_pos_of_neg_of_neg
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
hb : 0 < b
⊢ a * b ≠ 0

Tactic:
(mul_neg_of_neg_of_pos ha hb).ne

Premises used: mul_neg_of_neg_of_pos, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
hb : b < 0
⊢ a * b ≠ 0

Tactic:
(mul_neg_of_pos_of_neg ha hb).ne

Premises used: mul_neg_of_pos_of_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
hb : 0 < b
⊢ a * b ≠ 0

Tactic:
(mul_pos ha hb).ne'

Premises used: LT.lt.ne', mul_pos
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
hb : b < 0
⊢ a * b ≠ 0

Tactic:
exacts [(mul_pos_of_neg_of_neg ha hb).ne', (mul_neg_of_neg_of_pos ha hb).ne,
      (mul_neg_of_pos_of_neg ha hb).ne, (mul_pos ha hb).ne']

Premises used: mul_neg_of_neg_of_pos, LT.lt.ne', mul_pos, mul_pos_of_neg_of_neg, mul_neg_of_pos_of_neg, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
inl : ∀ (ha : a < 0), x = x_1
inr : ∀ (ha : 0 < a), x = x_1
⊢ x = x_1

Tactic:
obtain ha | ha := ha.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha_1 : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
ha : a < 0
⊢ x = x_1

Tactic:
(strictAnti_mul_left ha).injective h

Premises used: strictAnti_mul_left, StrictAnti.injective
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha_1 : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
ha : 0 < a
⊢ x = x_1

Tactic:
(strictMono_mul_left_of_pos ha).injective h

Premises used: strictMono_mul_left_of_pos, StrictMono.injective
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha_1 : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ a * x) x) ((fun (x : R) ↦ a * x) x_1)
ha : a < 0
⊢ x = x_1

Tactic:
exacts [(strictAnti_mul_left ha).injective h, (strictMono_mul_left_of_pos ha).injective h]

Premises used: strictAnti_mul_left, strictMono_mul_left_of_pos, StrictMono.injective, StrictAnti.injective
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
inl : ∀ (ha : a < 0), x = x_1
inr : ∀ (ha : 0 < a), x = x_1
⊢ x = x_1

Tactic:
obtain ha | ha := ha.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha_1 : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
ha : a < 0
⊢ x = x_1

Tactic:
(strictAnti_mul_right ha).injective h

Premises used: strictAnti_mul_right, StrictAnti.injective
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha_1 : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
ha : 0 < a
⊢ x = x_1

Tactic:
(strictMono_mul_right_of_pos ha).injective h

Premises used: strictMono_mul_right_of_pos, StrictMono.injective
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
a : R
ha_1 : a ≠ 0
x x_1 : R
h : Eq.{u + 1} (α := R) ((fun (x : R) ↦ x * a) x) ((fun (x : R) ↦ x * a) x_1)
ha : a < 0
⊢ x = x_1

Tactic:
exacts [(strictAnti_mul_right ha).injective h, (strictMono_mul_right_of_pos ha).injective h]

Premises used: strictAnti_mul_right, strictMono_mul_right_of_pos, StrictMono.injective, StrictAnti.injective
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
rw : 1 + (a + b + b * c) ≤ 1 + c
⊢ 1 + a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]

Premises used: add_assoc, one_sub_mul, le_sub_iff_add_le, mul_one_add
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : a + b + b * c ≤ c
⊢ 1 + (a + b + b * c) ≤ 1 + c

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
rw : 1 + (a + c + b * c) ≤ 1 + b
⊢ 1 + a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, le_sub_iff_add_le, add_assoc, ← add_assoc a]

Premises used: add_assoc, mul_one_sub, one_add_mul, le_sub_iff_add_le
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + (a + c + b * c) ≤ 1 + b

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
rw : 1 + (b + b * c) ≤ 1 + (a + c)
⊢ 1 - a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, sub_le_sub_iff, add_assoc, add_comm c]

Premises used: add_assoc, one_sub_mul, add_comm, sub_le_sub_iff, mul_one_add
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (a + c)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
rw : 1 + (c + b * c) ≤ 1 + (a + b)
⊢ 1 - a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]

Premises used: add_assoc, mul_one_sub, add_comm, sub_le_sub_iff, one_add_mul
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 + (c + b * c) ≤ 1 + (a + b)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
⊢ CharZero R

Tactic:
AddMonoidWithOne.toCharZero

Premises used: AddMonoidWithOne.toCharZero
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a_1 b c : R
inst_3 : Nontrivial R
a : R
⊢ a < a + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Defs
Goal:
R : Type u
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
a_1 b c : R
inst_3 : Nontrivial R
a : R
⊢ a - 1 < a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
s : Finset ι
f : ι → ℕ
hs : s.Nonempty
⊢ Eq.{u_2 + 1} (α := R) (↑(s.sup' hs f) : R) (s.sup' hs fun (i : ι) ↦ (↑(f i) : R))

Tactic:
comp_sup'_eq_sup'_comp _ _ cast_max

Premises used: Nat.cast_max, Finset.comp_sup'_eq_sup'_comp
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
s : Finset ι
f : ι → ℕ
hs : s.Nonempty
⊢ Eq.{u_2 + 1} (α := R) (↑(s.inf' hs f) : R) (s.inf' hs fun (i : ι) ↦ (↑(f i) : R))

Tactic:
comp_inf'_eq_inf'_comp _ _ cast_min

Premises used: Nat.cast_min, Finset.comp_inf'_eq_inf'_comp
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : OrderBot R
inst_4 : CanonicallyOrderedAdd R
s : Finset ι
f : ι → ℕ
⊢ Eq.{u_2 + 1} (α := R) (↑⊥ : R) ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
f : ι → R
a : R
⊢ a * sup ∅ f = sup ∅ fun (x : ι) ↦ a * f x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
f : ι → R
a : R
a_1 : ι
s : Finset ι
h : a_1 ∉ s
IH : a * s.sup f = s.sup fun (x : ι) ↦ a * f x
⊢ a * (insert a_1 s).sup f = (insert a_1 s).sup fun (x : ι) ↦ a * f x

Tactic:
simp only [sup_insert, mul_max, ← IH]

Premises used: Finset.sup_insert, mul_max
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : a * sup ∅ f = sup ∅ fun (x : ι) ↦ a * f x
insert :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      ∀ (IH : a * s.sup f = s.sup fun (x : ι) ↦ a * f x),
        a * (Insert.insert a_1 s).sup f = (Insert.insert a_1 s).sup fun (x : ι) ↦ a * f x
⊢ a * s.sup f = s.sup fun (x : ι) ↦ a * f x

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, mul_max, ← IH]

Premises used: Finset.sup_insert, Insert.insert, mul_max
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : a * sup ∅ f = sup ∅ fun (x : ι) ↦ a * f x
insert :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      ∀ (IH : a * s.sup f = s.sup fun (x : ι) ↦ a * f x),
        a * (Insert.insert a_1 s).sup f = (Insert.insert a_1 s).sup fun (x : ι) ↦ a * f x
⊢ a * s.sup f = s.sup fun (x : ι) ↦ a * f x

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, mul_max, ← IH]

Premises used: Finset.sup_insert, Insert.insert, mul_max
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
f : ι → R
a : R
⊢ sup ∅ f * a = sup ∅ fun (x : ι) ↦ f x * a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
f : ι → R
a : R
a_1 : ι
s : Finset ι
h : a_1 ∉ s
IH : s.sup f * a = s.sup fun (x : ι) ↦ f x * a
⊢ (insert a_1 s).sup f * a = (insert a_1 s).sup fun (x : ι) ↦ f x * a

Tactic:
simp only [sup_insert, max_mul, ← IH]

Premises used: Finset.sup_insert, max_mul
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : sup ∅ f * a = sup ∅ fun (x : ι) ↦ f x * a
insert :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      ∀ (IH : s.sup f * a = s.sup fun (x : ι) ↦ f x * a),
        (Insert.insert a_1 s).sup f * a = (Insert.insert a_1 s).sup fun (x : ι) ↦ f x * a
⊢ s.sup f * a = s.sup fun (x : ι) ↦ f x * a

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]

Premises used: Finset.sup_insert, Insert.insert, max_mul
-- Module: Mathlib.Algebra.Order.Ring.Finset
Goal:
R : Type u_1
ι : Type u_2
inst : LinearOrder R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : CanonicallyOrderedAdd R
inst_3 : OrderBot R
s : Finset ι
f : ι → R
a : R
empty : sup ∅ f * a = sup ∅ fun (x : ι) ↦ f x * a
insert :
  ∀ (a_1 : ι) (s : Finset ι),
    a_1 ∉ s →
      ∀ (IH : s.sup f * a = s.sup fun (x : ι) ↦ f x * a),
        (Insert.insert a_1 s).sup f * a = (Insert.insert a_1 s).sup fun (x : ι) ↦ f x * a
⊢ s.sup f * a = s.sup fun (x : ι) ↦ f x * a

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ IH => simp only [sup_insert, max_mul, ← IH]

Premises used: Finset.sup_insert, Insert.insert, max_mul
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 ≤ x
hn : n ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) x 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
n : ℕ
⊢ x ≤ 0

Tactic:
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
⊢ if Even (α := ℕ) 0 then LE.le.{u_1} (α := R) (∑ i ∈ range 0, x ^ i) 0
  else LE.le.{u_1} (α := R) 1 (∑ i ∈ range 0, x ^ i)

Tactic:
simp only [range_zero, sum_empty, le_refl, ite_true, Even.zero]

Premises used: le_refl, Even.zero, ite_true, Finset.sum_empty, Finset.range_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
succ : if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
⊢ if Even (n + 1) then LE.le.{u_1} (α := R) (∑ i ∈ range (n + 1), x ^ i) 0
  else LE.le.{u_1} (α := R) 1 (∑ i ∈ range (n + 1), x ^ i)

Tactic:
simp only [Nat.even_add_one, geom_sum_succ]

Premises used: Nat.even_add_one, geom_sum_succ
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 else LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
pos : ∀ (h : Even n) (ih : LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0), 1 ≤ x * ∑ i ∈ range n, x ^ i + 1
neg : ∀ (h : ¬Even n) (ih : LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)), x * ∑ i ∈ range n, x ^ i + 1 ≤ 0
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Tactic:
split_ifs at ih ⊢ with h
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
pos : 0 ≤ x * ∑ i ∈ range n, x ^ i
⊢ 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Tactic:
rw [le_add_iff_nonneg_left]

Premises used: le_add_iff_nonneg_left
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i

Tactic:
mul_nonneg_of_nonpos_of_nonpos hx0 ih

Premises used: mul_nonneg_of_nonpos_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i

Tactic:
exact mul_nonneg_of_nonpos_of_nonpos hx0 ih

Premises used: mul_nonneg_of_nonpos_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
neg : x * ∑ i ∈ range n, x ^ i + 1 ≤ x + 1
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Tactic:
grw [← hx]
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
neg : x * ∑ i ∈ range n, x ^ i ≤ x
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ x + 1

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : R
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : LE.le.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
⊢ x * ∑ i ∈ range n, x ^ i ≤ x

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

Premises used: mul_le_mul_of_nonpos_left, mul_one