awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := inf' univ ⋯ v
w' : (i : Fin (n + 1)) → ℕ := fun (i : Fin (n + 1)) ↦ (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), (↑(w' i) : ℤ) = v i - m
h :
  (vandermonde v).det =
    det (n := Fin (n + 1))
      ((of : (a : Fin (n + 1) → Fin (n + 1) → ℤ) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ) fun (i j : Fin (n + 1)) ↦
        eval ((fun (i : Fin (n + 1)) ↦ ((↑(w' i) : ℤ) : ℤ)) i)
          ((fun (i : Fin (n + 1)) ↦ (descPochhammer ℤ (↑i : ℕ) : ℤ[X])) j))
h₁ :
  (vandermonde v).det =
    HMul.hMul (α := ℤ) (↑n.superFactorial : ℤ)
      (det (n := Fin (n + 1))
        ((of : (a : Fin (n + 1) → Fin (n + 1) → ℤ) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ) fun (i j : Fin (n + 1)) ↦
          (↑((w' i).choose (↑j : ℕ)) : ℤ)))
⊢ (↑n.superFactorial : ℤ) ∣ (vandermonde v).det

Tactic:
use (of (fun (i j : Fin (n + 1)) => (Nat.choose (w' i) (j : ℕ) : ℤ))).det

Premises used: Nat.choose, Matrix.of, Fin.val, Nat.cast, DFunLike.coe, Matrix.det
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
n : ℕ
v : Fin (n + 1) → ℤ
m : ℤ := inf' univ ⋯ v
w' : (i : Fin (n + 1)) → ℕ := fun (i : Fin (n + 1)) ↦ (v i - m).toNat
hw' : ∀ (i : Fin (n + 1)), (↑(w' i) : ℤ) = v i - m
h :
  (vandermonde v).det =
    det (n := Fin (n + 1))
      ((of : (a : Fin (n + 1) → Fin (n + 1) → ℤ) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ) fun (i j : Fin (n + 1)) ↦
        eval ((fun (i : Fin (n + 1)) ↦ ((↑(w' i) : ℤ) : ℤ)) i)
          ((fun (i : Fin (n + 1)) ↦ (descPochhammer ℤ (↑i : ℕ) : ℤ[X])) j))
⊢ (vandermonde v).det =
    HMul.hMul (α := ℤ) (↑n.superFactorial : ℤ)
      (det (n := Fin (n + 1))
        ((of : (a : Fin (n + 1) → Fin (n + 1) → ℤ) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ) fun (i j : Fin (n + 1)) ↦
          (↑((w' i).choose (↑j : ℕ)) : ℤ)))

Tactic:
simp [h, of_eval_descPochhammer_eq_mul_of_choose w', Fin.prod_univ_eq_prod_range]

Premises used: Fin.prod_univ_eq_prod_range, _private.0.Matrix.of_eval_descPochhammer_eq_mul_of_choose
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b : α
rw rw₁ : (b = a) = (b = a)
⊢ (a = b) = (b = a)

Tactic:
rw [@eq_comm _ a b]

Premises used: eq_comm
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
rw rw₁ : (b ↔ a) = (b ↔ a)
⊢ (a ↔ b) = (b ↔ a)

Tactic:
rw [@iff_comm a b]

Premises used: iff_comm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
inst : Subsingleton α
p : α → Prop
x_1 x_2 : Subtype p
x : α
property : p x
y : α
property_1 : p y
refl : ∀ (property_2 : p x), Eq.{max 1 u_1} (Subtype.mk (p := p) x property) (Subtype.mk (p := p) x property_2)
⊢ Eq.{max 1 u_1} (Subtype.mk (p := p) x property) (Subtype.mk (p := p) y property_1)

Tactic:
cases Subsingleton.elim x y

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
inst : Subsingleton α
p : α → Prop
x_1 x_2 : Subtype p
x : α
property property_1 : p x
⊢ Eq.{max 1 u_1} (Subtype.mk (p := p) x property) (Subtype.mk (p := p) x property_1)

Tactic:
rfl
-- Module: Mathlib.Logic.Basic
Goal:
α β : Sort u_2
γ : Sort u_3
f : α → γ
g : β → γ
x : α
y : β
h₁ : f ≍ g
h₂ : x ≍ y
refl : ∀ {g : α → γ} (h₁ : f ≍ g), f x = g x
⊢ f x = g y

Tactic:
cases h₂
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : f ≍ g
refl : f x = f x
⊢ f x = g x

Tactic:
cases h₁
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
⊢ f x = f x

Tactic:
rfl
-- Module: Mathlib.Logic.Basic
Goal:
α₁ α₂ : Sort u
β₁ : α₁ → Sort v
β₂ : α₂ → Sort v
f₁ : (a : α₁) → β₁ a
f₂ : (a : α₂) → β₂ a
a₁ : α₁
a₂ : α₂
hargs : a₁ ≍ a₂
ht : ∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂
refl :
  ∀ {β₂ : α₁ → Sort v} {f₂ : (a : α₁) → β₂ a} (ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂)
    (hf : α₁ = α₁ → β₁ ≍ β₂ → f₁ ≍ f₂), f₁ a₁ ≍ f₂ a₁
⊢ f₁ a₁ ≍ f₂ a₂

Tactic:
cases hargs
-- Module: Mathlib.Logic.Basic
Goal:
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
β₂ : α₁ → Sort v
f₂ : (a : α₁) → β₂ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₁ → β₁ ≍ β₂ → f₁ ≍ f₂
refl :
  ∀ {f₂ : (a : α₁) → β₁ a} (ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂) (hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₂),
    f₁ a₁ ≍ f₂ a₁
⊢ f₁ a₁ ≍ f₂ a₁

Tactic:
cases funext fun v => ht v v .rfl

Premises used: HEq.rfl, funext
-- Module: Mathlib.Logic.Basic
Goal:
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
f₂ : (a : α₁) → β₁ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂
hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₂
refl : ∀ (hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₁), f₁ a₁ ≍ f₁ a₁
⊢ f₁ a₁ ≍ f₂ a₁

Tactic:
cases hf rfl .rfl

Premises used: HEq.rfl, rfl
-- Module: Mathlib.Logic.Basic
Goal:
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂
hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₁
⊢ f₁ a₁ ≍ f₁ a₁

Tactic:
rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
rw rw₁ : b = b
⊢ b = c

Tactic:
rw [← h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
b c : α
h : b = c
a : α
rw rw₁ : a = c ↔ a = c
⊢ a = b ↔ a = c

Tactic:
rw [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
rw rw₁ : b = b
⊢ a = b

Tactic:
rw [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a_1 b : α
h : a_1 = b
a : α
rw rw₁ : b = a ↔ b = a
⊢ a_1 = a ↔ b = a

Tactic:
rw [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b c : α
h : b ≠ c
⊢ a ≠ b ∧ a = c ↔ a = c

Tactic:
and_iff_right_of_imp (fun h2 => h2.symm ▸ h.symm)

Premises used: Eq.rec, Ne.symm, Eq.symm, and_iff_right_of_imp
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
h : Fact p
⊢ p

Tactic:
h.1

Premises used: Fact.out
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
⊢ Fact p ↔ p

Tactic:
⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩

Premises used: Fact.mk, Iff.intro, Fact.out
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (a → b) → ¬b → ¬a

Tactic:
mt

Premises used: mt
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
inst : Decidable p
⊢ ¬p ∨ p

Tactic:
(dec_em p).symm

Premises used: Or.symm, dec_em
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
⊢ ¬p ∨ p

Tactic:
(em p).symm

Premises used: em, Or.symm
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
⊢ p ∨ ¬p

Tactic:
em _

Premises used: em
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
x y : α
inst : Decidable (x = y)
⊢ x = y ∨ x ≠ y

Tactic:
dec_em <| x = y

Premises used: Eq, dec_em
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
x y : α
inst : Decidable (x = y)
⊢ x ≠ y ∨ x = y

Tactic:
dec_em' <| x = y

Premises used: dec_em', Eq
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
x y : α
⊢ x = y ∨ x ≠ y

Tactic:
em <| x = y

Premises used: em, Eq
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
x y : α
⊢ x ≠ y ∨ x = y

Tactic:
em' <| x = y

Premises used: Eq, em'
-- Module: Mathlib.Logic.Basic
Goal:
p : Prop
⊢ (¬p → False) → p

Tactic:
open scoped Classical in Decidable.byContradiction

Premises used: Decidable.byContradiction
-- Module: Mathlib.Logic.Basic
Goal:
p q : Prop
hpq : p → q
hnpq : ¬p → q
⊢ q

Tactic:
open scoped Classical in if hp : p then hpq hp else hnpq hp

Premises used: dite
-- Module: Mathlib.Logic.Basic
Goal:
a : Prop
⊢ ¬¬a → a

Tactic:
by_contra

Premises used: by_contra, Not
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b : α
⊢ ¬a ≠ b ↔ a = b

Tactic:
not_not

Premises used: Classical.not_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ ¬(a → b) → a

Tactic:
open scoped Classical in Decidable.of_not_imp

Premises used: Decidable.of_not_imp
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (¬a → b) → ¬b → a

Tactic:
open scoped Classical in Not.decidable_imp_symm

Premises used: Not.decidable_imp_symm
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ ¬a → b ↔ ¬b → a

Tactic:
open scoped Classical in Decidable.not_imp_comm

Premises used: Decidable.not_imp_comm
-- Module: Mathlib.Logic.Basic
Goal:
a : Prop
⊢ ¬a → a ↔ a

Tactic:
open scoped Classical in Decidable.not_imp_self

Premises used: Decidable.not_imp_self
-- Module: Mathlib.Logic.Basic
Goal:
a : Sort u_1
b : Sort u_2
c : Prop
⊢ (∀ (a : a) (a : b), c) ↔ ∀ (a_1 : b) (a : a), c

Tactic:
⟨fun h x y ↦ h y x, fun h x y ↦ h y x⟩

Premises used: Iff.intro
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
h : a ↔ ¬b
⊢ ¬a ↔ b

Tactic:
h.not.trans not_not

Premises used: Classical.not_not, Iff.not, Iff.trans
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
h : ¬a ↔ b
⊢ a ↔ ¬b

Tactic:
not_not.symm.trans h.not

Premises used: Classical.not_not, Iff.not, Iff.trans, Iff.symm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
a b : α
c d : β
⊢ (a = b ↔ c = d) → (a ≠ b ↔ c ≠ d)

Tactic:
Iff.not

Premises used: Iff.not
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
a b : α
c d : β
⊢ (a = b ↔ c ≠ d) → (a ≠ b ↔ c = d)

Tactic:
Iff.not_left

Premises used: Iff.not_left
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
a b : α
c d : β
⊢ (a ≠ b ↔ c = d) → (a = b ↔ c ≠ d)

Tactic:
Iff.not_right

Premises used: Iff.not_right
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Xor a b ↔ a ∧ ¬b ∨ b ∧ ¬a

Tactic:
Iff.rfl

Premises used: Iff.rfl, Xor
-- Module: Mathlib.Logic.Basic
Goal:
⊢ Xor True = Not

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
⊢ Xor False = id

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Xor a b = Xor b a

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Std.Commutative Xor

Tactic:
⟨xor_comm⟩

Premises used: xor_comm, Std.Commutative.mk
-- Module: Mathlib.Logic.Basic
Goal:
a : Prop
⊢ Xor a a = False

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Xor (¬a) b ↔ (a ↔ b)

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Xor a ¬b ↔ (a ↔ b)

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Xor (¬a) ¬b ↔ Xor a b

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
h : Xor a b
⊢ a ∨ b

Tactic:
grind
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b : α
p : Prop
⊢ p ∧ a = b ↔ p ∧ b = a

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b : α
p : Prop
⊢ a = b ∧ p ↔ b = a ∧ p

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Logic.Basic
Goal:
a b c d : Prop
h : a ∨ b ∨ c
ha : a → d
hb : b → d
hc : c → d
⊢ d

Tactic:
Or.elim h ha fun h₂ ↦ Or.elim h₂ hb hc

Premises used: Or.elim
-- Module: Mathlib.Logic.Basic
Goal:
a b d e c f : Prop
had : a → d
hbe : b → e
hcf : c → f
⊢ a ∨ b ∨ c → d ∨ e ∨ f

Tactic:
Or.imp had <| Or.imp hbe hcf

Premises used: Or.imp
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (a → b) → ¬a ∨ b

Tactic:
open scoped Classical in Decidable.not_or_of_imp

Premises used: Decidable.not_or_of_imp
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
inst : Decidable a
h : a → b
⊢ b ∨ ¬a

Tactic:
dite _ (Or.inl ∘ h) Or.inr

Premises used: Function.comp, dite, Or.inl, Or.inr
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (a → b) → b ∨ ¬a

Tactic:
open scoped Classical in Decidable.or_not_of_imp

Premises used: Decidable.or_not_of_imp
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ a → b ↔ ¬a ∨ b

Tactic:
open scoped Classical in Decidable.imp_iff_not_or

Premises used: Decidable.imp_iff_not_or
-- Module: Mathlib.Logic.Basic
Goal:
b a : Prop
⊢ b → a ↔ a ∨ ¬b

Tactic:
open scoped Classical in Decidable.imp_iff_or_not

Premises used: Decidable.imp_iff_or_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ ¬a → ¬b ↔ b → a

Tactic:
open scoped Classical in Decidable.not_imp_not

Premises used: Decidable.not_imp_not
-- Module: Mathlib.Logic.Basic
Goal:
p q : Prop
⊢ (p → q) ∧ (¬p → q) ↔ q

Tactic:
Classical.imp_and_neg_imp_iff p

Premises used: Classical.imp_and_neg_imp_iff
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (¬a → ¬b) → b → a

Tactic:
not_imp_not.mp

Premises used: Iff.mp, not_imp_not
-- Module: Mathlib.Logic.Basic
Goal:
c a b : Prop
h : ¬c → (a ↔ b)
⊢ a ∨ c ↔ b ∨ c

Tactic:
open scoped Classical in Decidable.or_congr_left' h

Premises used: Decidable.or_congr_left'
-- Module: Mathlib.Logic.Basic
Goal:
a b c : Prop
h : ¬a → (b ↔ c)
⊢ a ∨ b ↔ a ∨ c

Tactic:
open scoped Classical in Decidable.or_congr_right' h

Premises used: Decidable.or_congr_right'
-- Module: Mathlib.Logic.Basic
Goal:
P : Prop
h : P
⊢ ⋯ = h

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Basic
Goal:
a b c : Prop
⊢ a → b ∨ c ↔ (a → b) ∨ (a → c)

Tactic:
open scoped Classical in Decidable.imp_or

Premises used: Decidable.imp_or
-- Module: Mathlib.Logic.Basic
Goal:
a : Sort u_1
b c : Prop
⊢ (∀ (a : a), b ∨ c) ↔ (∀ (a : a), b) ∨ ∀ (a : a), c

Tactic:
open scoped Classical in Decidable.imp_or'

Premises used: Decidable.imp_or'
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ ((a → b) → a) → a

Tactic:
open scoped Classical in Decidable.peirce _ _

Premises used: Decidable.peirce
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (¬a ↔ ¬b) ↔ (a ↔ b)

Tactic:
open scoped Classical in Decidable.not_iff_not

Premises used: Decidable.not_iff_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (¬a ↔ b) ↔ (¬b ↔ a)

Tactic:
open scoped Classical in Decidable.not_iff_comm

Premises used: Decidable.not_iff_comm
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ ¬(a ↔ b) ↔ (¬a ↔ b)

Tactic:
open scoped Classical in Decidable.not_iff

Premises used: Decidable.not_iff
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (a ↔ ¬b) ↔ (b ↔ ¬a)

Tactic:
open scoped Classical in Decidable.iff_not_comm

Premises used: Decidable.iff_not_comm
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b

Tactic:
open scoped Classical in Decidable.iff_iff_and_or_not_and_not

Premises used: Decidable.iff_iff_and_or_not_and_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

Tactic:
open scoped Classical in Decidable.iff_iff_not_or_and_or_not

Premises used: Decidable.iff_iff_not_or_and_or_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ ¬(a ∧ ¬b) ↔ a → b

Tactic:
open scoped Classical in Decidable.not_and_not_right

Premises used: Decidable.not_and_not_right
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ ¬(a ∧ b) ↔ ¬a ∨ ¬b

Tactic:
open scoped Classical in Decidable.not_and_iff_not_or_not

Premises used: Decidable.not_and_iff_not_or_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ a ∨ b ↔ ¬(¬a ∧ ¬b)

Tactic:
open scoped Classical in Decidable.or_iff_not_not_and_not

Premises used: Decidable.or_iff_not_not_and_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ a ∧ b ↔ ¬(¬a ∨ ¬b)

Tactic:
open scoped Classical in Decidable.and_iff_not_not_or_not

Premises used: Decidable.and_iff_not_not_or_not
-- Module: Mathlib.Logic.Basic
Goal:
P Q : Prop
⊢ ¬Xor P Q ↔ (P ↔ Q)

Tactic:
simp only [not_and, Xor, not_or, not_not, ← iff_iff_implies_and_implies]

Premises used: Classical.not_not, Xor, iff_iff_implies_and_implies, not_or, not_and
-- Module: Mathlib.Logic.Basic
Goal:
P Q : Prop
⊢ Xor P Q ↔ ¬(P ↔ Q)

Tactic:
(not_xor P Q).not_right

Premises used: not_xor, Iff.not_right
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Xor a b ↔ (a ↔ ¬b)

Tactic:
simp only [← @xor_not_right a, not_not]

Premises used: xor_not_right, Classical.not_not
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
⊢ Xor a b ↔ (¬a ↔ b)

Tactic:
simp only [← @xor_not_left _ b, not_not]

Premises used: Classical.not_not, xor_not_left
-- Module: Mathlib.Logic.Basic
Goal:
a b : Prop
rw : a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∨ b) ∧ ¬(a ∧ b)
rw₁ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬(a ∧ b) ∨ b ∧ ¬(a ∧ b)
rw₂ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ (¬a ∨ ¬b) ∨ b ∧ (¬a ∨ ¬b)
rw₃ : a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∧ ¬a ∨ a ∧ ¬b) ∨ b ∧ (¬a ∨ ¬b)
rw₄ : a ∧ ¬b ∨ b ∧ ¬a ↔ (False ∨ a ∧ ¬b) ∨ b ∧ (¬a ∨ ¬b)
rw₅ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ (¬a ∨ ¬b)
rw₆ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ b ∧ ¬b
rw₇ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ False
rw₈ rw₉ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)

Tactic:
rw [Xor, or_and_right, not_and_or, and_or_left, and_not_self_iff, false_or,
    and_or_left, and_not_self_iff, or_false]

Premises used: and_or_left, Xor, and_not_self_iff, false_or, not_and_or, or_false, or_and_right
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
s : α → Prop
p : α → α → Prop
⊢ (∀ (a : α), s a → ∀ (b : α), s b → p a b) ↔ ∀ (a b : α), s a → s b → p a b

Tactic:
⟨fun h a b ha hb ↦ h a ha b hb, fun h a ha b hb ↦ h a b ha hb⟩

Premises used: Iff.intro
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Membership α β
s : β
p : α → α → Prop
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → p a b) ↔ ∀ (a b : α), a ∈ s → b ∈ s → p a b

Tactic:
forall_cond_comm

Premises used: forall_cond_comm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b c : α
h₁ : a = b
h₂ : b ≠ c
⊢ a ≠ c

Tactic:
h₁.symm ▸ h₂

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
a b c : α
h₁ : a ≠ b
h₂ : b = c
⊢ a ≠ c

Tactic:
h₂ ▸ h₁

Premises used: Eq.rec
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
⊢ Equivalence.{u_1} (α := α) Eq

Tactic:
⟨Eq.refl, @Eq.symm _, @Eq.trans _⟩

Premises used: Eq.refl, Equivalence.mk, Eq.symm, Eq.trans
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
a b : α
h : a = b
⊢ ⋯ = ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f g : α → β
h : f = g
a : α
⊢ ⋯ = ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
f : α → β
a : α
⊢ ⋯ = ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
a a' : α
p : a = a'
b : β
⊢ ⋯ = ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_2
β : Sort u_1
a b : α
C : α → Sort u_1
x : C a
y : β
e : a = b
h : x ≍ y
⊢ HEq (α := C b) (Eq.rec (motive := fun (x : α) (h : a = x) ↦ C x) x e : C b) y

Tactic:
eqRec_heq_iff_heq.mpr h

Premises used: Iff.mpr, eqRec_heq_iff_heq
-- Module: Mathlib.Logic.Basic
Goal:
α β γ : Sort u_1
e : α = β
a : α
c : γ
subst : cast ⋯ a ≍ c ↔ a ≍ c
⊢ cast e a ≍ c ↔ a ≍ c

Tactic:
subst e
-- Module: Mathlib.Logic.Basic
Goal:
α γ : Sort u_1
a : α
c : γ
⊢ cast ⋯ a ≍ c ↔ a ≍ c

Tactic:
rfl
-- Module: Mathlib.Logic.Basic
Goal:
α β γ : Sort u_1
e : β = γ
a : α
b : β
subst : a ≍ cast ⋯ b ↔ a ≍ b
⊢ a ≍ cast e b ↔ a ≍ b

Tactic:
subst e
-- Module: Mathlib.Logic.Basic
Goal:
α β : Sort u_1
a : α
b : β
⊢ a ≍ cast ⋯ b ↔ a ≍ b

Tactic:
rfl
-- Module: Mathlib.Logic.Basic
Goal:
α β : Sort u
b : β
e : β = α
⊢ cast e b ≍ b

Tactic:
simp
-- Module: Mathlib.Logic.Basic
Goal:
α β : Sort u
e : β = α
a : α
b : β
h : a ≍ b
refl : ∀ {e : α = α}, a = cast e a
⊢ a = cast e b

Tactic:
cases h
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u
a : α
e : α = α
⊢ a = cast e a

Tactic:
rfl
-- Module: Mathlib.Logic.Basic
Goal:
β : Sort u
b a : β
h : a = cast ⋯ b
rw : cast ⋯ b ≍ b
rw₁ rw₂ : b ≍ b
⊢ a ≍ b

Tactic:
rw [h, cast_eq]

Premises used: cast_eq
-- Module: Mathlib.Logic.Basic
Goal:
α β : Sort u
a : α
b : β
⊢ a ≍ b ↔ ∃ (h : α = β), cast h a = b

Tactic:
simp only [heq_comm (a := a), heq_iff_exists_eq_cast, eq_comm]

Premises used: heq_iff_exists_eq_cast, eq_comm, heq_comm
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
p q : (a : α) → β a → Prop
h : ∀ (a : α) (b : β a), p a b → q a b
⊢ (∀ (a : α) (b : β a), p a b) → ∀ (a : α) (b : β a), q a b

Tactic:
forall_imp fun i ↦ forall_imp <| h i

Premises used: forall_imp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
γ : (a : α) → β a → Sort u_3
p q : (a : α) → (b : β a) → γ a b → Prop
h : ∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c
⊢ (∀ (a : α) (b : β a) (c : γ a b), p a b c) → ∀ (a : α) (b : β a) (c : γ a b), q a b c

Tactic:
forall_imp fun a ↦ forall₂_imp <| h a

Premises used: forall₂_imp, forall_imp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
p q : (a : α) → β a → Prop
h : ∀ (a : α) (b : β a), p a b → q a b
⊢ (∃ (a : α), ∃ (b : β a), p a b) → ∃ (a : α), ∃ (b : β a), q a b

Tactic:
Exists.imp fun a ↦ Exists.imp <| h a

Premises used: Exists.imp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
γ : (a : α) → β a → Sort u_3
p q : (a : α) → (b : β a) → γ a b → Prop
h : ∀ (a : α) (b : β a) (c : γ a b), p a b c → q a b c
⊢ (∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), p a b c) → ∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), q a b c

Tactic:
Exists.imp fun a ↦ Exists₂.imp <| h a

Premises used: Exists.imp, Exists₂.imp
-- 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:
⟨swap₂, swap₂⟩

Premises used: Function.swap₂, Iff.intro
-- Module: Mathlib.Logic.Basic
Goal:
α : Type u_3
p : Prop
q : α → Prop
⊢ (p → ∀ (x : α), q x) ↔ ∀ (x : α), p → q x

Tactic:
forall_comm

Premises used: forall_comm
-- Module: Mathlib.Logic.Basic
Goal:
A : Prop
B : A → Prop
pos : ∀ (h : A), (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
neg : ∀ (h : ¬A), (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
by_cases h : A
-- Module: Mathlib.Logic.Basic
Goal:
A : Prop
B : A → Prop
h : A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
A : Prop
B : A → Prop
h : ¬A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
simp [h]
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
β : Sort u_2
P : α → Prop
Q : β → Prop
⊢ ((∃ (a : α), P a) ∧ ∃ (b : β), Q b) ↔ ∃ (a : α), ∃ (b : β), P a ∧ Q b

Tactic:
⟨fun ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ↦ ⟨a, b, ⟨ha, hb⟩⟩, fun ⟨a, b, ⟨ha, hb⟩⟩ ↦ ⟨⟨a, ha⟩, ⟨b, hb⟩⟩⟩

Premises used: Exists, And, _private.0.exists_and_exists_comm.match_1, And.intro, Iff.intro, Exists.intro, _private.0.exists_and_exists_comm.match_2
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
p : α → Prop
⊢ (¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

Tactic:
open scoped Classical in Decidable.not_forall_not

Premises used: Decidable.not_forall_not
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : α → Prop
rw : (∀ (a : α), P a) ∨ ¬∀ (x : α), P x
⊢ (∀ (a : α), P a) ∨ ∃ (a : α), ¬P a

Tactic:
rw [← not_forall]

Premises used: Classical.not_forall
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Tactic:
em _

Premises used: em
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Tactic:
exact em _

Premises used: em
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : α → Prop
rw : (∃ (a : α), P a) ∨ ¬∃ (x : α), P x
⊢ (∃ (a : α), P a) ∨ ∀ (a : α), ¬P a

Tactic:
rw [← not_exists]

Premises used: not_exists
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : α → Prop
⊢ (∃ (a : α), P a) ∨ ¬∃ (x : α), P x

Tactic:
em _

Premises used: em
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_1
P : α → Prop
⊢ (∃ (a : α), P a) ∨ ¬∃ (x : α), P x

Tactic:
exact em _

Premises used: em
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
let : ∀ (a : α), (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b

Tactic:
let ⟨a⟩ := ha
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b

Tactic:
⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩

Premises used: not_forall_not, Iff.intro, Iff.mp, _private.0.forall_imp_iff_exists_imp.match_2
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
refine : ∀ (h : (∀ (x : α), p x) → b) (h' : ∀ (x : α), ¬(p x → b)), False
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b

Tactic:
refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False

Tactic:
if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (Classical.not_imp.1 (h' x)).1

Premises used: dite, And.left, Classical.not_imp, Iff.mp
-- Module: Mathlib.Logic.Basic
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False

Tactic:
exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (Classical.not_imp.1 (h' x)).1

Premises used: And.left, Classical.not_imp, Iff.mp