awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
⊢ IsEmpty.{max 1 u} { _a : α // False }

Tactic:
Subtype.isEmpty_of_false fun _ ↦ id

Premises used: id, Subtype.isEmpty_of_false
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α_1 : Sort u
β : Sort v
α : Type u_1
inst : IsEmpty α
E : α → Type v
⊢ IsEmpty (Sigma E)

Tactic:
Function.isEmpty Sigma.fst

Premises used: Function.isEmpty, Sigma.fst
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
h : Nonempty α
inst : IsEmpty β
⊢ IsEmpty (α → β)

Tactic:
infer_instance
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
⊢ IsEmpty α ↔ ∀ (a : α), False

Tactic:
⟨@IsEmpty.false α, IsEmpty.mk⟩

Premises used: IsEmpty.mk, Iff.intro, IsEmpty.false
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
p : Prop
⊢ IsEmpty p ↔ ¬p

Tactic:
isEmpty_iff

Premises used: isEmpty_iff, Not
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
inst : IsEmpty α
p : α → Prop
⊢ (∀ (a : α), p a) ↔ True

Tactic:
iff_true_intro isEmptyElim

Premises used: isEmptyElim, iff_true_intro
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
inst : IsEmpty α
p : α → Prop
⊢ (∃ (a : α), p a) ↔ False

Tactic:
iff_false_intro fun ⟨x, _⟩ ↦ IsEmpty.false x

Premises used: False, _private.0.IsEmpty.exists_iff.match_1, iff_false_intro, IsEmpty.false
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty α
⊢ Subsingleton α

Tactic:
⟨isEmptyElim⟩

Premises used: isEmptyElim, Subsingleton.intro
-- Module: Mathlib.Logic.Lemmas
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → (a ↔ (b ↔ c))
mpr : (a ↔ (b ↔ c)) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₂ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₃ : (a ↔ b) → c → (a ↔ (b ↔ c))
mp₄ : ¬(a ↔ b) → ¬c → (a ↔ (b ↔ c))
mp₅ : (a ↔ b) → c → a → (b ↔ c)
mp₆ : (a ↔ b) → c → (b ↔ c) → a
mp₇ : ¬(a ↔ b) → ¬c → a → (b ↔ c)
mp₈ : ¬(a ↔ b) → ¬c → (b ↔ c) → a
mpr₁ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₂ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₃ : a → (b ↔ c) → ((a ↔ b) ↔ c)
mpr₄ : ¬a → ¬(b ↔ c) → ((a ↔ b) ↔ c)
mpr₅ : a → (b ↔ c) → (a ↔ b) → c
mpr₆ : a → (b ↔ c) → c → (a ↔ b)
mpr₇ : ¬a → ¬(b ↔ c) → (a ↔ b) → c
mpr₈ : ¬a → ¬(b ↔ c) → c → (a ↔ b)
mp₉ : c → a → a → b → (b ↔ c)
mp₁₀ : c → a → ¬a → ¬b → (b ↔ c)
mp₁₁ : c → a → a → b → (b ↔ c)
mp₁₂ : c → a → a → b → b → c
mp₁₃ : c → a → a → b → c → b
mp₁₄ : c → a → b → b → c → a
mp₁₅ : c → a → b → ¬b → ¬c → a
mp₁₆ : c → ¬a → ¬b → b → c → a
mp₁₇ : c → ¬a → ¬b → ¬b → ¬c → a
mp₁₈ mp₁₉ : c → a → b → b → c → a
mp₂₀ : ¬c → a → ¬a → b → (b ↔ c)
mp₂₁ mp₂₂ : ¬c → a → ¬¬a → ¬b → (b ↔ c)
mp₂₃ : ¬c → a → ¬¬a → ¬b → b → c
mp₂₄ : ¬c → a → ¬¬a → ¬b → c → b
mp₂₅ : ¬c → ¬a → b → b → c → a
mp₂₆ : ¬c → ¬a → b → ¬b → ¬c → a
mp₂₇ : ¬c → ¬¬a → ¬b → b → c → a
mp₂₈ mp₂₉ mp₃₀ : ¬c → ¬¬a → ¬b → ¬b → ¬c → a
mpr₉ : a → b → c → a → b → c
mpr₁₀ : a → b → c → ¬a → ¬b → c
mpr₁₁ : a → ¬b → ¬c → a → b → c
mpr₁₂ : a → ¬b → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : a → b → c → a → b → c
mpr₁₅ : a → c → b → c → (a ↔ b)
mpr₁₆ : a → c → ¬b → ¬c → (a ↔ b)
mpr₁₇ : a → c → b → c → (a ↔ b)
mpr₁₈ : a → c → b → c → a → b
mpr₁₉ : a → c → b → c → b → a
mpr₂₀ : ¬a → ¬b → c → a → b → c
mpr₂₁ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₂ : ¬a → ¬¬b → ¬c → a → b → c
mpr₂₃ : ¬a → ¬¬b → ¬c → ¬a → ¬b → c
mpr₂₄ mpr₂₅ : ¬a → ¬b → c → ¬a → ¬b → c
mpr₂₆ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₇ : ¬a → c → ¬¬b → ¬c → (a ↔ b)
mpr₂₈ : ¬a → c → ¬b → c → (a ↔ b)
mpr₂₉ : ¬a → c → ¬b → c → a → b
mpr₃₀ : ¬a → c → ¬b → c → b → a
mp₃₁ mp₃₂ mp₃₃ : c → a → a → b → b → c
mp₃₄ mp₃₅ mp₃₆ : c → a → a → b → c → b
mp₃₇ : ¬c → a → a → ¬b → b → c
mp₃₈ : ¬c → a → a → ¬b → c → b
mp₃₉ mp₄₀ mp₄₁ : ¬c → a → ¬b → ¬b → ¬c → a
mpr₃₁ mpr₃₂ mpr₃₃ : a → c → b → c → a → b
mpr₃₄ mpr₃₅ mpr₃₆ : a → c → b → c → b → a
mpr₃₇ : ¬a → c → ¬b → c → a → b
mpr₃₈ : ¬a → c → ¬b → c → b → a
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))

