awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
h : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
inl : ∀ (hxbc : x ≤ b * c), x ∈ Icc a b * Icc c d
⊢ x ∈ Icc a b * Icc c d
have inr : ∀ (hbcx : b * c ≤ x), x ∈ Icc a b * Icc c d
Tactic: obtain hxbc | hbcx := le_total x (b * c)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
h : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hxbc : x ≤ b * c
⊢ x ∈ Icc a b * Icc c d
have inl : ∀ (y : α) (hy : 1 ≤ y),
  a * c * y ∈ Icc (a * c) (b * d) →
    ∀ (hacx : a * c ≤ a * c * y) (hxbd : a * c * y ≤ b * d) (hxbc : a * c * y ≤ b * c), a * c * y ∈ Icc a b * Icc c d
Tactic: obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hacx
Cleared hypotheses: x, h, hacx, hxbd, hxbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * c * y ∈ Icc a b * Icc c d
have inl : a * y ≤ b
Tactic: refine ⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
⊢ a * y ≤ b
have inl : ∀ (hxbc : a * y * c ≤ b * c), a * y ≤ b
Tactic: rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc
Cleared hypotheses: hxbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : a * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ a * c * y
hxbd : a * c * y ≤ b * d
hxbc : a * c * y ≤ b * c
inl : ∀ (hxbc : a * y * c ≤ b * c), a * y ≤ b
⊢ a * y ≤ b
have inl₁ : ∀ (hxbc : a * y ≤ b), a * y ≤ b
Tactic: rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc
Cleared hypotheses: hxbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
x : α
h : x ∈ Icc (a * c) (b * d)
hacx : a * c ≤ x
hxbd : x ≤ b * d
hbcx : b * c ≤ x
⊢ x ∈ Icc a b * Icc c d
have inr : ∀ (y : α) (hy : 1 ≤ y),
  b * c * y ∈ Icc (a * c) (b * d) →
    ∀ (hacx : a * c ≤ b * c * y) (hxbd : b * c * y ≤ b * d) (hbcx : b * c ≤ b * c * y), b * c * y ∈ Icc a b * Icc c d
Tactic: obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hbcx
Cleared hypotheses: x, h, hacx, hxbd, hbcx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ b * c * y ∈ Icc a b * Icc c d
have inr : c * y ≤ d
Tactic: refine ⟨b, right_mem_Icc.2 hab, c * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
⊢ c * y ≤ d
have inr : ∀ (hxbd : b * (c * y) ≤ b * d) (hbcx : b * c ≤ b * c * y), c * y ≤ d
Tactic: rwa [mul_assoc, mul_le_mul_iff_left] at hxbd
Cleared hypotheses: hxbd, hbcx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : MulLeftReflectLE α
inst_4 : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
y : α
hy : 1 ≤ y
h : b * c * y ∈ Icc (a * c) (b * d)
hacx : a * c ≤ b * c * y
hxbd : b * c * y ≤ b * d
hbcx : b * c ≤ b * c * y
inr : ∀ (hxbd : b * (c * y) ≤ b * d) (hbcx : b * c ≤ b * c * y), c * y ≤ d
⊢ c * y ≤ d
have inr₁ : ∀ (hxbd : c * y ≤ d) (hbcx : b * c ≤ b * c * y), c * y ≤ d
Tactic: rwa [mul_assoc, mul_le_mul_iff_left] at hxbd
Cleared hypotheses: hxbd, hbcx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) '' Ici b = Iic (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) '' Iic b = Ici (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) '' Ioi b = Iio (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ (fun (x : α) ↦ a / x) '' Iio b = Ioi (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a / x) '' Icc b c = Icc (a / c) (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a / x) '' Ico b c = Ioc (a / c) (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a / x) '' Ioc b c = Ico (a / c) (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ (fun (x : α) ↦ a / x) '' Ioo b c = Ioo (a / c) (a / b)
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a * x) ∘ fun (x : α) ↦ x⁻¹) '' a_1)
    ((fun (x : α) ↦ a * x) '' (fun (x : α) ↦ x⁻¹) '' a_1)
