awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
β : Type v
f : α → α
a : α
l : List β
nil : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a [] = f^[length.{v} (α := β) []] a
cons :
  ∀ (b : β) (l : List β) (H : ∀ (a : α), foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a) (a : α),
    foldl (fun (b : α) (x : β) ↦ f b) a (b :: l) = f^[(b :: l).length] a
⊢ foldl (fun (b : α) (x : β) ↦ f b) a l = f^[l.length] a

Tactic:
induction l generalizing a with
  | nil => rfl
  | cons b l H => rw [length_cons, foldl, iterate_succ_apply, H]

Premises used: List.length_cons, List.foldl, List.cons, Function.iterate_succ_apply, List.nil
-- Module: Mathlib.Logic.Function.Iterate
Goal:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
rw : foldr (fun (x : α) ↦ f) b (a :: l) = f^[l.length + 1] b
rw₁ : f (foldr (fun (x : α) ↦ f) b l) = f^[l.length + 1] b
rw₂ : f (f^[l.length] b) = f^[l.length + 1] b
rw₃ rw₄ : f (f^[l.length] b) = f (f^[l.length] b)
⊢ foldr (fun (x : α) ↦ f) b (a :: l) = f^[(a :: l).length] b

Tactic:
rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']

Premises used: Function.iterate_succ_apply', List.length_cons, List.foldr
-- Module: Mathlib.Logic.Function.Iterate
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n : ℕ
zero : (Pi.map (α := α) (β := α) f)^[0] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[0]
succ :
  ∀ (n : ℕ),
    ((Pi.map (α := α) (β := α) f)^[n] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n]) →
      (Pi.map (α := α) (β := α) f)^[n + 1] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n + 1]
⊢ (Pi.map (α := α) (β := α) f)^[n] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n]

Tactic:
induction n
-- Module: Mathlib.Logic.Function.Iterate
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
⊢ (Pi.map (α := α) (β := α) f)^[0] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[0]

Tactic:
simp [*, map_comp_map]

Premises used: Pi.map_comp_map
-- Module: Mathlib.Logic.Function.Iterate
Goal:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n : ℕ
h : (Pi.map (α := α) (β := α) f)^[n] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n]
⊢ (Pi.map (α := α) (β := α) f)^[n + 1] = Pi.map (α := α) (β := α) fun (i : ι) ↦ (f i)^[n + 1]

Tactic:
simp [*, map_comp_map]

Premises used: Pi.map_comp_map
-- Module: Mathlib.Logic.Function.OfArity
Goal:
α β : Type u
⊢ OfArity α β 0 = β

Tactic:
fromTypes_zero _ _

Premises used: Function.fromTypes_zero
-- Module: Mathlib.Logic.Function.OfArity
Goal:
α β : Type u
n : ℕ
⊢ OfArity α β n.succ = (α → OfArity α β n)

Tactic:
fromTypes_succ _ _

Premises used: Matrix.vecHead, Matrix.vecTail, Function.fromTypes_succ
-- Module: Mathlib.Logic.Function.OfArity
Goal:
α β : Type u
b : β
⊢ const α b 0 = b

Tactic:
FromTypes.const_zero (fun _ => α) b

Premises used: Function.OfArity.const, Function.FromTypes.const_zero
-- Module: Mathlib.Logic.Function.OfArity
Goal:
α β : Type u
b : β
n : ℕ
⊢ Eq (α := OfArity α β n.succ) (const α b n.succ) fun (x : Matrix.vecHead (n := n) fun (x : Fin n.succ) ↦ α) ↦
    const α b n

Tactic:
FromTypes.const_succ (fun _ => α) b

Premises used: Function.OfArity.const, Function.FromTypes.const_succ, Matrix.vecTail
-- Module: Mathlib.Logic.Function.OfArity
Goal:
α β : Type u
b : β
n : ℕ
x : α
⊢ const α b n.succ x = const α b n

Tactic:
FromTypes.const_succ_apply _ b x

Premises used: Function.OfArity.const, Function.FromTypes.const_succ_apply, Matrix.vecTail
-- Module: Mathlib.Logic.Function.OfArity
Goal:
α β : Type u
n : ℕ
⊢ FromTypes (n := n) (fun (x : Fin n) ↦ α) β = OfArity α β n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Function.ULift
Goal:
α : Type u_1
a b : α
h : down.{u_2, u_1} { down := a : ULift.{u_2, u_1} α } = down.{u_2, u_1} { down := b }
⊢ { down := a : ULift.{u_2, u_1} α } = { down := b }