Tactic:
tauto
-- Module: Mathlib.Logic.Lemmas
Goal:
a b c : Prop
mp : (a ↔ (b ↔ c)) → (b ↔ (a ↔ c))
mpr : (b ↔ (a ↔ c)) → (a ↔ (b ↔ c))
mp₁ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₂ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₃ : a → (b ↔ c) → (b ↔ (a ↔ c))
mp₄ : ¬a → ¬(b ↔ c) → (b ↔ (a ↔ c))
mp₅ : a → (b ↔ c) → b → (a ↔ c)
mp₆ : a → (b ↔ c) → (a ↔ c) → b
mp₇ : ¬a → ¬(b ↔ c) → b → (a ↔ c)
mp₈ : ¬a → ¬(b ↔ c) → (a ↔ c) → b
mpr₁ : b → (a ↔ c) → (a ↔ (b ↔ c))
mpr₂ : ¬b → ¬(a ↔ c) → (a ↔ (b ↔ c))
mpr₃ : b → (a ↔ c) → (a ↔ (b ↔ c))
mpr₄ : ¬b → ¬(a ↔ c) → (a ↔ (b ↔ c))
mpr₅ : b → (a ↔ c) → a → (b ↔ c)
mpr₆ : b → (a ↔ c) → (b ↔ c) → a
mpr₇ : ¬b → ¬(a ↔ c) → a → (b ↔ c)
mpr₈ : ¬b → ¬(a ↔ c) → (b ↔ c) → a
mp₉ : a → b → b → c → (a ↔ c)
mp₁₀ : a → b → ¬b → ¬c → (a ↔ c)
mp₁₁ : a → b → b → c → (a ↔ c)
mp₁₂ : a → b → b → c → a → c
mp₁₃ : a → b → b → c → c → a
mp₁₄ : a → b → c → a → c → b
mp₁₅ : a → b → c → ¬a → ¬c → b
mp₁₆ : a → ¬b → ¬c → a → c → b
mp₁₇ : a → ¬b → ¬c → ¬a → ¬c → b
mp₁₈ mp₁₉ : a → b → c → a → c → b
mp₂₀ : ¬a → b → ¬b → c → (a ↔ c)
mp₂₁ mp₂₂ : ¬a → b → ¬¬b → ¬c → (a ↔ c)
mp₂₃ : ¬a → b → ¬¬b → ¬c → a → c
mp₂₄ : ¬a → b → ¬¬b → ¬c → c → a
mp₂₅ : ¬a → ¬b → c → a → c → b
mp₂₆ : ¬a → ¬b → c → ¬a → ¬c → b
mp₂₇ : ¬a → ¬¬b → ¬c → a → c → b
mp₂₈ mp₂₉ mp₃₀ : ¬a → ¬¬b → ¬c → ¬a → ¬c → b
mpr₉ : b → a → a → c → (b ↔ c)
mpr₁₀ : b → a → ¬a → ¬c → (b ↔ c)
mpr₁₁ : b → a → a → c → (b ↔ c)
mpr₁₂ : b → a → a → c → b → c
mpr₁₃ : b → a → a → c → c → b
mpr₁₄ : b → a → c → b → c → a
mpr₁₅ : b → a → c → ¬b → ¬c → a
mpr₁₆ : b → ¬a → ¬c → b → c → a
mpr₁₇ : b → ¬a → ¬c → ¬b → ¬c → a
mpr₁₈ mpr₁₉ : b → a → c → b → c → a
mpr₂₀ : ¬b → a → ¬a → c → (b ↔ c)
mpr₂₁ mpr₂₂ : ¬b → a → ¬¬a → ¬c → (b ↔ c)
mpr₂₃ : ¬b → a → ¬¬a → ¬c → b → c
mpr₂₄ : ¬b → a → ¬¬a → ¬c → c → b
mpr₂₅ : ¬b → ¬a → c → b → c → a
mpr₂₆ : ¬b → ¬a → c → ¬b → ¬c → a
mpr₂₇ : ¬b → ¬¬a → ¬c → b → c → a
mpr₂₈ mpr₂₉ mpr₃₀ : ¬b → ¬¬a → ¬c → ¬b → ¬c → a
mp₃₁ mp₃₂ mp₃₃ : a → b → b → c → a → c
mp₃₄ mp₃₅ mp₃₆ : a → b → b → c → c → a
mp₃₇ : ¬a → b → b → ¬c → a → c
mp₃₈ : ¬a → b → b → ¬c → c → a
mp₃₉ mp₄₀ mp₄₁ : ¬a → b → ¬c → ¬a → ¬c → b
mpr₃₁ mpr₃₂ mpr₃₃ : b → a → a → c → b → c
mpr₃₄ mpr₃₅ mpr₃₆ : b → a → a → c → c → b
mpr₃₇ : ¬b → a → a → ¬c → b → c
mpr₃₈ : ¬b → a → a → ¬c → c → b
mpr₃₉ mpr₄₀ mpr₄₁ : ¬b → a → ¬c → ¬b → ¬c → a
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))

