[GOAL]
α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ : p x
y : α
property✝ : p y
⊢ { val := x, property := property✝¹ } = { val := y, property := property✝ }
[PROOFSTEP]
cases Subsingleton.elim x y
[GOAL]
case refl
α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ property✝ : p x
⊢ { val := x, property := property✝¹ } = { val := x, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α β : Sort u_1
γ : Sort u_2
f : α → γ
g : β → γ
x : α
y : β
h₁ : HEq f g
h₂ : HEq x y
⊢ f x = g y
[PROOFSTEP]
cases h₂
[GOAL]
case refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
g : α → γ
h₁ : HEq f g
⊢ f x = g x
[PROOFSTEP]
cases h₁
[GOAL]
case refl.refl
α : Sort u_1
γ : Sort u_2
f : α → γ
x : α
⊢ f x = f x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
a b : ULift α
h : a = b
⊢ a.down = b.down
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }
[PROOFSTEP]
congr
[GOAL]
α : Sort u_1
a b : PLift α
h : a = b
⊢ a.down = b.down
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = c
[PROOFSTEP]
rw [← h]
[GOAL]
α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = b ↔ a = c
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ a = b
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ a✝ = a ↔ b = a
[PROOFSTEP]
rw [h]
[GOAL]
⊢ Eq True = id
[PROOFSTEP]
funext _
[GOAL]
case h
x✝ : Prop
⊢ (True = x✝) = id x✝
[PROOFSTEP]
simp only [true_iff, id.def, eq_iff_iff]
[GOAL]
⊢ Xor' True = Not
[PROOFSTEP]
simp [Xor']
[GOAL]
⊢ Xor' False = id
[PROOFSTEP]
ext
[GOAL]
case h.a
x✝ : Prop
⊢ Xor' False x✝ ↔ id x✝
[PROOFSTEP]
simp [Xor']
[GOAL]
a b : Prop
⊢ Xor' a b = Xor' b a
[PROOFSTEP]
simp [Xor', and_comm, or_comm]
[GOAL]
a : Prop
⊢ Xor' a a = False
[PROOFSTEP]
simp [Xor']
[GOAL]
a b : Prop
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
a b : Prop
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
case pos
a b : Prop
h : a
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
a b : Prop
h : ¬a
⊢ Xor' (¬a) b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
a b : Prop
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
a b : Prop
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
by_cases a
[GOAL]
case pos
a b : Prop
h : a
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
a b : Prop
h : ¬a
⊢ Xor' a ¬b ↔ (a ↔ b)
[PROOFSTEP]
simp [*]
[GOAL]
a b : Prop
⊢ Xor' (¬a) ¬b ↔ Xor' a b
[PROOFSTEP]
simp [Xor', or_comm, and_comm]
[GOAL]
α : Sort u_1
a b : α
p : Prop
⊢ p ∧ a = b ↔ p ∧ b = a
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Sort u_1
a b : α
p : Prop
⊢ a = b ∧ p ↔ b = a ∧ p
[PROOFSTEP]
simp [eq_comm]
[GOAL]
P Q : Prop
⊢ ¬Xor' P Q ↔ (P ↔ Q)
[PROOFSTEP]
simp only [not_and, Xor', not_or, not_not, ← iff_iff_implies_and_implies]
[GOAL]
a b : Prop
⊢ Xor' a b ↔ (a ↔ ¬b)
[PROOFSTEP]
simp only [← @xor_not_right a, not_not]
[GOAL]
a b : Prop
⊢ Xor' a b ↔ (¬a ↔ b)
[PROOFSTEP]
simp only [← @xor_not_left _ b, not_not]
[GOAL]
a✝¹ a✝ : Sort u_1
e : a✝¹ = a✝
a : a✝¹
a' : a✝
h : HEq a a'
⊢ cast e a = a'
[PROOFSTEP]
cases h
[GOAL]
case refl
a✝ : Sort u_1
a : a✝
e : a✝ = a✝
⊢ cast e a = a
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u
p : motive a' (_ : a' = a')
a : α
t : a' = a
⊢ HEq (t ▸ p) p
[PROOFSTEP]
subst t
[GOAL]
α : Sort u_1
a' : α
motive : (a : α) → a' = a → Sort u
p : motive a' (_ : a' = a')
⊢ HEq ((_ : a' = a') ▸ p) p
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
b : α
C : α → Sort u_1
x : C a
y : β
e : a = b
h : HEq x y
⊢ HEq (e ▸ x) y
[PROOFSTEP]
subst e
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
C : α → Sort u_1
x : C a
y : β
h : HEq x y
⊢ HEq ((_ : a = a) ▸ x) y
[PROOFSTEP]
exact h
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
b : α
C : α → Sort u_1
x : C a
y : β
e : a = b
⊢ HEq (e ▸ x) y ↔ HEq x y
[PROOFSTEP]
subst e
[GOAL]
α : Sort u_2
a : α
β : Sort u_1
C : α → Sort u_1
x : C a
y : β
⊢ HEq ((_ : a = a) ▸ x) y ↔ HEq x y
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_2
β : Sort u_1
a b : α
C : α → Sort u_1
x : β
y : C a
e : a = b
⊢ HEq x (e ▸ y) ↔ HEq x y
[PROOFSTEP]
subst e
[GOAL]
α : Sort u_2
β : Sort u_1
a : α
C : α → Sort u_1
x : β
y : C a
⊢ HEq x ((_ : a = a) ▸ y) ↔ HEq x y
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u_1
x₁ y₁ x₂ y₂ : α✝
h₁ : x₁ = y₁
h₂ : x₂ = y₂
⊢ x₁ = x₂ ↔ y₁ = y₂
[PROOFSTEP]
subst h₁
[GOAL]
α✝ : Sort u_1
x₁ x₂ y₂ : α✝
h₂ : x₂ = y₂
⊢ x₁ = x₂ ↔ x₁ = y₂
[PROOFSTEP]
subst h₂
[GOAL]
α✝ : Sort u_1
x₁ x₂ : α✝
⊢ x₁ = x₂ ↔ x₁ = x₂
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
x y z : α
h : x = y
⊢ x = z ↔ y = z
[PROOFSTEP]
rw [h]
[GOAL]
α : Sort u_1
x y z : α
h : x = y
⊢ z = x ↔ z = y
[PROOFSTEP]
rw [h]
[GOAL]
ι : Sort ?u.13179
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
inst✝ : (x : α) → Decidable (p x)
⊢ (¬∃ x, ¬p x) ↔ ∀ (x : α), p x
[PROOFSTEP]
simp only [not_exists, Decidable.not_not]
[GOAL]
ι : Sort ?u.13446
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
[PROOFSTEP]
let ⟨a⟩ := ha
[GOAL]
ι : Sort ?u.13446
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
[PROOFSTEP]
refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
[GOAL]
ι : Sort ?u.13446
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False
[PROOFSTEP]
exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (not_imp.1 (h' x)).1
[GOAL]
ι : Sort ?u.13873
α : Sort ?u.13878
κ : ι → Sort u_1
p q : α → Prop
β : α → Sort u_2
⊢ (∀ (a : α), β a → True) ↔ True
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.14073
α : Sort ?u.14078
κ : ι → Sort u_1
p q : α → Prop
β : α → Sort u_2
γ : (a : α) → β a → Sort u_3
⊢ (∀ (a : α) (b : β a), γ a b → True) ↔ True
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.14717
α✝ : Sort ?u.14722
κ : ι → Sort u_1
p q : α✝ → Prop
b : Prop
α : Sort u_2
i : Nonempty α
inst✝ : Subsingleton α
⊢ (∃! x, b) ↔ b
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.14980
α : Sort u_2
κ : ι → Sort u_1
p✝ q : α → Prop
inst✝ : DecidableEq α
a : α
p : α → Prop
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
[PROOFSTEP]
simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]
[GOAL]
ι : Sort ?u.15561
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
a' : α
⊢ ∃! a, a = a'
[PROOFSTEP]
simp only [eq_comm, ExistsUnique, and_self, forall_eq', exists_eq']
[GOAL]
ι : Sort ?u.15937
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
a' : α
⊢ ∃! a, a' = a
[PROOFSTEP]
simp only [ExistsUnique, and_self, forall_eq', exists_eq']
[GOAL]
ι : Sort ?u.17741
α : Sort ?u.17746
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.18041
α : Sort ?u.18046
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp [forall_swap]
[GOAL]
ι : Sort ?u.18571
α : Sort ?u.18576
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.18901
α : Sort ?u.18906
κ : ι → Sort u_1
p✝ q : α → Prop
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)
[PROOFSTEP]
simp [forall_swap]
[GOAL]
ι : Sort ?u.19647
α : Sort u_2
κ : ι → Sort u_1
p q : α → Prop
a' : α
⊢ (∃ a, p a ∧ a' = a) ↔ p a'
[PROOFSTEP]
simp [@eq_comm _ a']
[GOAL]
ι : Sort ?u.19995
α : Sort ?u.20000
κ : ι → Sort u_1
p✝ q : α → Prop
ι₁ : Sort u_4
ι₂ : Sort u_5
κ₁ : ι₁ → Sort u_2
κ₂ : ι₂ → Sort u_3
p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop
⊢ (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂
[PROOFSTEP]
simp only [@exists_comm (κ₁ _), @exists_comm ι₁]
[GOAL]
ι : Sort ?u.21140
α : Sort ?u.21145
κ : ι → Sort u_1
p✝ q✝ : α → Prop
q : Prop
p : α → Prop
inst✝ : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
[PROOFSTEP]
simp [or_comm, Decidable.forall_or_left]
[GOAL]
ι : Sort ?u.21525
α : Sort ?u.21530
κ : ι → Sort u_1
p✝ q✝ : α → Prop
p q : Prop
⊢ (∃! x, q) ↔ p ∧ q
[PROOFSTEP]
simp
[GOAL]
ι : Sort ?u.22333
α : Sort ?u.22338
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True
[PROOFSTEP]
simpa only [H] using h₂
[GOAL]
ι : Sort ?u.22333
α : Sort ?u.22338
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False
[PROOFSTEP]
simpa only [H] using h₂
[GOAL]
ι : Sort ?u.22592
α : Sort ?u.22597
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
⊢ p h
[PROOFSTEP]
by_cases H : h
[GOAL]
case pos
ι : Sort ?u.22592
α : Sort ?u.22597
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : h
⊢ p h
[PROOFSTEP]
simpa only [H]
[GOAL]
case neg
ι : Sort ?u.22592
α : Sort ?u.22597
κ : ι → Sort u_1
p✝ q : α → Prop
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : ¬h
⊢ p h
[PROOFSTEP]
simpa only [H]
[GOAL]
ι : Sort ?u.23891
α✝ : Sort ?u.23896
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x h, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ b
[PROOFSTEP]
simp only [exists_unique_iff_exists] at h₂ 
[GOAL]
ι : Sort ?u.23891
α✝ : Sort ?u.23896
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ b
[PROOFSTEP]
apply h₂.elim
[GOAL]
ι : Sort ?u.23891
α✝ : Sort ?u.23896
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ ∀ (x : α), (∃ h, q x h) → (∀ (y : α), (∃ h, q y h) → y = x) → b
[PROOFSTEP]
exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩
[GOAL]
ι : Sort ?u.24313
α✝ : Sort ?u.24318
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x hx, q x hx
[PROOFSTEP]
simp only [exists_unique_iff_exists]
[GOAL]
ι : Sort ?u.24313
α✝ : Sort ?u.24318
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
w : α
hp : p w
hq : q w hp
H : ∀ (y : α) (hy : p y), q y hy → y = w
⊢ ∃! x, ∃ hx, q x hx
[PROOFSTEP]
exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq
[GOAL]
ι : Sort ?u.24821
α✝ : Sort ?u.24826
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
h : ∃! x hx, q x hx
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
⊢ y₁ = y₂
[PROOFSTEP]
simp only [exists_unique_iff_exists] at h 
[GOAL]
ι : Sort ?u.24821
α✝ : Sort ?u.24826
κ : ι → Sort u_1
p✝ q✝ : α✝ → Prop
α : Sort u_2
p : α → Sort u_3
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
y₁ y₂ : α
hpy₁ : p y₁
hqy₁ : q y₁ hpy₁
hpy₂ : p y₂
hqy₂ : q y₂ hpy₂
h : ∃! x, ∃ hx, q x hx
⊢ y₁ = y₂
[PROOFSTEP]
exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩
[GOAL]
α : Sort ?u.25125
p✝ : α → Prop
p : Prop
⊢ Decidable p
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort ?u.25149
p✝ p : α → Prop
⊢ DecidablePred p
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort ?u.25193
p✝ : α → Prop
p : α → α → Prop
⊢ DecidableRel p
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Sort ?u.25252
p : α✝ → Prop
α : Sort u
⊢ DecidableEq α
[PROOFSTEP]
infer_instance
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
a : α
⊢ (∃ x x_1, p x) ↔ p a
[PROOFSTEP]
simp only [exists_prop, exists_eq_left]
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x h, P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b
[PROOFSTEP]
simp
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x
[PROOFSTEP]
simp only [exists_prop]
[GOAL]
α : Sort u_1
r p q : α → Prop
P Q : (x : α) → p x → Prop
b : Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x
[PROOFSTEP]
exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or
[GOAL]
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
by_cases P
[GOAL]
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
by_cases P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
simp [*, exists_prop_of_true, exists_prop_of_false]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.31192
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
[PROOFSTEP]
simp [*, exists_prop_of_true, exists_prop_of_false]
[GOAL]
α : Sort u_2
β : Sort ?u.31675
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ ((∃ h, (fun x => a) h = c) ∨ ∃ h, (fun x => b) h = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
[PROOFSTEP]
simp only
[GOAL]
α : Sort u_2
β : Sort ?u.31675
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ ((∃ h, a = c) ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
[PROOFSTEP]
rw [exists_prop, exists_prop]
[GOAL]
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
by_cases P
[GOAL]
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
by_cases P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : P
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.32661
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
by_cases P
[GOAL]
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
by_cases P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : P
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.33174
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ (dite P A fun x => b) = b ↔ ∀ (h : P), A h = b
[PROOFSTEP]
simp [*, forall_prop_of_true, forall_prop_of_false]
[GOAL]
α : Sort u_2
β : Sort ?u.33996
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ dite P (fun x => a) B ≠ a ↔ ∃ h, a ≠ B h
[PROOFSTEP]
rw [Ne.def, dite_eq_left_iff, not_forall]
[GOAL]
α : Sort u_2
β : Sort ?u.33996
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ x, ¬B x = a) ↔ ∃ h, a ≠ B h
[PROOFSTEP]
exact exists_congr fun h ↦ by rw [ne_comm]
[GOAL]
α : Sort u_2
β : Sort ?u.33996
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ ¬B h = a ↔ a ≠ B h
[PROOFSTEP]
rw [ne_comm]
[GOAL]
α : Sort u_2
β : Sort ?u.34290
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (dite P A fun x => b) ≠ b ↔ ∃ h, A h ≠ b
[PROOFSTEP]
simp only [Ne.def, dite_eq_right_iff, not_forall]
[GOAL]
α : Sort u_2
β : Sort ?u.34782
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ (fun x => b) h) ↔ ¬P ∧ a ≠ b
[PROOFSTEP]
simp only
[GOAL]
α : Sort u_2
β : Sort ?u.34782
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b
[PROOFSTEP]
rw [exists_prop]
[GOAL]
α : Sort u_2
β : Sort ?u.35052
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, (fun x => a) h ≠ b) ↔ P ∧ a ≠ b
[PROOFSTEP]
simp only
[GOAL]
α : Sort u_2
β : Sort ?u.35052
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ b) ↔ P ∧ a ≠ b
[PROOFSTEP]
rw [exists_prop]
[GOAL]
α : Sort u_3
β : Sort u_4
σ : α → Sort u_1
f✝ : α → β
P✝ Q : Prop
inst✝² : Decidable P✝
inst✝¹ : Decidable Q
a✝ b✝ c✝ : α
A : P✝ → α
B : ¬P✝ → α
γ : Sort u_2
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Sort u_3
β : Sort u_4
σ : α → Sort u_1
f✝ : α → β
P✝ Q : Prop
inst✝² : Decidable P✝
inst✝¹ : Decidable Q
a✝ b✝ c✝ : α
A : P✝ → α
B : ¬P✝ → α
γ : Sort u_2
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Sort u_3
β : Sort u_4
σ : α → Sort u_1
f✝ : α → β
P✝ Q : Prop
inst✝² : Decidable P✝
inst✝¹ : Decidable Q
a✝ b✝ c✝ : α
A : P✝ → α
B : ¬P✝ → α
γ : Sort u_2
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : ¬P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
[PROOFSTEP]
simp [h]
[GOAL]
α : Sort u_2
β : Sort ?u.37772
σ : α → Sort u_1
f✝ : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a✝ b c : α
A : P → α
B : ¬P → α
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
⊢ dite P f g a = if h : P then f h a else g h a
[PROOFSTEP]
by_cases h : P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.37772
σ : α → Sort u_1
f✝ : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a✝ b c : α
A : P → α
B : ¬P → α
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : P
⊢ dite P f g a = if h : P then f h a else g h a
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.37772
σ : α → Sort u_1
f✝ : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a✝ b c : α
A : P → α
B : ¬P → α
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : ¬P
⊢ dite P f g a = if h : P then f h a else g h a
[PROOFSTEP]
simp [h]
[GOAL]
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
by_cases hp : P
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
by_cases hq : Q
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : ¬P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
by_cases hq : Q
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case pos
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case neg
α : Sort u_2
β : Sort ?u.38314
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
[PROOFSTEP]
simp [hp, hq]
[GOAL]
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
p : P
⊢ A p = if q : Q then B q else if p : P then A p else C p q
[PROOFSTEP]
rw [dif_neg (h p), dif_pos p]
[GOAL]
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (if q : Q then B q else C np q) = if q : Q then B q else if p : P then A p else C p q
[PROOFSTEP]
congr
[GOAL]
case e_e
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (fun q => C np q) = fun q => if p : P then A p else C p q
[PROOFSTEP]
funext _
[GOAL]
case e_e.h
α : Sort u_2
β : Sort ?u.39011
σ : α → Sort u_1
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B✝ : ¬P → α
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
x✝ : ¬Q
⊢ C np x✝ = if p : P then A p else C p x✝
[PROOFSTEP]
rw [dif_neg np]