Tactic:
congr
-- Module: Mathlib.Logic.Function.ULift
Goal:
α : Type u_1
a b : ULift.{u_2, u_1} α
h : a = b
rw rw₁ : b.down = b.down
⊢ a.down = b.down

Tactic:
rw [h]
-- Module: Mathlib.Logic.Function.ULift
Goal:
α : Sort u_1
a b : α
h : { down := a : PLift α }.down = { down := b }.down
⊢ { down := a : PLift α } = { down := b }

Tactic:
congr
-- Module: Mathlib.Logic.Function.ULift
Goal:
α : Sort u_1
a b : PLift α
h : a = b
rw rw₁ : b.down = b.down
⊢ a.down = b.down

Tactic:
rw [h]
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
⊢ p ∣ (m - n) * a

Tactic:
simpa [Nat.succ_sub_succ, ← Nat.mul_sub_right_distrib] using
        Nat.dvd_sub hm hn

Premises used: Nat.mul_sub_right_distrib, Nat.dvd_sub, Nat.succ_sub_succ
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
⊢ p ∣ (m - n) * a

Tactic:
have : p ∣ (m - n) * a := by
      simpa [Nat.succ_sub_succ, ← Nat.mul_sub_right_distrib] using
        Nat.dvd_sub hm hn
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
inl : ∀ (hp : p ∣ m - n), p ∣ a
inr : ∀ (hp : p ∣ a), p ∣ a
⊢ p ∣ a

Tactic:
rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)

Premises used: Iff.mp, Nat.Prime.dvd_mul
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ m - n
⊢ p ∣ a

Tactic:
Nat.dvd_trans hp ha

Premises used: Nat.dvd_trans
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ m - n
⊢ p ∣ a

Tactic:
exact Nat.dvd_trans hp ha

Premises used: Nat.dvd_trans
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ a
⊢ p ∣ a

Tactic:
hp
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ a
⊢ p ∣ a

Tactic:
exact hp
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
⊢ p ∣ a

Tactic:
have : p ∣ a := by
      rcases (Nat.Prime.dvd_mul pp).mp this with (hp | hp)
      · exact Nat.dvd_trans hp ha
      · exact hp
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this_1 : p ∣ (m - n) * a
this : p ∣ a
apply : p = 1
⊢ False

Tactic:
apply pp.ne_one

Premises used: Nat.Prime.ne_one
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this_1 : p ∣ (m - n) * a
this : p ∣ a
⊢ p = 1

Tactic:
simpa [Nat.add_sub_cancel_left] using Nat.dvd_sub hn (this.mul_left n)

Premises used: Nat.add_sub_cancel_left, Dvd.dvd.mul_left, Nat.dvd_sub
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
a : Fin m → ℕ
i : Fin m
⊢ Membership.mem (γ := Finset (Fin m)) Finset.univ i

Tactic:
simp
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
a : Fin m → ℕ
i : Fin m
⊢ a i < supOfSeq a

Tactic:
have h₁ : a i < supOfSeq a :=
    Nat.lt_add_one_iff.mpr (le_max_of_le_right <| Finset.le_sup (by simp))
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < supOfSeq a
⊢ supOfSeq a ≤ ((↑i : ℕ) + 1) * (supOfSeq a)! + 1

Tactic:
have h₂ : supOfSeq a ≤ (i + 1) * (supOfSeq a)! + 1 :=
    le_trans (self_le_factorial _) (le_trans (Nat.le_mul_of_pos_left (supOfSeq a)! (succ_pos i))
      (le_add_right _ _))
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < supOfSeq a
h₂ : supOfSeq a ≤ ((↑i : ℕ) + 1) * (supOfSeq a)! + 1
⊢ a i < coprimes a i

Tactic:
simpa only [coprimes] using lt_of_lt_of_le h₁ h₂

Premises used: lt_of_lt_of_le, _private.0.Nat.coprimes
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
inr :
  ∀ (this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄ (hij : i ≠ j) (ltij : i < j), (Coprime on coprimes a) i j)
    (ltij : j ≤ i), (Coprime on coprimes a) i j