Tactic:
tauto
-- Module: Mathlib.Logic.Lemmas
Goal:
a b c : Prop
mp : ((a ↔ b) ↔ c) → ((a ↔ c) ↔ b)
mpr : ((a ↔ c) ↔ b) → ((a ↔ b) ↔ c)
mp₁ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₂ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₃ : (a ↔ b) → c → ((a ↔ c) ↔ b)
mp₄ : ¬(a ↔ b) → ¬c → ((a ↔ c) ↔ b)
mp₅ : (a ↔ b) → c → (a ↔ c) → b
mp₆ : (a ↔ b) → c → b → (a ↔ c)
mp₇ : ¬(a ↔ b) → ¬c → (a ↔ c) → b
mp₈ : ¬(a ↔ b) → ¬c → b → (a ↔ c)
mpr₁ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₂ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₃ : (a ↔ c) → b → ((a ↔ b) ↔ c)
mpr₄ : ¬(a ↔ c) → ¬b → ((a ↔ b) ↔ c)
mpr₅ : (a ↔ c) → b → (a ↔ b) → c
mpr₆ : (a ↔ c) → b → c → (a ↔ b)
mpr₇ : ¬(a ↔ c) → ¬b → (a ↔ b) → c
mpr₈ : ¬(a ↔ c) → ¬b → c → (a ↔ b)
mp₉ : c → a → b → a → c → b
mp₁₀ : c → a → b → ¬a → ¬c → b
mp₁₁ : c → ¬a → ¬b → a → c → b
mp₁₂ : c → ¬a → ¬b → ¬a → ¬c → b
mp₁₃ mp₁₄ : c → a → b → a → c → b
mp₁₅ : c → b → a → b → (a ↔ c)
mp₁₆ : c → b → ¬a → ¬b → (a ↔ c)
mp₁₇ : c → b → a → b → (a ↔ c)
mp₁₈ : c → b → a → b → a → c
mp₁₉ : c → b → a → b → c → a
mp₂₀ : ¬c → ¬a → b → a → c → b
mp₂₁ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₂ : ¬c → ¬¬a → ¬b → a → c → b
mp₂₃ : ¬c → ¬¬a → ¬b → ¬a → ¬c → b
mp₂₄ mp₂₅ : ¬c → ¬a → b → ¬a → ¬c → b
mp₂₆ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₇ : ¬c → b → ¬¬a → ¬b → (a ↔ c)
mp₂₈ : ¬c → b → ¬a → b → (a ↔ c)
mp₂₉ : ¬c → b → ¬a → b → a → c
mp₃₀ : ¬c → b → ¬a → b → c → a
mpr₉ : b → a → c → a → b → c
mpr₁₀ : b → a → c → ¬a → ¬b → c
mpr₁₁ : b → ¬a → ¬c → a → b → c
mpr₁₂ : b → ¬a → ¬c → ¬a → ¬b → c
mpr₁₃ mpr₁₄ : b → a → c → a → b → c
mpr₁₅ : b → c → a → c → (a ↔ b)
mpr₁₆ : b → c → ¬a → ¬c → (a ↔ b)
mpr₁₇ : b → c → a → c → (a ↔ b)
mpr₁₈ : b → c → a → c → a → b
mpr₁₉ : b → c → a → c → b → a
mpr₂₀ : ¬b → ¬a → c → a → b → c
mpr₂₁ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₂ : ¬b → ¬¬a → ¬c → a → b → c
mpr₂₃ : ¬b → ¬¬a → ¬c → ¬a → ¬b → c
mpr₂₄ mpr₂₅ : ¬b → ¬a → c → ¬a → ¬b → c
mpr₂₆ : ¬b → c → ¬a → c → (a ↔ b)
mpr₂₇ : ¬b → c → ¬¬a → ¬c → (a ↔ b)
mpr₂₈ : ¬b → c → ¬a → c → (a ↔ b)
mpr₂₉ : ¬b → c → ¬a → c → a → b
mpr₃₀ : ¬b → c → ¬a → c → b → a
mp₃₁ mp₃₂ mp₃₃ : c → b → a → b → a → c
mp₃₄ mp₃₅ mp₃₆ : c → b → a → b → c → a
mp₃₇ : ¬c → b → ¬a → b → a → c
mp₃₈ : ¬c → b → ¬a → b → c → a
mpr₃₁ mpr₃₂ mpr₃₃ : b → c → a → c → a → b
mpr₃₄ mpr₃₅ mpr₃₆ : b → c → a → c → b → a
mpr₃₇ : ¬b → c → ¬a → c → a → b
mpr₃₈ : ¬b → c → ¬a → c → b → a
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)

