Theorem: LO.Semantics.RealizeSet.union_iff (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
⊢ 𝓜 ⊧* T ∪ U ↔ 𝓜 ⊧* T ∧ 𝓜 ⊧* U
Tactic:
simp [realizeSet_iff]
State after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
⊢ (∀ ⦃f : F⦄, f ∈ T ∨ f ∈ U → 𝓜 ⊧ f) ↔ (∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f) ∧ ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
⊢ (∀ ⦃f : F⦄, f ∈ T ∨ f ∈ U → 𝓜 ⊧ f) ↔ (∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f) ∧ ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
Tactic:
exact
  ⟨ fun h => ⟨fun _ hf => h (Or.inl hf), fun _ hf => h (Or.inr hf)⟩,
    by rintro ⟨h₁, h₂⟩ f (h | h); exact h₁ h; exact h₂ h ⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
⊢ ((∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f) ∧ ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f) → ∀ ⦃f : F⦄, f ∈ T ∨ f ∈ U → 𝓜 ⊧ f
Tactic:
rintro ⟨h₁, h₂⟩ f (h | h)
State after:
case intro.inl
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ T
⊢ 𝓜 ⊧ f

case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f

State before:
case intro.inl
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ T
⊢ 𝓜 ⊧ f

case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f
Tactic:
exact h₁ h
State after:
case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f

State before:
case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f
Tactic:
exact h₂ h
State after:
no goals