wlog! : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄ (hij : i ≠ j) (ltij : i < j), (Coprime on coprimes a) i j
⊢ (Coprime on coprimes a) i j

Tactic:
wlog! ltij : i < j
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄ (hij : i ≠ j) (ltij : i < j), (Coprime on coprimes a) i j
ltij : j ≤ i
⊢ (Coprime on coprimes a) i j

Tactic:
(this a hij.symm (lt_of_le_of_ne ltij hij.symm)).symm

Premises used: Nat.Coprime.symm, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄ (hij : i ≠ j) (ltij : i < j), (Coprime on coprimes a) i j
ltij : j ≤ i
⊢ (Coprime on coprimes a) i j

Tactic:
exact (this a hij.symm (lt_of_le_of_ne ltij hij.symm)).symm

Premises used: Nat.Coprime.symm, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m_1 m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ (↑j : ℕ) < supOfSeq a

Tactic:
have hja : j < supOfSeq a := lt_of_lt_of_le j.prop (le_succ_of_le (le_max_left _ _))
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m_1 m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : (↑j : ℕ) < supOfSeq a
⊢ 0 < (↑j : ℕ) + 1 - ((↑i : ℕ) + 1)

Tactic:
lia
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m_1 m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : (↑j : ℕ) < supOfSeq a
⊢ (↑j : ℕ) + 1 - ((↑i : ℕ) + 1) ≤ supOfSeq a

Tactic:
simpa only [Nat.succ_sub_succ] using le_of_lt (lt_of_le_of_lt (sub_le j i) hja)

Premises used: lt_of_le_of_lt, le_of_lt, Nat.sub_le, Fin.val, Nat.succ_sub_succ
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m_1 m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : (↑j : ℕ) < supOfSeq a
⊢ (((↑i : ℕ) + 1) * (supOfSeq a)! + 1).Coprime (((↑j : ℕ) + 1) * (supOfSeq a)! + 1)

Tactic:
exact coprime_mul_succ
    (Nat.dvd_factorial (by lia)
      (by simpa only [Nat.succ_sub_succ] using le_of_lt (lt_of_le_of_lt (sub_le j i) hja)))

Premises used: Nat.dvd_factorial, Nat.coprime_mul_succ
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
l : List ℕ
⊢ ∀ (i : Fin l.length),
    Membership.mem (γ := Finset (Fin l.length)) Finset.univ i →
      coprimes
          (fun (x : Fin l.length) ↦
            getElem (valid := fun (xs : List ℕ) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l x ⋯)
          i ≠
        0

Tactic:
simp [coprimes]

Premises used: _private.0.Nat.coprimes
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
m : ℕ
l : List ℕ
⊢ (↑Finset.univ : Set (Fin l.length)).Pairwise
    (Function.onFun Coprime
      (coprimes fun (x : Fin l.length) ↦
        getElem (valid := fun (xs : List ℕ) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l x ⋯))

Tactic:
simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _)

Premises used: Iff.mpr, Set.pairwise_univ, _private.0.Nat.pairwise_coprime_coprimes
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
l : List ℕ
i : Fin l.length
⊢ ∀ (i : Fin l.length),
    Membership.mem (γ := Finset (Fin l.length)) Finset.univ i →
      coprimes
          (fun (x : Fin l.length) ↦
            getElem (valid := fun (xs : List ℕ) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l x ⋯)
          i ≠
        0

Tactic:
simp [coprimes]

Premises used: _private.0.Nat.coprimes
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
l : List ℕ
i : Fin l.length
⊢ (↑Finset.univ : Set (Fin l.length)).Pairwise
    (Function.onFun Coprime
      (coprimes fun (x : Fin l.length) ↦
        getElem (valid := fun (xs : List ℕ) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l x ⋯))

Tactic:
simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _)

Premises used: Iff.mpr, Set.pairwise_univ, _private.0.Nat.pairwise_coprime_coprimes
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
l : List ℕ
i : Fin l.length
⊢ Membership.mem (γ := Finset (Fin l.length)) Finset.univ i

Tactic:
simp
-- Module: Mathlib.Logic.Godel.GodelBetaFunction
Goal:
l : List ℕ
i : Fin l.length
⊢ (unbeta l).beta (↑i : ℕ) = getElem (valid := fun (xs : List ℕ) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯

Tactic:
simpa [beta, unbeta, coprimes] using mod_eq_of_modEq
    ((chineseRemainderOfFinset (l[·]) (coprimes (l[·])) Finset.univ
      (by simp [coprimes])
      (by simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _))).prop i (by simp))
    (coprimes_lt _ _)

Premises used: Finset.univ, Nat.beta, Nat.mod_eq_of_modEq, Nat.unbeta, GetElem.getElem, Subtype.prop, Nat.chineseRemainderOfFinset, _private.0.Nat.coprimes
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
⊢ ¬Nonempty α ↔ IsEmpty α

Tactic:
⟨fun h ↦ ⟨fun x ↦ h ⟨x⟩⟩, fun h1 h2 ↦ h2.elim h1.elim⟩

Premises used: Nonempty.elim, IsEmpty.elim, Nonempty.intro, IsEmpty.mk, Iff.intro
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
⊢ ¬IsEmpty α ↔ Nonempty α

Tactic:
not_iff_comm.mp not_nonempty_iff

Premises used: not_nonempty_iff, Iff.mp, not_iff_comm
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
p : Prop
⊢ IsEmpty p ↔ ¬p

Tactic:
simp only [← not_nonempty_iff, nonempty_prop]

Premises used: not_nonempty_iff, nonempty_prop
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
π : α → Sort u_4
⊢ IsEmpty ((a : α) → π a) ↔ ∃ (a : α), IsEmpty.{u_4} (π a)

Tactic:
simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]

Premises used: not_nonempty_iff, Classical.nonempty_pi, Classical.not_forall
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
β : Sort u_2
rw : (∃ (a : α), IsEmpty β) ↔ Nonempty α ∧ IsEmpty β
rw₁ : (∃ (a : α), IsEmpty β) ↔ (∃ (x : α), True) ∧ IsEmpty β
rw₂ : (∃ (a : α), IsEmpty β) ↔ ∃ (x : α), True ∧ IsEmpty β
rw₃ rw₄ : (∃ (a : α), IsEmpty β) ↔ ∃ (x : α), IsEmpty β
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

Tactic:
rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]