Tactic:
tauto
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
pos : ∀ (h : p), q → a h = a h
neg : ∀ (h : p), ¬q → a h = a h
pos₁ : ∀ (h : ¬p) (h_1 : q), b h h_1 = b h ⋯
neg₁ : ∀ (h : ¬p) (h_1 : ¬q), c h h_1 = c h ⋯
⊢ (dite p a fun (hp : ¬p) ↦ dite q (b hp) (c hp)) =
    if hq : q then dite p a fun (hp : ¬p) ↦ b hp hq else dite p a fun (hp : ¬p) ↦ c hp hq

Tactic:
split_ifs
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h : p
h_1 : q
⊢ a h = a h

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h : p
h_1 : ¬q
⊢ a h = a h

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h : ¬p
h_1 : q
⊢ b h h_1 = b h ⋯

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b : ¬p → q → α
c : ¬p → ¬q → α
h : ¬p
h_1 : ¬q
⊢ c h h_1 = c h ⋯

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
pos : ∀ (h : p) (h_1 : q), a h h_1 = a h ⋯
neg : ∀ (h : p) (h_1 : ¬q), b h h_1 = b h ⋯
pos₁ : ∀ (h : ¬p), q → c h = c h
neg₁ : ∀ (h : ¬p), ¬q → c h = c h
⊢ dite p (fun (hp : p) ↦ dite q (a hp) (b hp)) c =
    if hq : q then dite p (fun (hp : p) ↦ a hp hq) c else dite p (fun (hp : p) ↦ b hp hq) c

