awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (hypothesis)
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 :
  Eq (α := ℤ) (det (n := Fin (n + 1)) (vandermonde fun (i : Fin (n + 1)) ↦ (↑(w' i) : ℤ)))
    (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)))
⊢ (↑n.superFactorial : ℤ) ∣ (vandermonde v).det
have 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))
Tactic: conv_lhs at h => simp only [hw', det_vandermonde_sub]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Vandermonde (goal)
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))
⊢ (↑n.superFactorial : ℤ) ∣ (vandermonde v).det
have 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 : ℕ)) : ℤ)))
Tactic: use (of (fun (i j : Fin (n + 1)) => (Nat.choose (w' i) (j : ℕ) : ℤ))).det
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
a b : α
⊢ (a = b) = (b = a)
have rw : (b = a) = (b = a)
Tactic: rw [@eq_comm _ a b]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
a b : Prop
⊢ (a ↔ b) = (b ↔ a)
have rw : (b ↔ a) = (b ↔ a)
Tactic: rw [@iff_comm a b]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
inst : Subsingleton α
p : α → Prop
x_1 x_2 : Subtype p
x : α
property : p x
y : α
property_1 : p y
⊢ Eq.{max 1 u_1} (Subtype.mk (p := p) x property) (Subtype.mk (p := p) y property_1)
have refl : ∀ (property_2 : p x), Eq.{max 1 u_1} (Subtype.mk (p := p) x property) (Subtype.mk (p := p) x property_2)
Tactic: cases Subsingleton.elim x y
Cleared hypotheses: y, property_1
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α β : Sort u_2
γ : Sort u_3
f : α → γ
g : β → γ
x : α
y : β
h₁ : f ≍ g
h₂ : x ≍ y
⊢ f x = g y
have refl : ∀ {g : α → γ} (h₁ : f ≍ g), f x = g x
Tactic: cases h₂
Cleared hypotheses: β, g, y, h₁, h₂
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
g : α → γ
h₁ : f ≍ g
⊢ f x = g x
have refl : f x = f x
Tactic: cases h₁
Cleared hypotheses: g, h₁
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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₂
⊢ f₁ a₁ ≍ f₂ a₂
have refl : ∀ {β₂ : α₁ → Sort v} {f₂ : (a : α₁) → β₂ a} (ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂)
  (hf : α₁ = α₁ → β₁ ≍ β₂ → f₁ ≍ f₂), f₁ a₁ ≍ f₂ a₁
Tactic: cases hargs
Cleared hypotheses: α₂, β₂, f₂, a₂, hargs, ht, hf
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
β₂ : α₁ → Sort v
f₂ : (a : α₁) → β₂ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₁ → β₁ ≍ β₂ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₁
have refl : ∀ {f₂ : (a : α₁) → β₁ a} (ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂) (hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₂),
  f₁ a₁ ≍ f₂ a₁
Tactic: cases funext fun v => ht v v .rfl
Cleared hypotheses: β₂, f₂, ht, hf
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
f₂ : (a : α₁) → β₁ a
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂
hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₁
have refl : ∀ (hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₁), f₁ a₁ ≍ f₁ a₁
Tactic: cases hf rfl .rfl
Cleared hypotheses: f₂, hf
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = c
have rw : b = b
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = b ↔ a = c
have rw : a = c ↔ a = c
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ a = b
have rw : b = b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
a_1 b : α
h : a_1 = b
a : α
⊢ a_1 = a ↔ b = a
have rw : b = a ↔ b = a
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
a b : Prop
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw : a ∧ ¬b ∨ b ∧ ¬a ↔ (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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
a b : Prop
rw : a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∨ b) ∧ ¬(a ∧ b)
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₁ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬(a ∧ b) ∨ 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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
a b : Prop
rw : a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∨ b) ∧ ¬(a ∧ b)
rw₁ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬(a ∧ b) ∨ b ∧ ¬(a ∧ b)
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₂ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ (¬a ∨ ¬b) ∨ 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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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)
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₃ : a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∧ ¬a ∨ a ∧ ¬b) ∨ 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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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)
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₄ : a ∧ ¬b ∨ b ∧ ¬a ↔ (False ∨ a ∧ ¬b) ∨ 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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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)
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₅ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ 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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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)
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₆ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ b ∧ ¬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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₇ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ False
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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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
⊢ Xor a b ↔ (a ∨ b) ∧ ¬(a ∧ b)
have rw₈ : a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a
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]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α β γ : Sort u_1
e : α = β
a : α
c : γ
⊢ cast e a ≍ c ↔ a ≍ c
have subst : cast sorry a ≍ c ↔ a ≍ c
Tactic: subst e
Cleared hypotheses: β, e
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α β γ : Sort u_1
e : β = γ
a : α
b : β
⊢ a ≍ cast e b ↔ a ≍ b
have subst : a ≍ cast sorry b ↔ a ≍ b
Tactic: subst e
Cleared hypotheses: γ, e
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α β : Sort u
e : β = α
a : α
b : β
h : a ≍ b
⊢ a = cast e b
have refl : ∀ {e : α = α}, a = cast e a
Tactic: cases h
Cleared hypotheses: β, e, b, h
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
β : Sort u
b a : β
h : a = cast ⋯ b
⊢ a ≍ b
have rw : cast sorry b ≍ b
Tactic: rw [h, cast_eq]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
β : Sort u
b a : β
h : a = cast ⋯ b
rw : cast ⋯ b ≍ b
⊢ a ≍ b
have rw₁ : b ≍ b
Tactic: rw [h, cast_eq]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
A : Prop
B : A → Prop
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
have pos : ∀ (h : A), (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
Tactic: by_cases h : A
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
A : Prop
B : A → Prop
pos : ∀ (h : A), (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
have neg : ∀ (h : ¬A), (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
Tactic: by_cases h : A
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ∃ (a : α), ¬P a
have rw : (∀ (a : α), P a) ∨ ¬∀ (x : α), P x
Tactic: rw [← not_forall]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P : α → Prop
⊢ (∃ (a : α), P a) ∨ ∀ (a : α), ¬P a
have rw : (∃ (a : α), P a) ∨ ¬∃ (x : α), P x
Tactic: rw [← not_exists]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
have let : ∀ (a : α), (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
Tactic: let ⟨a⟩ := ha
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
have refine : ∀ (h : (∀ (x : α), p x) → b) (h' : ∀ (x : α), ¬(p x → b)), False
Tactic: refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
have let : ∀ (a : α), (∀ (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
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
let let₁ let₂ : ∀ (a : α), (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
⊢ (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
have let₃ : ∀ (a : α) (h : (∀ (x : α), p x) → b) (h' : ∀ (x : α), ¬(p x → b)), False
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
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
p : Prop → Prop
h_1 : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
⊢ p h
have pos : ∀ (H : h), p h
Tactic: by_cases H : h
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
p : Prop → Prop
h_1 : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
pos : ∀ (H : h), p h
⊢ p h
have neg : ∀ (H : ¬h), p h
Tactic: by_cases H : h
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
ι : Sort u_3
inst : Subsingleton ι
P : ι → ι → Prop
⊢ (∀ (i j : ι), P i j) ↔ ∀ (i : ι), P i i
have refine : ∀ (i : ι), (∀ (j : ι), P i j) ↔ P i i
Tactic: refine forall_congr' fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Logic.Basic (hypothesis)
Goal:
ι : Sort u_3
inst : Subsingleton ι
P : ι → ι → Prop
i : ι
⊢ (∀ (j : ι), P i j) ↔ P i i
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨i⟩
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
inst : Nonempty α
q : Prop
p : α → Prop
⊢ (∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x
have rw : ((∀ (x : α), q) ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x
Tactic: rw [forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
inst : Nonempty α
q : Prop
p : α → Prop
rw : ((∀ (x : α), q) ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x
⊢ (∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x
have rw₁ : (q ∧ ∀ (x : α), p x) ↔ q ∧ ∀ (x : α), p x
Tactic: rw [forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
inst : Nonempty α
p : α → Prop
q : Prop
⊢ (∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q
have rw : ((∀ (x : α), p x) ∧ ∀ (x : α), q) ↔ (∀ (x : α), p x) ∧ q
Tactic: rw [forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
inst : Nonempty α
p : α → Prop
q : Prop
rw : ((∀ (x : α), p x) ∧ ∀ (x : α), q) ↔ (∀ (x : α), p x) ∧ q
⊢ (∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q
have rw₁ : (∀ (x : α), p x) ∧ q ↔ (∀ (x : α), p x) ∧ q
Tactic: rw [forall_and, forall_const]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
r p q : α → Prop
⊢ (∃ (x : α), ∃ (x_1 : p x ∨ q x), r x) ↔ (∃ (x : α), ∃ (x_1 : p x), r x) ∨ ∃ (x : α), ∃ (x_1 : q x), r x
have simp : (∃ (x : α), (p x ∨ q x) ∧ r x) ↔ (∃ (x : α), p x ∧ r x) ∨ ∃ (x : α), q x ∧ r x
Tactic: simp only [exists_prop]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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
have pos : P → (dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c)
Tactic: by_cases P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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)
⊢ dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c
have neg : ¬P → (dite P A B = c ↔ (∃ (h : P), A h = c) ∨ ∃ (h : ¬P), B h = c)
Tactic: by_cases P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b c : α
⊢ ((∃ (h : P), a = c) ∨ ∃ (h : ¬P), b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
have rw : (P ∧ a = c ∨ ∃ (h : ¬P), b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
Tactic: rw [exists_prop, exists_prop]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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
⊢ ((∃ (h : P), a = c) ∨ ∃ (h : ¬P), b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
have rw₁ : P ∧ a = c ∨ ¬P ∧ b = c ↔ P ∧ a = c ∨ ¬P ∧ b = c
Tactic: rw [exists_prop, exists_prop]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
⊢ (∃ (h : ¬P), a ≠ b) ↔ ¬P ∧ a ≠ b
have rw : ¬P ∧ a ≠ b ↔ ¬P ∧ a ≠ b
Tactic: rw [exists_prop]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P : Prop
inst : Decidable P
a b : α
⊢ (∃ (h : P), a ≠ b) ↔ P ∧ a ≠ b
have rw : P ∧ a ≠ b ↔ P ∧ a ≠ b
Tactic: rw [exists_prop]
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
have 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)
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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)
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
have 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)
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
⊢ dite P f g a = if h : P then f h a else g h a
have pos : ∀ (h : P), dite P f g a = if h : P then f h a else g h a
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
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
⊢ dite P f g a = if h : P then f h a else g h a
have neg : ∀ (h : ¬P), dite P f g a = if h : P then f h a else g h a
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
have pos : ∀ (hp : P), (if P ∧ Q then a else b) = if P then if Q then a else b else b
Tactic: by_cases hp : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
pos : ∀ (hp : P), (if P ∧ Q then a else b) = if P then if Q then a else b else b
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
have neg : ∀ (hp : ¬P), (if P ∧ Q then a else b) = if P then if Q then a else b else b
Tactic: by_cases hp : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
have pos : ∀ (hq : Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
pos : ∀ (hq : Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
have neg : ∀ (hq : ¬Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
have pos : ∀ (hq : Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
pos : ∀ (hq : Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
have neg : ∀ (hq : ¬Q), (if P ∧ Q then a else b) = if P then if Q then a else b else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
have pos : ∀ (hp : P), (if P ∨ Q then a else b) = if P then a else if Q then a else b
Tactic: by_cases hp : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
pos : ∀ (hp : P), (if P ∨ Q then a else b) = if P then a else if Q then a else b
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
have neg : ∀ (hp : ¬P), (if P ∨ Q then a else b) = if P then a else if Q then a else b
Tactic: by_cases hp : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
have pos : ∀ (hq : Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : P
pos : ∀ (hq : Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
have neg : ∀ (hq : ¬Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
have pos : ∀ (hq : Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
α : Sort u_1
P Q : Prop
inst : Decidable P
a b : α
inst_1 : Decidable Q
hp : ¬P
pos : ∀ (hq : Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
have neg : ∀ (hq : ¬Q), (if P ∨ Q then a else b) = if P then a else if Q then a else b
Tactic: by_cases hq : Q
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P Q R : Prop
inst : Decidable P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
have pos : ∀ (p : P), (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
Tactic: by_cases p : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P Q R : Prop
inst : Decidable P
pos : ∀ (p : P), (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
have neg : ∀ (p : ¬P), (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
Tactic: by_cases p : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
have pos : ∀ (h : P), dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
pos : ∀ (h : P), dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
⊢ dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
have neg : ∀ (h : ¬P), dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
Tactic: by_cases h : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P Q R : Prop
inst : Decidable P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
have pos : ∀ (p : P), (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
Tactic: by_cases p : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P Q R : Prop
inst : Decidable P
pos : ∀ (p : P), (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
have neg : ∀ (p : ¬P), (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
Tactic: by_cases p : P
-- Lean 4 proof step from Mathlib.Logic.Basic (goal)
Goal:
P : Prop
inst : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
have pos : ∀ (h : P), dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
Tactic: by_cases h : P