Theorem: LO.System.iff_provable_list_conj (Logic/Logic/HilbertStyle/Supplemental.lean)

State before:
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
Γ : List F
⊢ 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simp;
| hsingle => simp;
| hcons p Γ hΓ ih =>
  simp_all;
  constructor;
  . intro h;
    constructor;
    . exact conj₁'! h;
    . exact ih.mp (conj₂'! h);
  . rintro ⟨h₁, h₂⟩;
    exact conj₃'! h₁ (ih.mpr h₂);
State after:
no goals

State before:
case hnil
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
⊢ 𝓢 ⊢! [].conj' ↔ ∀ p ∈ [], 𝓢 ⊢! p
Tactic:
simp
State after:
no goals

State before:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
⊢ 𝓢 ⊢! [a✝].conj' ↔ ∀ p ∈ [a✝], 𝓢 ⊢! p
Tactic:
simp
State after:
no goals

State before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : Γ ≠ []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! (p :: Γ).conj' ↔ ∀ p_1 ∈ p :: Γ, 𝓢 ⊢! p_1
Tactic:
simp_all
State after:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' ↔ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a

State before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' ↔ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
constructor
State after:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' → 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a

case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'

State before:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' → 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a

case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
. intro h;
  constructor;
  . exact conj₁'! h;
  . exact ih.mp (conj₂'! h);
State after:
case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'

State before:
case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
. rintro ⟨h₁, h₂⟩;
  exact conj₃'! h₁ (ih.mpr h₂);
State after:
no goals

State before:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ 𝓢 ⊢! p ⋏ Γ.conj' → 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
intro h
State after:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a

State before:
case hcons.mp
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
constructor
State after:
case hcons.mp.left
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p

case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a

State before:
case hcons.mp.left
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p

case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
. exact conj₁'! h;
State after:
case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a

State before:
case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
. exact ih.mp (conj₂'! h);
State after:
no goals

State before:
case hcons.mp.left
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ 𝓢 ⊢! p
Tactic:
exact conj₁'! h
State after:
no goals

State before:
case hcons.mp.right
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h : 𝓢 ⊢! p ⋏ Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! a
Tactic:
exact ih.mp (conj₂'! h)
State after:
no goals

State before:
case hcons.mpr
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
⊢ (𝓢 ⊢! p ∧ ∀ a ∈ Γ, 𝓢 ⊢! a) → 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
rintro ⟨h₁, h₂⟩
State after:
case hcons.mpr.intro
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h₁ : 𝓢 ⊢! p
h₂ : ∀ a ∈ Γ, 𝓢 ⊢! a
⊢ 𝓢 ⊢! p ⋏ Γ.conj'

State before:
case hcons.mpr.intro
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hΓ : ¬Γ = []
ih : 𝓢 ⊢! Γ.conj' ↔ ∀ p ∈ Γ, 𝓢 ⊢! p
h₁ : 𝓢 ⊢! p
h₂ : ∀ a ∈ Γ, 𝓢 ⊢! a
⊢ 𝓢 ⊢! p ⋏ Γ.conj'
Tactic:
exact conj₃'! h₁ (ih.mpr h₂)
State after:
no goals