Tactic:
split_ifs
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h : p
h_1 : q
⊢ a h h_1 = a h ⋯

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h : p
h_1 : ¬q
⊢ b h h_1 = b h ⋯

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h : ¬p
h_1 : q
⊢ c h = c h

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → q → α
b : p → ¬q → α
c : ¬p → α
h : ¬p
h_1 : ¬q
⊢ c h = c h

Tactic:
rfl
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : α
b : q → α
c : ¬q → α
⊢ (if p then a else dite q b c) = if hq : q then if p then a else b hq else if p then a else c hq

Tactic:
dite_dite_distrib_left

Premises used: dite_dite_distrib_left, ite
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : q → α
b : ¬q → α
c : α
⊢ (if p then dite q a b else c) = if hq : q then if p then a hq else c else if p then b hq else c

Tactic:
dite_dite_distrib_right

Premises used: dite_dite_distrib_right, ite
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a : p → α
b c : ¬p → α
⊢ (dite p a fun (hp : ¬p) ↦ if q then b hp else c hp) = if q then dite p a b else dite p a c

Tactic:
dite_dite_distrib_left

Premises used: dite_dite_distrib_left, ite
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a b : p → α
c : ¬p → α
⊢ dite p (fun (hp : p) ↦ if q then a hp else b hp) c = if q then dite p a c else dite p b c

Tactic:
dite_dite_distrib_right

Premises used: dite_dite_distrib_right, ite
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a b c : α
⊢ (if p then a else if q then b else c) = if q then if p then a else b else if p then a else c

Tactic:
dite_dite_distrib_left

Premises used: dite_dite_distrib_left, ite
-- Module: Mathlib.Logic.Lemmas
Goal:
α : Sort u_1
p q : Prop
inst : Decidable p
inst_1 : Decidable q
a b c : α
⊢ (if p then if q then a else b else c) = if q then if p then a else c else if p then b else c

Tactic:
dite_dite_distrib_right

Premises used: dite_dite_distrib_right, ite
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
pos : ∀ (hp : p), f p
neg : ∀ (hp : ¬p), f p
⊢ f p

Tactic:
by_cases hp : p
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
pos : f True
⊢ f p

Tactic:
simp only [hp]
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
neg : f False
⊢ f p

Tactic:
simp only [hp]
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f True

Tactic:
assumption
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f False

Tactic:
assumption
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
⊢ f True ∨ f False

Tactic:
(em p).imp ?_ ?_

Premises used: em, Or.imp
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
refine_1 : p → f True
refine_2 : ¬p → f False
⊢ f True ∨ f False

Tactic:
refine (em p).imp ?_ ?_

Premises used: em, Or.imp
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : p
⊢ f p

Tactic:
h
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : p
h₁ : True ↔ p
⊢ f True

Tactic:
convert! h
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : ¬p
⊢ f p

Tactic:
h
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : ¬p
h₁ : False ↔ p
⊢ f False

Tactic:
convert! h
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : p
⊢ True ↔ p

Tactic:
simp [H]
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h_1 : ∃ (p : Prop), f p
p : Prop
h : f p
H : ¬p
⊢ False ↔ p

Tactic:
simp [H]
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h : f True
⊢ ∃ (p : Prop), f p

Tactic:
⟨_, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h : f True
⊢ ∃ (p : Prop), f p

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h : f False
⊢ ∃ (p : Prop), f p

Tactic:
⟨_, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Logic.Lemmas
Goal:
f : Prop → Prop
h : f False
⊢ ∃ (p : Prop), f p

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
p : Nonempty α → Prop
⊢ (∀ (h : Nonempty α), p h) ↔ ∀ (a : α), p ⋯

