-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem hasProd_le_inj {g : κ → α} (e : ι → κ) (he : Injective e)
    (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c) (h : ∀ i, f i ≤ g (e i)) (hf : HasProd f a₁)
    (hg : HasProd g a₂) : a₁ ≤ a₂

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂

Tactic:
refine hasProd_le (fun c ↦ ?_) hf hg

Result:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
⊢ extend e f 1 c ≤ g c

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd f a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂

Tactic:
rw [← hasProd_extend_one he] at hf

Result:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
⊢ extend e f 1 c ≤ g c

Tactic:
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)

Result:
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ extend e f 1 (e i) ≤ g (e i)

case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ extend e f 1 c ≤ g c

Proof state:
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ 1 c ≤ g c

Tactic:
exact hs _ h

Result:
no goals

Proof state:
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ extend e f 1 c ≤ g c

Tactic:
rw [extend_apply' _ _ _ h]

Result:
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ 1 c ≤ g c

Proof state:
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ f i ≤ g (e i)

Tactic:
exact h _

Result:
no goals

Proof state:
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ extend e f 1 (e i) ≤ g (e i)

Tactic:
rw [he.extend_apply]

Result:
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ f i ≤ g (e i)