awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
rwa : ∀ (this : b ^ m < b ^ (m + 1)), 1 < b
rwa₁ : ∀ (this : b ^ m * 1 < b ^ (m + 1)), 1 < b
rwa₂ : ∀ (this : b ^ m * 1 < b ^ m * b), 1 < b
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : 1 < b), 1 < b
⊢ 1 < b

Tactic:
rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this

Premises used: mul_lt_mul_iff_left, zpow_add_one, HPow.hPow, mul_one
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b

Tactic:
have hb : 1 < b := by
    have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
    rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ a * b ^ m < a * b ^ (n + 1)

Tactic:
have i1 := hx.1.1.trans_lt hx.2.2
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ a * b ^ n < a * b ^ (m + 1)

Tactic:
have i2 := hx.2.1.trans_lt hx.1.2
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m ≤ n

Tactic:
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2

Premises used: zpow_lt_zpow_iff_right, mul_lt_mul_iff_left, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
i1₁ : m ≤ n
⊢ n ≤ m

Tactic:
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff_right hb, Int.lt_add_one_iff] at i1 i2

Premises used: zpow_lt_zpow_iff_right, mul_lt_mul_iff_left, Int.lt_add_one_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m ≤ n
i2 : n ≤ m
⊢ m = n

Tactic:
le_antisymm i1 i2

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m ≤ n
i2 : n ≤ m
⊢ m = n

Tactic:
exact le_antisymm i1 i2

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ Pairwise (α := ℤ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ioo (a * b ^ n) (a * b ^ (n + 1)))

Tactic:
fun _ _ hmn =>
  (pairwise_disjoint_Ioc_mul_zpow a b hmn).mono Ioo_subset_Ioc_self Ioo_subset_Ioc_self

Premises used: Set.pairwise_disjoint_Ioc_mul_zpow, Set.Ioo_subset_Ioc_self, Pairwise, Disjoint.mono
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
b : α
⊢ Pairwise (α := ℤ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ioc (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b

Premises used: Set.pairwise_disjoint_Ioc_mul_zpow, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
b : α
⊢ Pairwise (α := ℤ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ico (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ico_mul_zpow 1 b

Premises used: Set.pairwise_disjoint_Ico_mul_zpow, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
b : α
⊢ Pairwise (α := ℤ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ioo (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ioo_mul_zpow 1 b

Premises used: Set.pairwise_disjoint_Ioo_mul_zpow, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a : α
⊢ Pairwise (α := ℤ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ioc (a + (↑n : α)) (a + (↑n : α) + 1))

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ioc_add_zsmul a (1 : α)

Premises used: add_assoc, Set.pairwise_disjoint_Ioc_add_zsmul, Int.cast_add, zsmul_one, OfNat.ofNat, Int.cast_one
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a : α
⊢ Pairwise (α := ℤ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ico (a + (↑n : α)) (a + (↑n : α) + 1))

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ico_add_zsmul a (1 : α)

Premises used: add_assoc, Int.cast_add, zsmul_one, OfNat.ofNat, Set.pairwise_disjoint_Ico_add_zsmul, Int.cast_one
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
a : α
⊢ Pairwise (α := ℤ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ioo (a + (↑n : α)) (a + (↑n : α) + 1))

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ioo_add_zsmul a (1 : α)

Premises used: Set.pairwise_disjoint_Ioo_add_zsmul, add_assoc, Int.cast_add, zsmul_one, OfNat.ofNat, Int.cast_one
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
⊢ Pairwise (α := ℤ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ico (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1))

Tactic:
simpa only [zero_add] using pairwise_disjoint_Ico_add_intCast (0 : α)

Premises used: Set.pairwise_disjoint_Ico_add_intCast, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
⊢ Pairwise (α := ℤ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ioo (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1))

Tactic:
simpa only [zero_add] using pairwise_disjoint_Ioo_add_intCast (0 : α)

Premises used: Set.pairwise_disjoint_Ioo_add_intCast, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Interval.Set.Group
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsOrderedRing α
⊢ Pairwise (α := ℤ)
    (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℤ) ↦ Ioc (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1))

Tactic:
simpa only [zero_add] using pairwise_disjoint_Ioc_add_intCast (0 : α)

Premises used: zero_add, Set.pairwise_disjoint_Ioc_add_intCast, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
⊢ ZeroLEOneClass.{u_1} (↑(Icc 0 1) : Type u_1)

Tactic:
⟨Subtype.coe_le_coe.mp zero_le_one⟩

Premises used: ZeroLEOneClass.mk, Subtype.coe_le_coe, zero_le_one, Iff.mp
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
h : Membership.mem (γ := Set R) (Icc 0 1) 0
⊢ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Icc 0 1) x) 0 h = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
h : Membership.mem (γ := Set R) (Icc 0 1) 1
⊢ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Icc 0 1) x) 1 h = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
symm : x = 0 ↔ (↑x : R) = 0
⊢ (↑x : R) = 0 ↔ x = 0

Tactic:
symm
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ x = 0 ↔ (↑x : R) = 0

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ x = 0 ↔ (↑x : R) = 0

Tactic:
exact Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ (↑x : R) ≠ 0 ↔ x ≠ 0

Tactic:
not_iff_not.mpr coe_eq_zero

Premises used: not_iff_not, Iff.mpr, Set.Icc.coe_eq_zero
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
symm : x = 1 ↔ (↑x : R) = 1
⊢ (↑x : R) = 1 ↔ x = 1

Tactic:
symm
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ x = 1 ↔ (↑x : R) = 1

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ x = 1 ↔ (↑x : R) = 1

Tactic:
exact Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
⊢ (↑x : R) ≠ 1 ↔ x ≠ 1

Tactic:
not_iff_not.mpr coe_eq_one

Premises used: not_iff_not, Iff.mpr, Set.Icc.coe_eq_one
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Icc 0 1) : Type u_1)
⊢ 0 ≤ (↑x : R)