Tactic:
Iff.intro (fun h _ ↦ h _) fun h ⟨a⟩ ↦ h a

Premises used: _private.0.Nonempty.forall.match_1, Nonempty.intro, Iff.intro
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
p : Nonempty α → Prop
⊢ (∃ (h : Nonempty α), p h) ↔ ∃ (a : α), p ⋯

Tactic:
Iff.intro (fun ⟨⟨a⟩, h⟩ ↦ ⟨a, h⟩) fun ⟨a, h⟩ ↦ ⟨⟨a⟩, h⟩

Premises used: Exists, _private.0.Nonempty.exists.match_2, _private.0.Nonempty.exists.match_1, Nonempty.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
P : Prop
⊢ (∃ (x : α), P) ↔ Nonempty α ∧ P

Tactic:
Iff.intro (fun ⟨a, h⟩ ↦ ⟨⟨a⟩, h⟩) fun ⟨⟨a⟩, h⟩ ↦ ⟨a, h⟩

Premises used: Exists, Nonempty.intro, And, And.intro, _private.0.exists_const_iff.match_2, Iff.intro, Exists.intro, Nonempty, _private.0.exists_const_iff.match_1
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
⊢ (∃ (x : α), True) ↔ Nonempty α

Tactic:
Iff.intro (fun ⟨a, _⟩ ↦ ⟨a⟩) fun ⟨a⟩ ↦ ⟨a, trivial⟩

Premises used: _private.0.Nonempty.forall.match_1, trivial, Exists, Nonempty.intro, True, Iff.intro, Exists.intro, Nonempty, _private.0.exists_true_iff_nonempty.match_1
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
p : Prop
⊢ Nonempty α → p ↔ ∀ (a : α), p

Tactic:
Nonempty.forall

Premises used: Nonempty.forall
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
⊢ ¬Nonempty α ↔ ∀ (a : α), False

Tactic:
Nonempty.imp

Premises used: Nonempty.imp, Not
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_4
β : α → Sort u_3
⊢ Nonempty (PSigma β) ↔ ∃ (a : α), Nonempty.{u_3} (β a)

Tactic:
Iff.intro (fun ⟨⟨a, c⟩⟩ ↦ ⟨a, ⟨c⟩⟩) fun ⟨a, ⟨c⟩⟩ ↦ ⟨⟨a, c⟩⟩

Premises used: _private.0.nonempty_psigma.match_2, _private.0.nonempty_psigma.match_1, Exists, Nonempty.intro, Iff.intro, Exists.intro, PSigma.mk, Nonempty, PSigma
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
p : α → Prop
⊢ Nonempty.{max 1 u_3} (Subtype p) ↔ ∃ (a : α), p a

Tactic:
Iff.intro (fun ⟨⟨a, h⟩⟩ ↦ ⟨a, h⟩) fun ⟨a, h⟩ ↦ ⟨⟨a, h⟩⟩