Premises used: exists_true_iff_nonempty, exists_and_right, isEmpty_pi, true_and
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
β : Sort u_2
rw : ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
rw₁ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
rw₂ : IsEmpty (α → β) ↔ ¬IsEmpty α ∧ IsEmpty β
rw₃ : Nonempty α ∧ IsEmpty β ↔ ¬IsEmpty α ∧ IsEmpty β
rw₄ rw₅ : Nonempty α ∧ IsEmpty β ↔ Nonempty α ∧ IsEmpty β
⊢ ¬Nonempty (α → β) ↔ ¬(IsEmpty α ∨ Nonempty β)

Tactic:
rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]

Premises used: not_or, not_nonempty_iff, not_isEmpty_iff, isEmpty_fun
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_5
E : α → Type u_4
⊢ IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty.{u_4 + 1} (E a)

Tactic:
simp only [← not_nonempty_iff, nonempty_sigma, not_exists]

Premises used: not_exists, not_nonempty_iff, nonempty_sigma
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_5
E : α → Sort u_4
⊢ IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty.{u_4} (E a)

Tactic:
simp only [← not_nonempty_iff, nonempty_psigma, not_exists]

Premises used: not_exists, not_nonempty_iff, nonempty_psigma
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
p : α → Prop
⊢ IsEmpty.{max 1 u_1} (Subtype p) ↔ ∀ (x : α), ¬p x

Tactic:
simp only [← not_nonempty_iff, nonempty_subtype, not_exists]

Premises used: not_exists, not_nonempty_iff, nonempty_subtype
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
⊢ IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_prod, not_and_or]

Premises used: nonempty_prod, not_nonempty_iff, not_and_or
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_pprod, not_and_or]

Premises used: not_nonempty_iff, nonempty_pprod, not_and_or
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_sum, not_or]

Premises used: not_or, not_nonempty_iff, nonempty_sum
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_4
β : Sort u_5
⊢ IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_psum, not_or]

Premises used: nonempty_psum, not_or, not_nonempty_iff
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
⊢ IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α

Tactic:
simp only [← not_nonempty_iff, nonempty_ulift]

