α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ A ⊓ K ≤ B ⊓ K ∧ ¬B ⊓ K ≤ A ⊓ K ∨ (A ⊓ K ≤ B ⊓ K ∧ B ⊓ K ≤ A ⊓ K) ∧ A ⊔ K ≤ B ⊔ K ∧ ¬B ⊔ K ≤ A ⊔ K
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ Prod.Lex (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (f₂ A, g₂ A) (f₂ B, g₂ B)
simp only [Prod.lex_def, lt_iff_le_not_le, ← gci.l_le_l_iff, ← gi.u_le_u_iff, hf, hg,
  le_antisymm_iff]
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ A ⊓ K ≤ B ⊓ K ∧ ¬B ⊓ K ≤ A ⊓ K ∨ (A ⊓ K ≤ B ⊓ K ∧ B ⊓ K ≤ A ⊓ K) ∧ A ⊔ K ≤ B ⊔ K ∧ ¬B ⊔ K ≤ A ⊔ K
simp only [gci.l_le_l_iff, gi.u_le_u_iff, ← lt_iff_le_not_le, ← le_antisymm_iff]
case inl
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
h : A ⊓ K < B ⊓ K
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K

case inr
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
h : A ⊓ K = B ⊓ K
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
cases' lt_or_eq_of_le (inf_le_inf_right K (le_of_lt hAB)) with h h
no goals
case inl
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
h : A ⊓ K < B ⊓ K
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
exact Or.inl h
no goals
case inr
α : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
x y z : α
β : Type u_1
γ : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder γ
h₁ : WellFounded fun x x_1 => x < x_1
h₂ : WellFounded fun x x_1 => x < x_1
K : α
f₁ : β → α
f₂ : α → β
g₁ : γ → α
g₂ : α → γ
gci : GaloisCoinsertion f₁ f₂
gi : GaloisInsertion g₂ g₁
hf : ∀ (a : α), f₁ (f₂ a) = a ⊓ K
hg : ∀ (a : α), g₁ (g₂ a) = a ⊔ K
A B : α
hAB : A < B
h : A ⊓ K = B ⊓ K
⊢ A ⊓ K < B ⊓ K ∨ A ⊓ K = B ⊓ K ∧ A ⊔ K < B ⊔ K
exact Or.inr ⟨h, sup_lt_sup_of_lt_of_inf_le_inf hAB (le_of_eq h.symm)⟩