awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
let let₁ let₂ : ∀ (a : α), (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
let₃ : ∀ (a : α) (h : (∀ (x : α), p x) → b) (h' : ∀ (x : α), ¬(p x → b)), False
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b

Tactic:
classical
  let ⟨a⟩ := ha
  refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
  exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (Classical.not_imp.1 (h' x)).1
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
⊢ (∀ (a : α), True) ↔ True

Tactic:
imp_true_iff _

Premises used: imp_true_iff
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
h : ∀ (a : α), p a ↔ True
⊢ (∀ (a : α), p a) ↔ True

Tactic:
iff_true_intro fun _ ↦ of_iff_true (h _)

Premises used: of_iff_true, iff_true_intro
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : α → Sort u_3
⊢ (∀ (a : α) (a : β a), True) ↔ True

Tactic:
simp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : α → Sort u_3
γ : (a : α) → β a → Sort u_4
⊢ (∀ (a : α) (b : β a) (a : γ a b), True) ↔ True

Tactic:
simp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
inst : DecidableEq α
a : α
p : α → Prop
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b

Tactic:
simp only [← @forall_eq _ p a, ← forall_and, ← or_imp, Decidable.em, forall_const]

Premises used: forall_eq, or_imp, Decidable.em, forall_const, forall_and
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
a : α
⊢ (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b

Tactic:
open scoped Classical in Decidable.and_forall_ne a

Premises used: Decidable.and_forall_ne
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
x y z : α
h : x ≠ y
⊢ x ≠ z ∨ y ≠ z

Tactic:
not_and_or.1 <| mt (and_imp.2 (· ▸ ·)) h.symm

Premises used: Iff.mpr, and_imp, mt, Ne.symm, not_and_or, Iff.mp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
a' : α
⊢ ∃ (a : α), f a' = f a

Tactic:
⟨a', rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
a : α
b : β
⊢ ∃ (x : α), ∃ (y : β), f x y = f a b

Tactic:
⟨a, b, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
a : α
b : β
⊢ ∃ (x : α), ∃ (y : β), f a b = f x y

Tactic:
⟨a, b, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
δ : Sort u_6
f : α → β → γ → δ
a : α
b : β
c : γ
⊢ ∃ (x : α), ∃ (y : β), ∃ (z : γ), f x y z = f a b c

Tactic:
⟨a, b, c, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
δ : Sort u_6
f : α → β → γ → δ
a : α
b : β
c : γ
⊢ ∃ (x : α), ∃ (y : β), ∃ (z : γ), f a b c = f x y z

Tactic:
⟨a, b, c, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
a : α
b : β
⊢ ∃ (f : α → β), f a = b

Tactic:
⟨fun _ ↦ b, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
p : α → Prop
q : β → Prop
⊢ (∃ (b : β), (∃ (a : α), p a ∧ f a = b) ∧ q b) ↔ ∃ (a : α), p a ∧ q (f a)

Tactic:
⟨fun ⟨_, ⟨a, ha, hab⟩, hb⟩ ↦ ⟨a, ha, hab.symm ▸ hb⟩, fun ⟨a, hp, hq⟩ ↦ ⟨f a, ⟨a, hp, rfl⟩, hq⟩⟩

Premises used: Exists, Eq.rec, And, And.intro, Iff.intro, Exists.intro, Eq.symm, Eq, _private.0.exists_exists_and_eq_and.match_1, rfl, _private.0.exists_exists_and_eq_and.match_2
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∃ (b : β), (∃ (a : α), f a = b) ∧ p b) ↔ ∃ (a : α), p (f a)

Tactic:
⟨fun ⟨_, ⟨a, ha⟩, hb⟩ ↦ ⟨a, ha.symm ▸ hb⟩, fun ⟨a, ha⟩ ↦ ⟨f a, ⟨a, rfl⟩, ha⟩⟩

Premises used: _private.0.exists_exists_eq_and.match_2, Exists, Eq.rec, _private.0.exists_exists_eq_and.match_1, And, And.intro, Iff.intro, Exists.intro, Eq.symm, Eq, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → γ
p : α → Prop
q : β → Prop
r : γ → Prop
⊢ (∃ (c : γ), (∃ (a : α), p a ∧ ∃ (b : β), q b ∧ f a b = c) ∧ r c) ↔ ∃ (a : α), p a ∧ ∃ (b : β), q b ∧ r (f a b)

Tactic:
⟨fun ⟨_, ⟨a, ha, b, hb, hab⟩, hc⟩ ↦ ⟨a, ha, b, hb, hab.symm ▸ hc⟩,
    fun ⟨a, ha, b, hb, hab⟩ ↦ ⟨f a b, ⟨a, ha, b, hb, rfl⟩, hab⟩⟩

Premises used: Exists, Eq.rec, _private.0.exists_exists_and_exists_and_eq_and.match_2, And, _private.0.exists_exists_and_exists_and_eq_and.match_1, And.intro, Iff.intro, Exists.intro, Eq.symm, Eq, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → γ
p : γ → Prop
⊢ (∃ (c : γ), (∃ (a : α), ∃ (b : β), f a b = c) ∧ p c) ↔ ∃ (a : α), ∃ (b : β), p (f a b)

Tactic:
⟨fun ⟨_, ⟨a, b, hab⟩, hc⟩ ↦ ⟨a, b, hab.symm ▸ hc⟩,
    fun ⟨a, b, hab⟩ ↦ ⟨f a b, ⟨a, b, rfl⟩, hab⟩⟩

Premises used: _private.0.exists_exists_exists_and_eq.match_1, Exists, _private.0.exists_exists_exists_and_eq.match_2, Eq.rec, And, And.intro, Iff.intro, Exists.intro, Eq.symm, Eq, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp
-- Module: Mathlib.Logic.Basic
Goal:
ι₁ : Sort u_3
ι₂ : Sort u_4
κ₁ : ι₁ → Sort u_5
κ₂ : ι₂ → Sort u_6
p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop
⊢ (∃ (i₁ : ι₁), ∃ (j₁ : κ₁ i₁), ∃ (i₂ : ι₂), ∃ (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ↔
    ∃ (i₂ : ι₂), ∃ (j₂ : κ₂ i₂), ∃ (i₁ : ι₁), ∃ (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂

Tactic:
simp only [@exists_comm (κ₁ _), @exists_comm ι₁]

Premises used: exists_comm
-- Module: Mathlib.Logic.Basic
Goal:
p q : Prop
f : p ∧ q → Prop
⊢ (∃ (h : p ∧ q), f h) ↔ ∃ (hp : p), ∃ (hq : q), f ⋯

Tactic:
⟨fun ⟨h, H⟩ ↦ ⟨h.1, h.2, H⟩, fun ⟨hp, hq, H⟩ ↦ ⟨⟨hp, hq⟩, H⟩⟩

Premises used: _private.0.And.exists.match_1, Exists, _private.0.And.exists.match_2, And.right, And.left, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
p : α → Prop
b : Prop
h : b ∨ ∀ (x : α), p x
x : α
⊢ b ∨ p x

Tactic:
h.imp_right fun h₂ ↦ h₂ x

Premises used: Or.imp_right
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
q : Prop
p : α → Prop
inst : Decidable q
⊢ (∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x

Tactic:
⟨fun h ↦ if hq : q then Or.inl hq else
    Or.inr fun x ↦ (h x).resolve_left hq, forall_or_of_or_forall⟩

Premises used: Or.resolve_left, dite, forall_or_of_or_forall, Iff.intro, Or.inl, Or.inr
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
q : Prop
p : α → Prop
⊢ (∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x

Tactic:
open scoped Classical in Decidable.forall_or_left

Premises used: Decidable.forall_or_left
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
q : Prop
p : α → Prop
inst : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

Tactic:
simp [or_comm, Decidable.forall_or_left]

Premises used: Decidable.forall_or_left, or_comm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
q : Prop
p : α → Prop
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

Tactic:
open scoped Classical in Decidable.forall_or_right

Premises used: Decidable.forall_or_right
-- Module: Mathlib.Logic.Basic
Goal:
p q : Prop
r : p ∧ q → Prop
⊢ (∀ (h : p ∧ q), r h) ↔ ∀ (hp : p) (hq : q), r ⋯

Tactic:
⟨fun h hp hq ↦ h ⟨hp, hq⟩, fun h h1 ↦ h h1.1 h1.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Logic.Basic
Goal:
p q : Prop
r : p → q → Prop
⊢ (∀ (hp : p) (hq : q), r hp hq) ↔ ∀ (h : p ∧ q), r ⋯ ⋯

Tactic:
(forall_and_index (r := fun h => r h.1 h.2)).symm

Premises used: Iff.symm, forall_and_index
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop → Prop
h : ∃ (h : Prop), p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True

Tactic:
simpa only [H] using h₂
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop → Prop
h : ∃ (h : Prop), p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False

Tactic:
simpa only [H] using h₂
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop → Prop
h_1 : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
pos : ∀ (H : h), p h
neg : ∀ (H : ¬h), p h
⊢ p h

Tactic:
by_cases H : h
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop → Prop
h_1 : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : h
⊢ p h

Tactic:
simpa only [H]
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop → Prop
h_1 : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : ¬h
⊢ p h

Tactic:
simpa only [H]
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
q : p → Prop
h : ∀ (h : p), q h
⊢ (∃ (h : p), q h) ↔ p

Tactic:
⟨Exists.fst, fun H ↦ ⟨H, h H⟩⟩

Premises used: Exists.fst, Iff.intro, Exists.intro
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
q : p → Prop
⊢ ¬p → ¬∃ (h' : p), q h'

Tactic:
mt Exists.fst

Premises used: mt, Exists.fst
-- Module: Mathlib.Logic.Basic
Goal:
p p' : Prop
q q' : p → Prop
hq : ∀ (h : p), q h ↔ q' h
hp : p ↔ p'
⊢ (∀ (h : p), q h) ↔ ∀ (h : p'), q' ⋯

Tactic:
⟨fun h1 h2 ↦ (hq _).1 (h1 (hp.2 h2)), fun h1 h2 ↦ (hq _).2 (h1 (hp.1 h2))⟩

Premises used: Iff.mpr, Iff.intro, Iff.mp
-- Module: Mathlib.Logic.Basic
Goal:
p p' : Prop
q q' : p → Prop
hq : ∀ (h : p), q h ↔ q' h
hp : p ↔ p'
⊢ Eq (α := Prop) (∀ (h : p), q h) (∀ (h : p'), q' ⋯)

Tactic:
propext (forall_prop_congr hq hp)

Premises used: forall_prop_congr, propext
-- Module: Mathlib.Logic.Basic
Goal:
a b c d : Prop
h₁ : a = c
h₂ : b = d
⊢ Eq (α := Prop) (a → b) (c → d)

Tactic:
propext (imp_congr h₁.to_iff h₂.to_iff)

Premises used: Eq.to_iff, imp_congr, propext
-- Module: Mathlib.Logic.Basic
Goal:
a b c d : Prop
h₁ : a = c
h₂ : c → b = d
⊢ Eq (α := Prop) (a → b) (c → d)

Tactic:
propext (imp_congr_ctx h₁.to_iff fun hc ↦ (h₂ hc).to_iff)

Premises used: Eq.to_iff, propext, imp_congr_ctx
-- Module: Mathlib.Logic.Basic
Goal:
a : Prop
h : a
⊢ a = True

Tactic:
propext (iff_true_intro h)

Premises used: propext, iff_true_intro
-- Module: Mathlib.Logic.Basic
Goal:
a : Prop
h : ¬a
⊢ a = False

Tactic:
propext (iff_false_intro h)

Premises used: iff_false_intro, propext
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (a ↔ b) = (a = b)

Tactic:
propext ⟨propext, Eq.to_iff⟩

Premises used: Eq.to_iff, Iff.intro, propext
-- Module: Mathlib.Logic.Basic
Goal:
p : True → Prop
⊢ (∀ (x : True), p x) ↔ p True.intro

Tactic:
forall_prop_of_true _

Premises used: forall_prop_of_true
-- Module: Mathlib.Logic.Basic
Goal:
ι : Sort u_3
inst : Subsingleton ι
P : ι → ι → Prop
⊢ (∀ (i j : ι), P i j) ↔ ∀ (i : ι), P i i

Tactic:
forall_congr' fun i ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Logic.Basic
Goal:
ι : Sort u_3
inst : Subsingleton ι
P : ι → ι → Prop
refine : ∀ (i : ι), (∀ (j : ι), P i j) ↔ P i i
⊢ (∀ (i j : ι), P i j) ↔ ∀ (i : ι), P i i

Tactic:
refine forall_congr' fun i ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Logic.Basic
Goal:
ι : Sort u_3
inst : Subsingleton ι
P : ι → ι → Prop
i : ι
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨i⟩
-- Module: Mathlib.Logic.Basic
Goal:
ι : Sort u_3
inst : Subsingleton ι
P : ι → ι → Prop
i : ι
this : Nonempty ι
⊢ (∀ (j : ι), P i j) ↔ P i i

Tactic:
simp [Subsingleton.elim _ i]

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
⊢ Decidable p

Tactic:
infer_instance
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
⊢ DecidablePred p

Tactic:
infer_instance
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → α → Prop
⊢ DecidableRel p

Tactic:
infer_instance
-- Module: Mathlib.Logic.Basic
Goal:
α_1 : Sort u_1
α : Sort u_2
⊢ DecidableEq α

Tactic:
infer_instance
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_2
p : α → Prop
h : ∃ (a : α), p a
q : α → Prop
hpq : ∀ (a : α), p a → q a
⊢ q (choose (p := p) h)

Tactic:
hpq _ <| choose_spec _

Premises used: Classical.choose_spec
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a : α
⊢ ⋯.choose (p := fun (x : α) ↦ x = a) = a

Tactic:
@choose_spec _ (· = a) _

Premises used: Classical.choose_spec
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a : α
⊢ ⋯.choose (p := fun (x : α) ↦ a = x) = a

Tactic:
(@choose_spec _ (a = ·) _).symm

Premises used: Classical.choose_spec, Eq.symm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p q : α → Prop
⊢ (∃ (x : α), ∃ (x_1 : p x), q x) ↔ ∃ (x : α), p x ∧ q x

Tactic:
⟨fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩, fun ⟨x, px, qx⟩ ↦ ⟨x, px, qx⟩⟩

Premises used: _private.0.bex_def.match_1, _private.0.bex_def.match_2, Exists, And, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
P : (x : α) → p x → Prop
a : α
h₁ : p a
h₂ : P a h₁
⊢ ∃ (x : α), ∃ (h : p x), P x h

Tactic:
⟨a, h₁, h₂⟩

Premises used: Exists.intro
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
P Q : (x : α) → p x → Prop
H : ∀ (x : α) (h : p x), P x h → Q x h
h₁ : ∀ (x : α) (h : p x), P x h
x : α
h : p x
⊢ Q x h

Tactic:
H _ _ <| h₁ _ _
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
r p q : α → Prop
H : ∀ (x : α), p x → q x
h₁ : ∀ (x : α), q x → r x
x : α
h : p x
⊢ r x

Tactic:
h₁ _ <| H _ h
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
P : (x : α) → p x → Prop
⊢ (¬∃ (x : α), ∃ (h : p x), P x h) ↔ ∀ (x : α) (h : p x), ¬P x h

Tactic:
exists₂_imp

Premises used: exists₂_imp, Not
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
P : (x : α) → p x → Prop
inst : Decidable (∃ (x : α), ∃ (h : p x), ¬P x h)
inst_1 : (x : α) → (h : p x) → Decidable (P x h)
⊢ (¬∀ (x : α) (h : p x), P x h) ↔ ∃ (x : α), ∃ (h : p x), ¬P x h

Tactic:
⟨Not.decidable_imp_symm fun nx x h ↦ nx.decidable_imp_symm
    fun h' ↦ ⟨x, h, h'⟩, not_forall₂_of_exists₂_not⟩

Premises used: Not.decidable_imp_symm, Iff.intro, not_forall₂_of_exists₂_not
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
P : (x : α) → p x → Prop
⊢ (¬∀ (x : α) (h : p x), P x h) ↔ ∃ (x : α), ∃ (h : p x), ¬P x h

Tactic:
open scoped Classical in Decidable.not_forall₂

Premises used: Decidable.not_forall₂
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
P Q : (x : α) → p x → Prop
⊢ (∀ (x : α) (h : p x), P x h ∧ Q x h) ↔ (∀ (x : α) (h : p x), P x h) ∧ ∀ (x : α) (h : p x), Q x h

Tactic:
Iff.trans (forall_congr' fun _ ↦ forall_and) forall_and

Premises used: forall_congr', Iff.trans, forall_and
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
inst : Nonempty α
q : Prop
p : α → Prop
rw : ((∀ (x : α), q) ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x
rw₁ rw₂ : (q ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x
⊢ (∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x

Tactic:
rw [forall_and, forall_const]

Premises used: forall_const, forall_and
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
inst : Nonempty α
p : α → Prop
q : Prop
rw : ((∀ (x : α), p x) ∧ ∀ (x : α), q) ↔ (∀ (x : α), p x) ∧ q
rw₁ rw₂ : (∀ (x : α), p x) ∧ q ↔ (∀ (x : α), p x) ∧ q
⊢ (∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q

Tactic:
rw [forall_and, forall_const]

Premises used: forall_const, forall_and
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
P Q : (x : α) → p x → Prop
⊢ (∃ (x : α), ∃ (h : p x), P x h ∨ Q x h) ↔ (∃ (x : α), ∃ (h : p x), P x h) ∨ ∃ (x : α), ∃ (h : p x), Q x h

Tactic:
Iff.trans (exists_congr fun _ ↦ exists_or) exists_or

Premises used: exists_or, exists_congr, Iff.trans
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
r p q : α → Prop
⊢ (∀ (x : α), p x ∨ q x → r x) ↔ (∀ (x : α), p x → r x) ∧ ∀ (x : α), q x → r x

Tactic:
Iff.trans (forall_congr' fun _ ↦ or_imp) forall_and

Premises used: or_imp, forall_congr', Iff.trans, forall_and
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
r p q : α → Prop
simp : (∃ (x : α), (p x ∨ q x) ∧ r x) ↔ (∃ (x : α), p x ∧ r x) ∨ ∃ (x : α), q x ∧ r x
⊢ (∃ (x : α), ∃ (x_1 : p x ∨ q x), r x) ↔ (∃ (x : α), ∃ (x_1 : p x), r x) ∨ ∃ (x : α), ∃ (x_1 : q x), r x

Tactic:
simp only [exists_prop]

Premises used: exists_prop
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
r p q : α → Prop
⊢ (∃ (x : α), (p x ∨ q x) ∧ r x) ↔ (∃ (x : α), p x ∧ r x) ∨ ∃ (x : α), q x ∧ r x

Tactic:
Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

Premises used: exists_or, exists_congr, Iff.trans, or_and_right
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
r p q : α → Prop
⊢ (∃ (x : α), (p x ∨ q x) ∧ r x) ↔ (∃ (x : α), p x ∧ r x) ∨ ∃ (x : α), q x ∧ r x

Tactic:
exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

Premises used: exists_or, exists_congr, Iff.trans, or_and_right
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
c : α
A : P → α
B : ¬P → α
pos : P → (dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c)
neg : ¬P → (dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c)
⊢ dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c

Tactic:
by_cases P
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
c : α
A : P → α
B : ¬P → α
h : P
⊢ dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c

Tactic:
simp [*, exists_prop_of_true, exists_prop_of_false]

Premises used: exists_prop_of_false, exists_prop_of_true
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
c : α
A : P → α
B : ¬P → α
h : ¬P
⊢ dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c

Tactic:
simp [*, exists_prop_of_true, exists_prop_of_false]

Premises used: exists_prop_of_false, exists_prop_of_true
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b c : α
rw : (P ∧ a = c ∨ ∃ (h : ¬P), b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
rw₁ rw₂ : P ∧ a = c ∨ ¬P ∧ b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c
⊢ ((∃ (h : P), a = c) ∨ ∃ (h : ¬P), b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c

Tactic:
rw [exists_prop, exists_prop]

Premises used: exists_prop
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b c : α
⊢ (a = if P then b else c) ↔ P ∧ a = b ∨ ¬P ∧ a = c

Tactic:
eq_comm.trans <| ite_eq_iff.trans <| (Iff.rfl.and eq_comm).or (Iff.rfl.and eq_comm)

Premises used: Iff.rfl, eq_comm, Iff.or, Iff.and, Iff.trans, ite_eq_iff
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∀ (h : P), A h = c) ∧ ∀ (h : ¬P), B h = c

Tactic:
⟨fun he ↦ ⟨fun h ↦ (dif_pos h).symm.trans he, fun h ↦ (dif_neg h).symm.trans he⟩, fun he ↦
    (em P).elim (fun h ↦ (dif_pos h).trans <| he.1 h) fun h ↦ (dif_neg h).trans <| he.2 h⟩

Premises used: em, dif_pos, dif_neg, And.right, And.left, And.intro, Iff.intro, Or.elim, Eq.symm, Eq.trans
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b c : α
⊢ (if P then a else b) = c ↔ (P → a = c) ∧ (¬P → b = c)

Tactic:
dite_eq_iff'

Premises used: dite_eq_iff', ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a : α
B : ¬P → α
⊢ dite P (fun (x : P) ↦ a) B ≠ a ↔ ∃ (h : ¬P), a ≠ B h

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
b : α
A : P → α
⊢ (dite P A fun (x : ¬P) ↦ b) ≠ b ↔ ∃ (h : P), A h ≠ b

Tactic:
simp only [Ne, dite_eq_right_iff, not_forall]

Premises used: dite_eq_right_iff, Ne, Classical.not_forall
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
rw rw₁ : ¬P ∧ a ≠ b ↔ ¬P ∧ a ≠ b
⊢ (∃ (h : ¬P), a ≠ b) ↔ ¬P ∧ a ≠ b

Tactic:
rw [exists_prop]

Premises used: exists_prop
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
rw rw₁ : P ∧ a ≠ b ↔ P ∧ a ≠ b
⊢ (∃ (h : P), a ≠ b) ↔ P ∧ a ≠ b

Tactic:
rw [exists_prop]

Premises used: exists_prop
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a : α
B : ¬P → α
h : ∀ (h : ¬P), a ≠ B h
⊢ dite P (fun (x : P) ↦ a) B = a ↔ P

Tactic:
dite_eq_left_iff.trans ⟨fun H ↦ of_not_not fun h' ↦ h h' (H h').symm, fun h H ↦ (H h).elim⟩

Premises used: False.elim, Iff.intro, of_not_not, Iff.trans, Eq.symm, dite_eq_left_iff
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
b : α
A : P → α
h : ∀ (h : P), A h ≠ b
⊢ (dite P A fun (x : ¬P) ↦ b) = b ↔ ¬P

Tactic:
dite_eq_right_iff.trans ⟨fun H h' ↦ h h' (H h'), fun h' H ↦ (h' H).elim⟩

Premises used: False.elim, dite_eq_right_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
h : a ≠ b
⊢ (if P then a else b) = a ↔ P

Tactic:
Ne.dite_eq_left_iff fun _ ↦ h

Premises used: Ne.dite_eq_left_iff, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
h : a ≠ b
⊢ (if P then a else b) = b ↔ ¬P

Tactic:
Ne.dite_eq_right_iff fun _ ↦ h

Premises used: Ne.dite_eq_right_iff, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a : α
B : ¬P → α
h : ∀ (h : ¬P), a ≠ B h
⊢ dite P (fun (x : P) ↦ a) B ≠ a ↔ ¬P

Tactic:
dite_ne_left_iff.trans <| exists_iff_of_forall h

Premises used: exists_iff_of_forall, dite_ne_left_iff, Iff.trans
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
b : α
A : P → α
h : ∀ (h : P), A h ≠ b
⊢ (dite P A fun (x : ¬P) ↦ b) ≠ b ↔ P

Tactic:
dite_ne_right_iff.trans <| exists_iff_of_forall h

Premises used: exists_iff_of_forall, dite_ne_right_iff, Iff.trans
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
h : a ≠ b
⊢ (if P then a else b) ≠ a ↔ ¬P

Tactic:
Ne.dite_ne_left_iff fun _ ↦ h

Premises used: Ne.dite_ne_left_iff, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
h : a ≠ b
⊢ (if P then a else b) ≠ b ↔ P

Tactic:
Ne.dite_ne_right_iff fun _ ↦ h

Premises used: Ne.dite_ne_right_iff, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
A : P → α
B : ¬P → α
⊢ (∃ (h : P), dite P A B = A h) ∨ ∃ (h : ¬P), dite P A B = B h

Tactic:
if h : _ then .inl ⟨h, dif_pos h⟩ else .inr ⟨h, dif_neg h⟩
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
⊢ (if P then a else b) = a ∨ (if P then a else b) = b

Tactic:
if h : _ then .inl (if_pos h) else .inr (if_neg h)
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
pos : ∀ (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)
neg : ∀ (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)
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
by_cases h : P
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
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)

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
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)

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst : Decidable P
a b : α
c d : β
⊢ f (if P then a else b) (if P then c else d) = if P then f a c else f b d

Tactic:
apply_dite₂ f P (fun _ ↦ a) (fun _ ↦ b) (fun _ ↦ c) fun _ ↦ d

Premises used: apply_dite₂, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
pos : ∀ (h : P), dite P f g a = if h : P then f h a else g h a
neg : ∀ (h : ¬P), dite P f g a = if h : P then f h a else g h a
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
by_cases h : P
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst : Decidable 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

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst : Decidable 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

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst : Decidable P
f g : (a : α) → σ a
a : α
⊢ (if P then f else g) a = if P then f a else g a

Tactic:
dite_apply P (fun _ ↦ f) (fun _ ↦ g) a

Premises used: dite_apply, ite
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst : Decidable P
x y : α
z : β
⊢ f (if P then x else y) z = if P then f x z else f y z

Tactic:
grind