Tactic:
x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Icc 0 1) : Type u_1)
⊢ (↑x : R) ≤ 1

Tactic:
x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
t : (↑(Icc 0 1) : Type u_1)
⊢ 0 ≤ t

Tactic:
t.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
t : (↑(Icc 0 1) : Type u_1)
⊢ t ≤ 1

Tactic:
t.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : (↑(Icc 0 1) : Type u_1)
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x : (↑(Icc 0 1) : Type u_1)
n : ℕ
⊢ (↑(x ^ n) : R) = (↑x : R) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : (↑(Icc 0 1) : Type u_1)
⊢ x * y ≤ x

Tactic:
(mul_le_mul_of_nonneg_left y.2.2 x.2.1).trans_eq (mul_one _)

Premises used: LE.le.trans_eq, And.right, And.left, mul_one, mul_le_mul_of_nonneg_left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : (↑(Icc 0 1) : Type u_1)
⊢ x * y ≤ y

Tactic:
(mul_le_mul_of_nonneg_right x.2.2 y.2.1).trans_eq (one_mul _)

Premises used: LE.le.trans_eq, mul_le_mul_of_nonneg_right, And.right, And.left, one_mul, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R_1 : Type u_1
inst : Semiring R_1
inst_1 : PartialOrder R_1
inst_2 : IsOrderedRing R_1
R : Type u_2
inst_3 : Ring R
inst_4 : PartialOrder R
inst_5 : IsOrderedRing R
inst_6 : NoZeroDivisors R
⊢ IsCancelMulZero.{u_2} (↑(Icc 0 1) : Type u_2)

Tactic:
@Function.Injective.isCancelMulZero _ R _ _ _ _ _ Subtype.coe_injective coe_zero coe_mul
    NoZeroDivisors.toIsCancelMulZero

Premises used: Function.Injective.isCancelMulZero, Set.Icc.coe_zero, Set.Icc.coe_mul, Subtype.coe_injective
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
t : β
ht : Membership.mem (γ := Set β) (Icc 0 1) t
⊢ 0 ≤ t ∧ t ≤ 1

Tactic:
rw [mem_Icc] at *

Premises used: Set.mem_Icc
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1

Tactic:
⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩

Premises used: Iff.mpr, And.right, And.left, And.intro, sub_nonneg, sub_le_self_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1

Tactic:
exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
t : β
⊢ Membership.mem (γ := Set β) (Icc 0 1) t ↔ Membership.mem (γ := Set β) (Icc 0 1) (1 - t)

Tactic:
⟨one_sub_mem, fun h => sub_sub_cancel 1 t ▸ one_sub_mem h⟩

Premises used: Set.Icc.one_sub_mem, Eq.rec, sub_sub_cancel, Iff.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
x : (↑(Icc 0 1) : Type u_2)
⊢ 0 ≤ 1 - (↑x : β)

Tactic:
simpa using x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
x : (↑(Icc 0 1) : Type u_2)
⊢ 1 - (↑x : β) ≤ 1

Tactic:
simpa using x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
⊢ Membership.mem (γ := Set R) (Ico 0 1) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) (↑0 : R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
h : Membership.mem (γ := Set R) (Ico 0 1) 0
⊢ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ico 0 1) x) 0 h = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
x : (↑(Ico 0 1) : Type u_1)
symm : x = 0 ↔ (↑x : R) = 0
⊢ (↑x : R) = 0 ↔ x = 0

