Theorem: LO.System.strictReducible_iff (Logic/Logic/System.lean)

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ 𝓢 <ₛ 𝓣 ↔ (∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f) ∧ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f
Tactic:
simp [StrictReducible, reducible_iff]
State after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ (∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f) → ((∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f)

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
⊢ (∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f) → ((∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f)
Tactic:
intro _
State after:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
a✝ : ∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f
⊢ (∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
a✝ : ∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f
⊢ (∃ x, 𝓣 ⊢! x ∧ ¬𝓢 ⊢! x) ↔ ∃ f, 𝓢 ⊬! f ∧ 𝓣 ⊢! f
Tactic:
exact exists_congr (fun _ ↦ by simp [and_comm])
State after:
no goals

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝² : System F S
inst✝¹ : System F T
inst✝ : System F U
𝓢 : S
𝓣 : T
𝓤 : U
a✝ : ∀ {f : F}, 𝓢 ⊢! f → 𝓣 ⊢! f
x✝ : F
⊢ 𝓣 ⊢! x✝ ∧ ¬𝓢 ⊢! x✝ ↔ 𝓢 ⊬! x✝ ∧ 𝓣 ⊢! x✝
Tactic:
simp [and_comm]
State after:
no goals