Theorem: formalAppMonotoneLeft (Fine/SystemB/Theories.lean)

State before:
⊢ ∀ (Γ : Ctx), Monotone (formalApplication Γ)
Tactic:
intros Γ a b h₁ A h₂
State after:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
⊢ A ∈ formalApplication Γ b

State before:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
⊢ A ∈ formalApplication Γ b
Tactic:
have ⟨g,h₃⟩ := h₂
State after:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
g : Form
h₃ : g ∈ a ∧ g⊃A ∈ Γ
⊢ A ∈ formalApplication Γ b

State before:
Γ a b : Ctx
h₁ : a ≤ b
A : Form
h₂ : A ∈ formalApplication Γ a
g : Form
h₃ : g ∈ a ∧ g⊃A ∈ Γ
⊢ A ∈ formalApplication Γ b
Tactic:
exact ⟨g, h₁ h₃.left, h₃.right⟩
State after:
no goals