Tactic:
symm
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
x : (↑(Ico 0 1) : Type u_1)
⊢ x = 0 ↔ (↑x : R) = 0

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
x : (↑(Ico 0 1) : Type u_1)
⊢ x = 0 ↔ (↑x : R) = 0

Tactic:
exact Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
x : (↑(Ico 0 1) : Type u_1)
⊢ (↑x : R) ≠ 0 ↔ x ≠ 0

Tactic:
not_iff_not.mpr coe_eq_zero

Premises used: not_iff_not, Iff.mpr, Set.Ico.coe_eq_zero
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Ico 0 1) : Type u_1)
⊢ 0 ≤ (↑x : R)

Tactic:
x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Ico 0 1) : Type u_1)
⊢ (↑x : R) < 1

Tactic:
x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Nontrivial R
t : (↑(Ico 0 1) : Type u_1)
⊢ 0 ≤ t

Tactic:
t.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
x y : (↑(Ico 0 1) : Type u_1)
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
h : Membership.mem (γ := Set R) (Ioc 0 1) 1
⊢ Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Set R) (Ioc 0 1) x) 1 h = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x : (↑(Ioc 0 1) : Type u_1)
symm : x = 1 ↔ (↑x : R) = 1
⊢ (↑x : R) = 1 ↔ x = 1

Tactic:
symm
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x : (↑(Ioc 0 1) : Type u_1)
⊢ x = 1 ↔ (↑x : R) = 1

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x : (↑(Ioc 0 1) : Type u_1)
⊢ x = 1 ↔ (↑x : R) = 1

Tactic:
exact Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x : (↑(Ioc 0 1) : Type u_1)
⊢ (↑x : R) ≠ 1 ↔ x ≠ 1

Tactic:
not_iff_not.mpr coe_eq_one

Premises used: not_iff_not, Iff.mpr, Set.Ioc.coe_eq_one
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Ioc 0 1) : Type u_1)
⊢ 0 < (↑x : R)

Tactic:
x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Ioc 0 1) : Type u_1)
⊢ (↑x : R) ≤ 1

Tactic:
x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
t : (↑(Ioc 0 1) : Type u_1)
⊢ t ≤ 1

Tactic:
t.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x y : (↑(Ioc 0 1) : Type u_1)
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x : (↑(Ioc 0 1) : Type u_1)
n : ℕ
⊢ (↑(x ^ n) : R) = (↑x : R) ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Ioo 0 1) : Type u_1)
⊢ 0 < (↑x : R)

Tactic:
x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
x : (↑(Ioo 0 1) : Type u_1)
⊢ (↑x : R) < 1

Tactic:
x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
x y : (↑(Ioo 0 1) : Type u_1)
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
t : β
ht : Membership.mem (γ := Set β) (Ioo 0 1) t
⊢ Membership.mem (γ := Set β) (Ioo 0 1) (1 - t)

Tactic:
simp_all only [mem_Ioo, sub_pos, sub_lt_self_iff, and_self]

Premises used: sub_pos, Set.mem_Ioo, and_self, sub_lt_self_iff
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
t : β
⊢ Membership.mem (γ := Set β) (Ioo 0 1) t ↔ Membership.mem (γ := Set β) (Ioo 0 1) (1 - t)

Tactic:
⟨one_sub_mem, fun h => sub_sub_cancel 1 t ▸ one_sub_mem h⟩

Premises used: Eq.rec, sub_sub_cancel, Set.Ioo.one_sub_mem, Iff.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
x : (↑(Ioo 0 1) : Type u_2)
⊢ 0 < 1 - (↑x : β)

Tactic:
simpa using x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Instances
Goal:
β : Type u_2
inst : Ring β
inst_1 : PartialOrder β
inst_2 : IsOrderedRing β
x : (↑(Ioo 0 1) : Type u_2)
⊢ 1 - (↑x : β) < 1

Tactic:
simpa using x.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
⊢ MapsTo (fun (x : M) ↦ x + d) (Ici a) (Ici (a + d))

Tactic:
simp [MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
⊢ InjOn (β := M) (fun (x : M) ↦ x + d) (Ici a)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Interval.Set.Monoid
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelAddMonoid M
inst_3 : ExistsAddOfLE M
a d : M
refine : ∀ (x : M) (h : x ∈ Ici (a + d)), Membership.mem (γ := Set M) ((fun (x : M) ↦ x + d) '' Ici a) x
⊢ BijOn (fun (x : M) ↦ x + d) (Ici a) (Ici (a + d))

Tactic:
refine ⟨by simp [MapsTo], by simp, fun _ h => ?_⟩