Theorem: Incomp_Lexcomb_iff (Algdata/Init/Order.lean)

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp (Lexcomb r s) a b
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
dsimp [Incomp] at h
State after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
⊢ Incomp r a b ∧ Incomp s a b

State before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hab := not_or.mp h.left
State after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
⊢ Incomp r a b ∧ Incomp s a b

State before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hba := not_or.mp h.right
State after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
⊢ Incomp r a b ∧ Incomp s a b

State before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have : Incomp r a b := ⟨hab.left, hba.left⟩
State after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
⊢ Incomp r a b ∧ Incomp s a b

State before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hsab : ¬ s a b :=
  λ h => absurd ⟨this, h⟩ hab.right
State after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
⊢ Incomp r a b ∧ Incomp s a b

State before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
have hsba : ¬ s b a :=
  λ h => absurd ⟨this.symm, h⟩ hba.right
State after:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
hsba : ¬s b a
⊢ Incomp r a b ∧ Incomp s a b

State before:
α : Type u
r s : α → α → Prop
a b : α
h : ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
hab : ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
hba : ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
this : Incomp r a b
hsab : ¬s a b
hsba : ¬s b a
⊢ Incomp r a b ∧ Incomp s a b
Tactic:
exact ⟨this, ⟨hsab, hsba⟩⟩
State after:
no goals

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ Incomp (Lexcomb r s) a b
Tactic:
unfold Incomp
State after:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬Lexcomb r s a b ∧ ¬Lexcomb r s b a
Tactic:
dsimp [Lexcomb]
State after:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬(r a b ∨ Incomp r a b ∧ s a b) ∧ ¬(r b a ∨ Incomp r b a ∧ s b a)

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬(r a b ∨ Incomp r a b ∧ s a b) ∧ ¬(r b a ∨ Incomp r b a ∧ s b a)
Tactic:
apply And.intro <;> apply not_or.mpr
State after:
case left
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r a b ∧ ¬(Incomp r a b ∧ s a b)

case right
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r b a ∧ ¬(Incomp r b a ∧ s b a)

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
Tactic:
case left =>
  exact ⟨h.left.left, h.right.left ∘ And.right⟩
State after:
no goals

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
Tactic:
case right =>
  exact ⟨h.left.right, h.right.right ∘ And.right⟩
State after:
no goals

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r a b ∧ ¬(Incomp r a b ∧ s a b)
Tactic:
exact ⟨h.left.left, h.right.left ∘ And.right⟩
State after:
no goals

State before:
α : Type u
r s : α → α → Prop
a b : α
h : Incomp r a b ∧ Incomp s a b
⊢ ¬r b a ∧ ¬(Incomp r b a ∧ s b a)
Tactic:
exact ⟨h.left.right, h.right.right ∘ And.right⟩
State after:
no goals