Tactic: have := image_comp (fun x => a * x) fun x => x⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]
have simp_rw : Icc (a - max b c) (a - min b c) = Icc (min (a - b) (a - c)) (max (a - b) (a - c))
Tactic: simp_rw [← Icc_min_max, preimage_const_sub_Icc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ (fun (x : α) ↦ a - x) '' [[b, c]] = [[a - b, a - c]]
have this : ∀ (a_1 : Set α),
  Eq (α := Set α) (((fun (x : α) ↦ a + x) ∘ fun (x : α) ↦ -x) '' a_1)
    ((fun (x : α) ↦ a + x) '' (fun (x : α) ↦ -x) '' a_1)
Tactic: have := image_comp (fun x => a + x) fun x => -x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ |d - c| ≤ |b - a|
have rw : max c d - min c d ≤ max a b - min a b
Tactic: rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ max c d - min c d ≤ max a b - min a b
have h₁ : min a b ≤ min c d ∧ max c d ≤ max a b
Tactic: rw [uIcc_subset_uIcc_iff_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
have inl : 0 = c → (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
Tactic: cases eq_or_lt_of_le hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
inl : 0 = c → (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
⊢ (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
have inr : 0 < c → (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
Tactic: cases eq_or_lt_of_le hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
h : 0 = c
⊢ (fun (x : G₀) ↦ x * c) '' Icc a b = Icc (a * c) (b * c)
have inl : ∀ (hc : LE.le.{u_2} (α := G₀) 0 0), (fun (x : G₀) ↦ x * 0) '' Icc a b = Icc (a * 0) (b * 0)
Tactic: subst c
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hbc : b ≤ c
⊢ (fun (x : G₀) ↦ a * x) '' Icc b c = Icc (a * b) (a * c)
have inl : ∀ (ha : LE.le.{u_2} (α := G₀) 0 0), (fun (x : G₀) ↦ 0 * x) '' Icc b c = Icc (0 * b) (0 * c)
Tactic: rcases ha.eq_or_lt with rfl | ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hbc : b ≤ c
inl : ∀ (ha : LE.le.{u_2} (α := G₀) 0 0), (fun (x : G₀) ↦ 0 * x) '' Icc b c = Icc (0 * b) (0 * c)
⊢ (fun (x : G₀) ↦ a * x) '' Icc b c = Icc (a * b) (a * c)
have inr : ∀ (ha : 0 < a), (fun (x : G₀) ↦ a * x) '' Icc b c = Icc (a * b) (a * c)
Tactic: rcases ha.eq_or_lt with rfl | ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ Eq.{u_2 + 1} (α := Set G₀) ((fun (x : G₀) ↦ a * x) '' Ioi 0) (Ioi 0)
have rw : Ioi (a * 0) = Ioi 0
Tactic: rw [image_mul_left_Ioi ha, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
a : G₀
ha : 0 < a
rw : Ioi (a * 0) = Ioi 0
⊢ Eq.{u_2 + 1} (α := Set G₀) ((fun (x : G₀) ↦ a * x) '' Ioi 0) (Ioi 0)
have rw₁ : Eq.{u_2 + 1} (α := Set G₀) (Ioi 0) (Ioi 0)
Tactic: rw [image_mul_left_Ioi ha, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹
have h : ∀ (x : G₀), x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
⊢ (Ioi a)⁻¹ = Ioo 0 a⁻¹
have rw : Ioi a = (Ioo 0 a⁻¹)⁻¹
Tactic: rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
rw : Ioi a = (Ioo 0 a⁻¹)⁻¹
⊢ (Ioi a)⁻¹ = Ioo 0 a⁻¹
have rw₁ : Ioi a = Ioi a⁻¹⁻¹
Tactic: rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : PartialOrder G₀
inst_2 : PosMulReflectLT G₀
inst_3 : MulPosReflectLT G₀
a : G₀
ha : 0 < a
rw : Ioi a = (Ioo 0 a⁻¹)⁻¹
rw₁ : Ioi a = Ioi a⁻¹⁻¹
⊢ (Ioi a)⁻¹ = Ioo 0 a⁻¹
have rw₂ : Ioi a = Ioi a
Tactic: rw [inv_eq_iff_eq_inv, inv_Ioo_0_left (inv_pos.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
have rwa : ∀ (this : (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)),
  (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
Tactic: rwa [Set.image_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ a * x + b) '' Icc c d = Icc (a * c + b) (a * d + b)
have suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
Tactic: suffices (· + b) '' (a * ·) '' Icc c d = Icc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
have rw : (fun (x : K) ↦ x + b) '' Icc (a * c) (a * d) = Icc (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Icc' h, image_add_const_Icc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Icc (a * c) (a * d) = Icc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Icc c d = Icc (a * c + b) (a * d + b)
have rw₁ : Icc (a * c + b) (a * d + b) = Icc (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Icc' h, image_add_const_Icc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
have rwa : ∀ (this : (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)),
  (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
Tactic: rwa [Set.image_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)
have suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)
Tactic: suffices (· + b) '' (a * ·) '' Ico c d = Ico (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)
have rw : (fun (x : K) ↦ x + b) '' Ico (a * c) (a * d) = Ico (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Ico h, image_add_const_Ico]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Ico (a * c) (a * d) = Ico (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ico c d = Ico (a * c + b) (a * d + b)
have rw₁ : Ico (a * c + b) (a * d + b) = Ico (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Ico h, image_add_const_Ico]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
have rwa : ∀ (this : (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)),
  (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
Tactic: rwa [Set.image_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ a * x + b) '' Ioc c d = Ioc (a * c + b) (a * d + b)
have suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)
Tactic: suffices (· + b) '' (a * ·) '' Ioc c d = Ioc (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)
have rw : (fun (x : K) ↦ x + b) '' Ioc (a * c) (a * d) = Ioc (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Ioc h, image_add_const_Ioc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Ioc (a * c) (a * d) = Ioc (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)
have rw₁ : Ioc (a * c + b) (a * d + b) = Ioc (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Ioc h, image_add_const_Ioc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
this : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
have rwa : ∀ (this : (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)),
  (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
Tactic: rwa [Set.image_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)
have suffices : (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)
Tactic: suffices (· + b) '' (a * ·) '' Ioo c d = Ioo (a * c + b) (a * d + b) by
    rwa [Set.image_image] at this
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)
have rw : (fun (x : K) ↦ x + b) '' Ioo (a * c) (a * d) = Ioo (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Ioo h, image_add_const_Ioo]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : PartialOrder K
inst_2 : PosMulReflectLT K
inst_3 : IsOrderedCancelAddMonoid K
inst_4 : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
rw : (fun (x : K) ↦ x + b) '' Ioo (a * c) (a * d) = Ioo (a * c + b) (a * d + b)
⊢ (fun (x : K) ↦ x + b) '' (fun (x : K) ↦ a * x) '' Ioo c d = Ioo (a * c + b) (a * d + b)
have rw₁ : Ioo (a * c + b) (a * d + b) = Ioo (a * c + b) (a * d + b)
Tactic: rw [image_mul_left_Ioo h, image_add_const_Ioo]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} U
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
have inl : ∀ (aU : α) (haU : U = Ioi aU), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
Tactic: obtain ⟨aU, (haU | haU)⟩ := hU
Cleared hypotheses: hU