Premises used: Exists, Subtype, Nonempty.intro, Subtype.mk, _private.0.nonempty_subtype.match_1, Iff.intro, Exists.intro, Nonempty, _private.0.nonempty_subtype.match_2
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
β : Sort u_4
⊢ Nonempty (α ×' β) ↔ Nonempty α ∧ Nonempty β

Tactic:
Iff.intro (fun ⟨⟨a, b⟩⟩ ↦ ⟨⟨a⟩, ⟨b⟩⟩) fun ⟨⟨a⟩, ⟨b⟩⟩ ↦ ⟨⟨a, b⟩⟩

Premises used: _private.0.nonempty_pprod.match_2, PProd.mk, Nonempty.intro, And, PProd, _private.0.nonempty_pprod.match_1, And.intro, Iff.intro, Nonempty
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
β : Sort u_4
⊢ Nonempty (α ⊕' β) ↔ Nonempty α ∨ Nonempty β

Tactic:
Iff.intro
    (fun ⟨h⟩ ↦
      match h with
      | PSum.inl a => Or.inl ⟨a⟩
      | PSum.inr b => Or.inr ⟨b⟩)
    fun h ↦
    match h with
    | Or.inl ⟨a⟩ => ⟨PSum.inl a⟩
    | Or.inr ⟨b⟩ => ⟨PSum.inr b⟩

Premises used: _private.0.nonempty_psum.match_2, PSum, PSum.inr, _private.0.nonempty_psum.match_1, Nonempty.intro, PSum.inl, Iff.intro, Nonempty, Or.inl, Or, _private.0.nonempty_psum.match_3, Or.inr
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
⊢ Nonempty.{u_3 + 1} (PLift α) ↔ Nonempty α

Tactic:
Iff.intro (fun ⟨⟨a⟩⟩ ↦ ⟨a⟩) fun ⟨a⟩ ↦ ⟨⟨a⟩⟩

Premises used: _private.0.Nonempty.forall.match_1, _private.0.nonempty_plift.match_1, PLift, Nonempty.intro, PLift.up, Iff.intro, Nonempty
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
β : Sort u_4
f : α → β
g : β → α
⊢ Nonempty α ↔ Nonempty β

Tactic:
⟨Nonempty.map f, Nonempty.map g⟩

Premises used: Iff.intro, Nonempty.map
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
h : Nonempty α
p : Prop
f : ∀ (a : Inhabited α), p
⊢ p

Tactic:
h.elim <| f ∘ Inhabited.mk

Premises used: Nonempty.elim, Function.comp, Inhabited.mk
-- Module: Mathlib.Logic.Nonempty
Goal:
ι : Sort u_4
α : ι → Sort u_3
⊢ Nonempty ((i : ι) → α i) ↔ ∀ (i : ι), Nonempty.{u_3} (α i)

Tactic:
⟨fun ⟨f⟩ a ↦ ⟨f a⟩, @Pi.instNonempty _ _⟩

Premises used: Nonempty.intro, _private.0.Classical.nonempty_pi.match_1, Pi.instNonempty, Iff.intro, Nonempty
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_3
h : ¬Nonempty α
⊢ Subsingleton α

Tactic:
⟨fun x ↦ False.elim <| not_nonempty_iff_imp_false.mp h x⟩

Premises used: False.elim, Subsingleton.intro, not_nonempty_iff_imp_false, Iff.mp
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Sort u_1
β : Sort u_2
h : Nonempty β
f : α → β
hf : Surjective f
⊢ Nonempty α

Tactic:
let ⟨y⟩ := h
  let ⟨x, _⟩ := hf y
  ⟨x⟩

Premises used: _private.0.Nonempty.forall.match_1, Nonempty.intro, _private.0.Function.Surjective.nonempty.match_1, Nonempty
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Type u_1
γ : α → Type u_3
⊢ Nonempty ((a : α) × γ a) ↔ ∃ (a : α), Nonempty.{u_3 + 1} (γ a)

Tactic:
Iff.intro (fun ⟨⟨a, c⟩⟩ ↦ ⟨a, ⟨c⟩⟩) fun ⟨a, ⟨c⟩⟩ ↦ ⟨⟨a, c⟩⟩

Premises used: _private.0.nonempty_sigma.match_2, Exists, Nonempty.intro, Iff.intro, Exists.intro, Nonempty, Sigma.mk, _private.0.nonempty_sigma.match_1, Sigma
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Type u_1
β : Type u_2
⊢ Nonempty (α ⊕ β) ↔ Nonempty α ∨ Nonempty β

Tactic:
Iff.intro
    (fun ⟨h⟩ ↦
      match h with
      | Sum.inl a => Or.inl ⟨a⟩
      | Sum.inr b => Or.inr ⟨b⟩)
    fun h ↦
    match h with
    | Or.inl ⟨a⟩ => ⟨Sum.inl a⟩
    | Or.inr ⟨b⟩ => ⟨Sum.inr b⟩

Premises used: _private.0.nonempty_sum.match_2, Sum, Sum.inl, Nonempty.intro, _private.0.nonempty_sum.match_1, Sum.inr, _private.0.nonempty_sum.match_3, Iff.intro, Nonempty, Or.inl, Or, Or.inr
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Type u_1
β : Type u_2
⊢ Nonempty (α × β) ↔ Nonempty α ∧ Nonempty β

Tactic:
Iff.intro (fun ⟨⟨a, b⟩⟩ ↦ ⟨⟨a⟩, ⟨b⟩⟩) fun ⟨⟨a⟩, ⟨b⟩⟩ ↦ ⟨⟨a, b⟩⟩

Premises used: _private.0.nonempty_prod.match_1, Prod.mk, Nonempty.intro, And, And.intro, Iff.intro, Nonempty, Prod, _private.0.nonempty_prod.match_2
-- Module: Mathlib.Logic.Nonempty
Goal:
α : Type u_1
⊢ Nonempty (ULift.{u_4, u_1} α) ↔ Nonempty α

Tactic:
Iff.intro (fun ⟨⟨a⟩⟩ ↦ ⟨a⟩) fun ⟨a⟩ ↦ ⟨⟨a⟩⟩

Premises used: ULift, _private.0.nonempty_ulift.match_2, Nonempty.intro, Iff.intro, Nonempty, ULift.up, _private.0.nonempty_ulift.match_1
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
inst : Preorder α
x y : α
h : x < y
⊢ Nontrivial α

Tactic:
⟨⟨x, y, ne_of_lt h⟩⟩

Premises used: Nontrivial.mk, Exists.intro, ne_of_lt
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
rcases : ∀ (x y : α) (hxy : x ≠ y), ∃ (x : α), ∃ (y : α), x < y
⊢ ∃ (x : α), ∃ (y : α), x < y

Tactic:
rcases exists_pair_ne α with ⟨x, y, hxy⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
x y : α
hxy : x ≠ y
inl : x < y → ∃ (x : α), ∃ (y : α), x < y
inr : y < x → ∃ (x : α), ∃ (y : α), x < y
⊢ ∃ (x : α), ∃ (y : α), x < y

Tactic:
cases lt_or_gt_of_ne hxy

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
x y : α
hxy : x ≠ y
h : x < y
⊢ ∃ (x : α), ∃ (y : α), x < y

Tactic:
⟨_, _, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
x y : α
hxy : x ≠ y
h : x < y
⊢ ∃ (x : α), ∃ (y : α), x < y

Tactic:
exact ⟨_, _, ‹_›⟩
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ (x : α), ∃ (y : α), x < y

Tactic:
⟨_, _, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : LinearOrder α
x y : α
hxy : x ≠ y
h : y < x
⊢ ∃ (x : α), ∃ (y : α), x < y

Tactic:
exact ⟨_, _, ‹_›⟩
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
inst : LinearOrder α
⊢ Nontrivial α ↔ ∃ (x : α), ∃ (y : α), x < y

Tactic:
⟨fun h ↦ @exists_pair_lt α h _, fun ⟨x, y, h⟩ ↦ nontrivial_of_lt x y h⟩

Premises used: Nontrivial, nontrivial_of_lt, _private.0.nontrivial_iff_lt.match_1, Iff.intro, exists_pair_lt
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
p : α → Prop
x : Subtype p
⊢ Nontrivial.{u_1} (Subtype p) ↔ ∃ (y : α), ∃ (x_1 : p y), y ≠ x.val (p := p)

Tactic:
simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne, Subtype.ext_iff]

Premises used: Subtype.exists, Ne, nontrivial_iff_exists_ne, Subtype.ext_iff
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Inhabited α
h : ¬Nontrivial α
x : α
by_contra : ∀ (H : ¬x = default), False
⊢ x = default

Tactic:
by_contra H
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Inhabited α
h : ¬Nontrivial α
x : α
H : ¬x = default
⊢ False

Tactic:
h ⟨_, _, H⟩

Premises used: Nontrivial.mk, Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : Inhabited α
h : ¬Nontrivial α
x : α
H : ¬x = default
⊢ False

Tactic:
exact h ⟨_, _, H⟩

Premises used: Nontrivial.mk, Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inhabit : ∀ (inhabited_h : Inhabited α), Nontrivial.{u_1} (Option α)
⊢ Nontrivial.{u_1} (Option α)

Tactic:
inhabit α
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inhabited_h : Inhabited α
⊢ Nontrivial.{u_1} (Option α)

Tactic:
⟨none, some default, nofun⟩

Premises used: Inhabited.default, False, Option.some, Nontrivial.mk, Option.none, Exists.intro, _private.0.Option.nontrivial.match_1