Theorem: le_of_lt_imp_le (Ray/Hartogs/Subharmonic.lean)

State before:
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : ∀ c < a, c ≤ b
⊢ a ≤ b
Tactic:
contrapose h
State after:
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : ¬a ≤ b
⊢ ¬∀ c < a, c ≤ b

State before:
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : ¬a ≤ b
⊢ ¬∀ c < a, c ≤ b
Tactic:
simp only [not_forall, not_le, exists_prop] at h ⊢
State after:
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
⊢ ∃ x < a, b < x

State before:
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
⊢ ∃ x < a, b < x
Tactic:
rcases exists_between h with ⟨x, bx, xa⟩
State after:
case intro.intro
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
x : L
bx : b < x
xa : x < a
⊢ ∃ x < a, b < x

State before:
case intro.intro
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
x : L
bx : b < x
xa : x < a
⊢ ∃ x < a, b < x
Tactic:
exact ⟨x, xa, bx⟩
State after:
no goals