-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem inf_eq_right {a b : CauSeq α abs} (h : b ≤ a) : a ⊓ b ≈ b

Proof state:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
⊢ a ⊓ b ≈ b

Tactic:
intro _ _

Result:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a ⊓ b - b) j| < ε✝

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b

Tactic:
refine Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) ?_

Result:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ b ⊓ b ≈ b

Proof state:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑(a ⊓ b - b) j| < ε✝

Tactic:
dsimp

Result:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑a j ⊓ ↑b j - ↑b j| < ε✝

Proof state:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |(↑a j - ↑b j) ⊓ (↑b j - ↑b j)| < ε✝

Tactic:
rwa [sub_self, min_eq_right, abs_zero]

Result:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑a j - ↑b j

Proof state:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑a j ⊓ ↑b j - ↑b j| < ε✝

Tactic:
rw [← min_sub_sub_right]

Result:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |(↑a j - ↑b j) ⊓ (↑b j - ↑b j)| < ε✝

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ b ⊓ b ≈ b

Tactic:
rw [CauSeq.inf_idem]

Result:
no goals

Proof state:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a ⊓ b - b) j| < ε✝

Tactic:
refine ⟨i, fun j hj => ?_⟩

Result:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ |↑(a ⊓ b - b) j| < ε✝

Proof state:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
ε✝ : α
a✝ : ε✝ > 0
j : ℕ
hj : j ≥ i
⊢ 0 ≤ ↑a j - ↑b j

Tactic:
exact ε0.le.trans (h _ hj)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≤ a
⊢ a ⊓ b ≈ b

Tactic:
obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h

Result:
case inl.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
ε : α
ε0 : 0 < ε
i : ℕ
h : ∀ j ≥ i, ε ≤ ↑(a - b) j
⊢ a ⊓ b ≈ b

case inr
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : b ≈ a
⊢ a ⊓ b ≈ b