Premises used: nonempty_ulift, not_nonempty_iff
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_4
⊢ IsEmpty.{u_4 + 1} (PLift α) ↔ IsEmpty α

Tactic:
simp only [← not_nonempty_iff, nonempty_plift]

Premises used: nonempty_plift, not_nonempty_iff
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_4
inst : IsEmpty α
r : α → α → Prop
⊢ WellFounded r

Tactic:
⟨isEmptyElim⟩

Premises used: isEmptyElim, WellFounded.intro
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
⊢ IsEmpty α ∨ Nonempty α

Tactic:
(em <| IsEmpty α).elim Or.inl <| Or.inr ∘ not_isEmpty_iff.mp

Premises used: Function.comp, em, IsEmpty, not_isEmpty_iff, Iff.mp, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
h : Nonempty α
⊢ ¬IsEmpty α

Tactic:
not_isEmpty_iff.mpr h

Premises used: Iff.mpr, not_isEmpty_iff
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
inst : IsEmpty α
f : α → β
g : α → γ
h : β → γ
⊢ extend f g h = h

Tactic:
funext fun _ ↦ (Function.extend_apply' _ _ _) fun ⟨a, _⟩ ↦ isEmptyElim a

Premises used: False, isEmptyElim, funext, Function.extend_apply', _private.0.Function.extend_of_isEmpty.match_1
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst : IsEmpty α
⊢ LeftTotal R

Tactic:
simp only [LeftTotal, IsEmpty.forall_iff]

Premises used: Relator.LeftTotal, IsEmpty.forall_iff
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst : IsEmpty β
⊢ LeftTotal R ↔ IsEmpty α

Tactic:
simp only [LeftTotal, IsEmpty.exists_iff, isEmpty_iff]

Premises used: Relator.LeftTotal, isEmpty_iff, IsEmpty.exists_iff
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst : IsEmpty β
⊢ RightTotal R

Tactic:
simp only [RightTotal, IsEmpty.forall_iff]

Premises used: Relator.RightTotal, IsEmpty.forall_iff
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst : IsEmpty α
⊢ RightTotal R ↔ IsEmpty β

Tactic:
simp only [RightTotal, IsEmpty.exists_iff, isEmpty_iff]

Premises used: isEmpty_iff, IsEmpty.exists_iff, Relator.RightTotal
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst : IsEmpty α
inst_1 : IsEmpty β
⊢ BiTotal R

Tactic:
⟨leftTotal_empty R, rightTotal_empty R⟩

Premises used: rightTotal_empty, leftTotal_empty, And.intro, Relator.BiTotal
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst : IsEmpty α
⊢ BiTotal R ↔ IsEmpty β

Tactic:
simp only [BiTotal, leftTotal_empty, rightTotal_iff_isEmpty_right, true_and]

Premises used: rightTotal_iff_isEmpty_right, leftTotal_empty, Relator.BiTotal, true_and
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst : IsEmpty β
⊢ BiTotal R ↔ IsEmpty α

Tactic:
simp only [BiTotal, leftTotal_iff_isEmpty_left, rightTotal_empty, and_true]

Premises used: and_true, rightTotal_empty, leftTotal_iff_isEmpty_left, Relator.BiTotal
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
inst : IsEmpty β
f : α → β
⊢ Surjective f

Tactic:
IsEmpty.elim ‹_›

Premises used: IsEmpty.elim, Function.Surjective
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
inst : IsEmpty α
f : α → β
⊢ Surjective f ↔ IsEmpty β

Tactic:
⟨Surjective.isEmpty, fun _ ↦ .of_isEmpty f⟩

Premises used: Function.Surjective.of_isEmpty, Iff.intro, Function.Surjective.isEmpty
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
f : α → β
inst : IsEmpty β
⊢ Bijective f

Tactic:
have := f.isEmpty
  ⟨injective_of_subsingleton f, .of_isEmpty f⟩

Premises used: Function.isEmpty, Function.injective_of_subsingleton, Function.Surjective.of_isEmpty, And.intro, Function.Bijective
-- Module: Mathlib.Logic.IsEmpty.Basic
Goal:
α : Type u_4
β : Type u_5
inst : IsEmpty α
inst_1 : Nonempty β
f : α → β
⊢ ¬Surjective f

Tactic:
(not_isEmpty_of_nonempty β ·.isEmpty)

Premises used: not_isEmpty_of_nonempty, Not, Function.Surjective.isEmpty
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
⊢ IsEmpty Empty

Tactic:
⟨Empty.elim⟩

Premises used: Empty.elim, IsEmpty.mk
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
⊢ IsEmpty PEmpty

Tactic:
⟨PEmpty.elim⟩

Premises used: PEmpty.elim, IsEmpty.mk
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
⊢ IsEmpty False

Tactic:
⟨id⟩

Premises used: id, IsEmpty.mk
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
⊢ IsEmpty (Fin 0)

Tactic:
⟨fun n ↦ Nat.not_lt_zero n.1 n.2⟩

Premises used: Fin.isLt, Fin.val, IsEmpty.mk, Nat.not_lt_zero
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
⊢ IsEmpty (Fin Nat.zero)

Tactic:
Fin.isEmpty

Premises used: Fin.isEmpty
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty β
f : α → β
⊢ IsEmpty α

Tactic:
⟨fun x ↦ IsEmpty.false (f x)⟩

Premises used: IsEmpty.mk, IsEmpty.false
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty α
f : α → β
hf : Surjective f
⊢ IsEmpty β

Tactic:
⟨fun y ↦ let ⟨x, _⟩ := hf y; IsEmpty.false x⟩

Premises used: False, _private.0.Function.Surjective.isEmpty.match_1, IsEmpty.mk, IsEmpty.false
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
p : α → Sort v
inst : ∀ (x : α), IsEmpty.{v} (p x)
h : Nonempty α
⊢ IsEmpty ((x : α) → p x)

Tactic:
h.elim fun x ↦ Function.isEmpty fun f ↦ f x

Premises used: Function.isEmpty, Nonempty.elim
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty α
⊢ IsEmpty (α ×' β)

Tactic:
Function.isEmpty PProd.fst

Premises used: Function.isEmpty, PProd.fst
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty β
⊢ IsEmpty (α ×' β)

Tactic:
Function.isEmpty PProd.snd

Premises used: Function.isEmpty, PProd.snd
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α_1 : Sort u
β_1 : Sort v
α : Type u_1
β : Type u_2
inst : IsEmpty α
⊢ IsEmpty (α × β)

Tactic:
Function.isEmpty Prod.fst

Premises used: Function.isEmpty, Prod.fst
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α_1 : Sort u
β_1 : Sort v
α : Type u_1
β : Type u_2
inst : IsEmpty β
⊢ IsEmpty (α × β)

Tactic:
Function.isEmpty Prod.snd

Premises used: Function.isEmpty, Prod.snd
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty α
r : α → α → Prop
⊢ IsEmpty.{u} (Quot r)

Tactic:
Function.Surjective.isEmpty Quot.exists_rep

Premises used: Quot.exists_rep, Function.Surjective.isEmpty
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty α
s : Setoid α
⊢ IsEmpty.{u} (Quotient s)

Tactic:
Quot.instIsEmpty

Premises used: Quot.instIsEmpty, Quotient
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty α
inst_1 : IsEmpty β
⊢ IsEmpty (α ⊕' β)

Tactic:
⟨fun x ↦ PSum.rec IsEmpty.false IsEmpty.false x⟩

Premises used: PSum.rec, IsEmpty.mk
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α_1 : Sort u
β_1 : Sort v
α : Type u_1
β : Type u_2
inst : IsEmpty α
inst_1 : IsEmpty β
⊢ IsEmpty (α ⊕ β)

Tactic:
⟨fun x ↦ Sum.rec IsEmpty.false IsEmpty.false x⟩

Premises used: IsEmpty.mk, Sum.rec
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
β : Sort v
inst : IsEmpty α
p : α → Prop
⊢ IsEmpty.{max 1 u} (Subtype p)

Tactic:
⟨fun x ↦ IsEmpty.false x.1⟩

Premises used: IsEmpty.mk, IsEmpty.false, Subtype.val
-- Module: Mathlib.Logic.IsEmpty.Defs
Goal:
α : Sort u
p : α → Prop
hp : ∀ (a : α), ¬p a
⊢ IsEmpty.{max 1 u} (Subtype p)

Tactic:
⟨fun x ↦ hp _ x.2⟩

Premises used: IsEmpty.mk, Subtype.val, Subtype.property