awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
rw : Eq (α := (x : ℕ) → ℝ) (fun (n : ℕ) ↦ (↑(Nat.fib n) : ℝ)) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
⊢ ∀ (n : ℕ), (↑(Nat.fib n) : ℝ) = (φ ^ n - ψ ^ n) / √5
have rw₁ : Eq (α := (x : ℕ) → ℝ) (fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5) fun (n : ℕ) ↦ (φ ^ n - ψ ^ n) / √5
Tactic: rw [← funext_iff, Real.coe_fib_eq']
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℤ
⊢ (↑(Int.fib n) : ℝ) = (φ ^ n - ψ ^ n) / √5
have inl : ∀ (n : ℕ), (↑(Int.fib (↑n : ℤ)) : ℝ) = (HPow.hPow (β := ℤ) φ (↑n : ℤ) - HPow.hPow (β := ℤ) ψ (↑n : ℤ)) / √5
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℤ
inl : ∀ (n : ℕ), (↑(Int.fib (↑n : ℤ)) : ℝ) = (HPow.hPow (β := ℤ) φ (↑n : ℤ) - HPow.hPow (β := ℤ) ψ (↑n : ℤ)) / √5
⊢ (↑(Int.fib n) : ℝ) = (φ ^ n - ψ ^ n) / √5
have inr : ∀ (n : ℕ), (↑(Int.fib (-(↑n : ℤ))) : ℝ) = (HPow.hPow (β := ℤ) φ (-(↑n : ℤ)) - HPow.hPow (β := ℤ) ψ (-(↑n : ℤ))) / √5
Tactic: obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
⊢ (↑(Int.fib (-(↑n : ℤ))) : ℝ) = (HPow.hPow (β := ℤ) φ (-(↑n : ℤ)) - HPow.hPow (β := ℤ) ψ (-(↑n : ℤ))) / √5
have inr : (if Even n then -(↑(Nat.fib n) : ℝ) else (↑(Nat.fib n) : ℝ)) =
  ((if Even n then 1 else -1) * ψ ^ n - (if Even n then 1 else -1) * φ ^ n) / √5
Tactic: simp only [Int.fib_neg, Int.even_coe_nat, Int.fib_natCast, Int.cast_ite, Int.cast_neg,
      Int.cast_natCast, zpow_neg, zpow_natCast, ← inv_pow, inv_goldenRatio, inv_goldenConj,
      ← neg_one_mul ψ, ← neg_one_mul φ, mul_pow, neg_one_pow_eq_ite]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
⊢ (↑(Nat.fib (n + 1)) : ℝ) - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n
have rw : (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n
Tactic: rw [coe_fib_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n
have rw : (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
Tactic: rw [coe_fib_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
⊢ (↑(Nat.fib (n + 1)) : ℝ) - φ * (↑(Nat.fib n) : ℝ) = ψ ^ n
have repeat : (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
Tactic: repeat rw [coe_fib_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1)) / √5 - φ * ((φ ^ n - ψ ^ n) / √5) = ψ ^ n
have rw : (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n
Tactic: rw [mul_div, div_sub_div_same, mul_sub, ← pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
⊢ (φ ^ (n + 1) - ψ ^ (n + 1) - (φ ^ (n + 1) - φ * ψ ^ n)) / √5 = ψ ^ n
have ring_nf : √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (hypothesis)
Goal:
n : ℕ
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
have nz : √5 ≠ 0
Tactic: have nz : √5 ≠ 0 := by norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
nz : √5 ≠ 0
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
have rw : 1 * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
Tactic: rw [← (mul_inv_cancel₀ nz).symm, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
nz : √5 ≠ 0
rw : 1 * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
⊢ √5 * (√5)⁻¹ * (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
have rw₁ : (1 / 2 + √5 * (-1 / 2)) ^ n = (1 / 2 + √5 * (-1 / 2)) ^ n
Tactic: rw [← (mul_inv_cancel₀ nz).symm, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
    φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ)
have simp : φ * HAdd.hAdd (α := ℝ) (↑(Nat.fib n) : ℝ) (↑(Nat.fib n.succ) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
  φ * (↑(Nat.fib n) : ℝ) + (φ + 1) * (↑(Nat.fib (n + 1)) : ℝ)
Tactic: simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
⊢ φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ)) = φ ^ (n + 2)
have rw : φ * φ ^ (n + 1) = φ ^ (n + 2)
Tactic: rw [add_comm, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) = φ ^ (n + 1 + 1)
have _ : φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
  φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ)
Tactic: calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
_ :
  φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
    φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ)
⊢ φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) = φ ^ (n + 1 + 1)
have _₁ : φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ) =
  φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ))
Tactic: calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
_ :
  φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) =
    φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ)
_₁ :
  φ * (↑(Nat.fib n) : ℝ) + HPow.hPow (β := ℕ) φ 2 * (↑(Nat.fib (n + 1)) : ℝ) =
    φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ))
⊢ φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) = φ ^ (n + 1 + 1)
have _₂ : φ * ((↑(Nat.fib n) : ℝ) + φ * (↑(Nat.fib (n + 1)) : ℝ)) = φ ^ (n + 2)
Tactic: calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
⊢ φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
have zero : φ * (↑(Nat.fib (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + (↑(Nat.fib 0) : ℝ) = φ ^ HAdd.hAdd (α := ℕ) 0 1
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Real.GoldenRatio (goal)
Goal:
n : ℕ
zero : φ * (↑(Nat.fib (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + (↑(Nat.fib 0) : ℝ) = φ ^ HAdd.hAdd (α := ℕ) 0 1
⊢ φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)
have succ : ∀ (n : ℕ) (ih : φ * (↑(Nat.fib (n + 1)) : ℝ) + (↑(Nat.fib n) : ℝ) = φ ^ (n + 1)),
  φ * (↑(Nat.fib (n + 1 + 1)) : ℝ) + (↑(Nat.fib (n + 1)) : ℝ) = φ ^ (n + 1 + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
have refine_1 : LE.le.{u_2} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
refine_1 : LE.le.{u_2} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
have refine_2 : LE.le.{u_2} (α := α) (⨆ (t : Finset ι), ⨆ i ∈ t, s i) (⨆ (i : ι), s i)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
have refine_1 : LE.le.{u_2} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
Tactic: classical
  refine le_antisymm ?_ ?_
  · exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
  · exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
α : Type u_2
ι : Type u_5
inst : CompleteLattice α
s : ι → α
refine_1 : LE.le.{u_2} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι), s i) (⨆ (t : Finset ι), ⨆ i ∈ t, s i)
have refine_2 : LE.le.{u_2} (α := α) (⨆ (t : Finset ι), ⨆ i ∈ t, s i) (⨆ (i : ι), s i)
Tactic: classical
  refine le_antisymm ?_ ?_
  · exact iSup_le fun b => le_iSup_of_le {b} <| le_iSup_of_le b <| le_iSup_of_le (by simp) <| le_rfl
  · exact iSup_le fun t => iSup_le fun b => iSup_le fun _ => le_iSup _ _
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
α : Type u_2
ι' : Sort u_7
inst : CompleteLattice α
s : ι' → α
⊢ Eq.{u_2 + 1} (α := α) (⨆ (i : ι'), s i) (⨆ (t : Finset (PLift ι')), ⨆ i ∈ t, s i.down)
have rw : Eq.{u_2 + 1} (α := α) (⨆ (x : PLift ι'), s ((Equiv.plift : (a : PLift ι') → ι') x)) (⨆ (i : PLift ι'), s i.down)
Tactic: rw [← iSup_eq_iSup_finset, ← Equiv.plift.surjective.iSup_comp]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
ι : Type u_5
s : Set ι
⊢ ⋃ (s' : Finset (↑s : Type u_5)), Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_5)) = s
have h : ∀ (x : ι),
  Membership.mem (γ := Set ι)
      (⋃ (s' : Finset (↑s : Type u_5)), Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_5))) x ↔
    x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
ι : Type u_5
s : Set ι
x : ι
⊢ Membership.mem (γ := Set ι)
      (⋃ (s' : Finset (↑s : Type u_5)), Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_5))) x ↔
    x ∈ s
have h : (∃ (i : Finset (↑s : Type u_5)) (x_1 : x ∈ s), Subtype.mk (p := fun (a : ι) ↦ a ∈ s) x sorry ∈ i) ↔ x ∈ s
Tactic: simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, Subtype.exists,
    exists_and_right, exists_eq_right]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s
⊢ Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s)
have simp : P s → ((∀ ⦃y : Finset α⦄, P y → s ≤ y → y ≤ s) ↔ ∀ x ∉ s, ¬P (insert x s))
Tactic: simp only [Maximal, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CompleteLattice β
inst_1 : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ ⨆ i ∈ insert x t, update (β := fun (a : α) ↦ β) f x s i = s ⊔ ⨆ i ∈ t, f i
have rw : update (β := fun (a : α) ↦ β) f x s x ⊔ ⨆ x_1 ∈ t, update (β := fun (a : α) ↦ β) f x s x_1 = s ⊔ ⨆ i ∈ t, f i
Tactic: rw [Finset.iSup_insert]
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
hl : l.Subsingleton
⊢ ∃ (a : α), l = pure a
have rcases : ∀ (s : Set α) (hsl : s ∈ l) (hs : s.Subsingleton), ∃ (a : α), l = pure a
Tactic: rcases hl with ⟨s, hsl, hs⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
s : Set α
hsl : s ∈ l
hs : s.Subsingleton
⊢ ∃ (a : α), l = pure a
have rcases : ∀ (a : α) (hsl : {a} ∈ l) (hs : Set.Subsingleton (α := α) {a}), ∃ (a : α), l = pure a
Tactic: rcases exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨nonempty_of_mem hsl, hs⟩ with ⟨a, rfl⟩
Cleared hypotheses: s, hsl, hs
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
inst : l.NeBot
a : α
hsl : {a} ∈ l
hs : Set.Subsingleton (α := α) {a}
⊢ ∃ (a : α), l = pure a
have refine : l ≤ pure a
Tactic: refine ⟨a, (NeBot.le_pure_iff ‹_›).1 ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
⊢ l.Subsingleton ↔ l = ⊥ ∨ ∃ (a : α), l = pure a
have refine_1 : ∀ (hl : l.Subsingleton), l = ⊥ ∨ ∃ (a : α), l = pure a
Tactic: refine ⟨fun hl ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
refine_1 : ∀ (hl : l.Subsingleton), l = ⊥ ∨ ∃ (a : α), l = pure a
⊢ l.Subsingleton ↔ l = ⊥ ∨ ∃ (a : α), l = pure a
have refine_2 : (l = ⊥ ∨ ∃ (a : α), l = pure a) → l.Subsingleton
Tactic: refine ⟨fun hl ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
inst : Nonempty α
⊢ l.Subsingleton ↔ ∃ (a : α), l ≤ pure a
have inl : Filter.Subsingleton.{u_1} (α := α) ⊥ ↔ ∃ (a : α), LE.le (α := Filter α) ⊥ (pure a)
Tactic: rcases eq_or_neBot l with rfl | hbot
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
inst : Nonempty α
inl : Filter.Subsingleton.{u_1} (α := α) ⊥ ↔ ∃ (a : α), LE.le (α := Filter α) ⊥ (pure a)
⊢ l.Subsingleton ↔ ∃ (a : α), l ≤ pure a
have inr : ∀ (hbot : l.NeBot), l.Subsingleton ↔ ∃ (a : α), l ≤ pure a
Tactic: rcases eq_or_neBot l with rfl | hbot
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
hl : l.Subsingleton
⊢ l.IsCountablyGenerated
have inl : ∀ (hl : Filter.Subsingleton.{u_1} (α := α) ⊥), IsCountablyGenerated.{u_1} (α := α) ⊥
Tactic: rcases subsingleton_iff_bot_or_pure.1 hl with rfl | ⟨x, rfl⟩
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Order.Filter.Subsingleton (goal)
Goal:
α : Type u_1
l : Filter α
hl : l.Subsingleton
inl : ∀ (hl : Filter.Subsingleton.{u_1} (α := α) ⊥), IsCountablyGenerated.{u_1} (α := α) ⊥
⊢ l.IsCountablyGenerated
have inr : ∀ (x : α) (hl : Filter.Subsingleton (pure x)), IsCountablyGenerated (pure x)
Tactic: rcases subsingleton_iff_bot_or_pure.1 hl with rfl | ⟨x, rfl⟩
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ≤ g
have rw : Disjoint (↑f : Filter α) g ↔ ¬((↑f : Filter α) ⊓ g).NeBot
Tactic: rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
rw : Disjoint (↑f : Filter α) g ↔ ¬((↑f : Filter α) ⊓ g).NeBot
⊢ Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ≤ g
have rw₁ : Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ⊓ g ≠ ⊥
Tactic: rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
rw : Disjoint (↑f : Filter α) g ↔ ¬((↑f : Filter α) ⊓ g).NeBot
rw₁ : Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ⊓ g ≠ ⊥
⊢ Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ≤ g
have rw₂ : Disjoint (↑f : Filter α) g ↔ ¬¬(↑f : Filter α) ⊓ g = ⊥
Tactic: rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
rw : Disjoint (↑f : Filter α) g ↔ ¬((↑f : Filter α) ⊓ g).NeBot
rw₁ : Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ⊓ g ≠ ⊥
rw₂ : Disjoint (↑f : Filter α) g ↔ ¬¬(↑f : Filter α) ⊓ g = ⊥
⊢ Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ≤ g
have rw₃ : Disjoint (↑f : Filter α) g ↔ (↑f : Filter α) ⊓ g = ⊥
Tactic: rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Ultrafilter α
g : Filter α
rw : Disjoint (↑f : Filter α) g ↔ ¬((↑f : Filter α) ⊓ g).NeBot
rw₁ : Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ⊓ g ≠ ⊥
rw₂ : Disjoint (↑f : Filter α) g ↔ ¬¬(↑f : Filter α) ⊓ g = ⊥
rw₃ : Disjoint (↑f : Filter α) g ↔ (↑f : Filter α) ⊓ g = ⊥
⊢ Disjoint (↑f : Filter α) g ↔ ¬(↑f : Filter α) ≤ g
have rw₄ : (↑f : Filter α) ⊓ g = ⊥ ↔ (↑f : Filter α) ⊓ g = ⊥
Tactic: rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Ultrafilter α
s : Set α
⊢ sᶜ ∈ f ↔ s ∉ f
have rw : sᶜᶜ ∉ f ↔ s ∉ f
Tactic: rw [← compl_notMem_iff, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Ultrafilter α
s : Set α
rw : sᶜᶜ ∉ f ↔ s ∉ f
⊢ sᶜ ∈ f ↔ s ∉ f
have rw₁ : s ∉ f ↔ s ∉ f
Tactic: rw [← compl_notMem_iff, compl_compl]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter α
h₀ : optParam (Injective.{u + 1, u + 1} (α := α) id) ⋯
⊢ range id ∈ f
have rw : univ ∈ f
Tactic: rw [range_id]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
f_1 g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ range (n ∘ m) ∈ f
have rw : n '' range m ∈ f
Tactic: rw [range_comp]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : Membership.mem (γ := Ultrafilter β) (pure (m a)) (range m)
⊢ 𝓟 (m ⁻¹' {m a}) = (↑(pure a) : Filter α)
have rw : 𝓟 (m ⁻¹' {m a}) = pure a
Tactic: rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : Membership.mem (γ := Ultrafilter β) (pure (m a)) (range m)
rw : 𝓟 (m ⁻¹' {m a}) = pure a
⊢ 𝓟 (m ⁻¹' {m a}) = (↑(pure a) : Filter α)
have rw₁ : 𝓟 (m ⁻¹' {m a}) = 𝓟 {a}
Tactic: rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : Membership.mem (γ := Ultrafilter β) (pure (m a)) (range m)
rw : 𝓟 (m ⁻¹' {m a}) = pure a
rw₁ : 𝓟 (m ⁻¹' {m a}) = 𝓟 {a}
⊢ 𝓟 (m ⁻¹' {m a}) = (↑(pure a) : Filter α)
have rw₂ : 𝓟 (m ⁻¹' m '' {a}) = 𝓟 {a}
Tactic: rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : Membership.mem (γ := Ultrafilter β) (pure (m a)) (range m)
rw : 𝓟 (m ⁻¹' {m a}) = pure a
rw₁ : 𝓟 (m ⁻¹' {m a}) = 𝓟 {a}
rw₂ : 𝓟 (m ⁻¹' m '' {a}) = 𝓟 {a}
⊢ 𝓟 (m ⁻¹' {m a}) = (↑(pure a) : Filter α)
have rw₃ : Eq (α := Filter α) (𝓟 {a}) (𝓟 {a})
Tactic: rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Filter α
hf : f.NeBot
x : α
⊢ f = pure x ↔ {x} ∈ f
have rw : f ≤ pure x ↔ {x} ∈ f
Tactic: rw [← hf.le_pure_iff, le_pure_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Filter α
hf : f.NeBot
x : α
rw : f ≤ pure x ↔ {x} ∈ f
⊢ f = pure x ↔ {x} ∈ f
have rw₁ : {x} ∈ f ↔ {x} ∈ f
Tactic: rw [← hf.le_pure_iff, le_pure_iff]
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
f : Filter α
s : Set α
⊢ s ∈ f ↔ ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g
have refine : ∀ (H : ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g) (hf : s ∉ f), False
Tactic: refine ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (hypothesis)
Goal:
α : Type u
f : Filter α
s : Set α
H : ∀ (g : Ultrafilter α), (↑g : Filter α) ≤ f → s ∈ g
hf : s ∉ f
g : Filter (↑sᶜ : Type u) := comap (Subtype.val (p := fun (x : α) ↦ x ∈ sᶜ)) f
⊢ False
have this : g.NeBot
Tactic: haveI : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_setOf])
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
g : Filter α
p : Filter α → Prop
hp : Monotone p
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → p (↑f : Filter α)
have refine : (∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → p (↑f : Filter α)) → ∀ (f : Filter α), f.NeBot → f ≤ g → p f
Tactic: refine ⟨fun H f hf => H f f.neBot hf, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (hypothesis)
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal (s := s) h
have this : f.NeBot
Tactic: haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (hypothesis)
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ s ∈ ofComapInfPrincipal (s := s) h
have this₁ : s ∈ f
Tactic: have : s ∈ f := mem_inf_of_right (mem_principal_self s)
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (hypothesis)
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal (s := s) h) = g
have this : f.NeBot
Tactic: haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ map m (ofComapInfPrincipal (s := s) h) = g
have h₁ : (↑(map m (ofComapInfPrincipal (s := s) h)) : Filter β) ≤ (↑g : Filter β)
Tactic: apply eq_of_le
-- Lean 4 proof step from Mathlib.Order.Filter.Ultrafilter.Defs (goal)
Goal:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m (↑g : Filter β) ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ Filter.map m (𝓟 s) =
    Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s)
have rw : Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s) = Filter.map m (Filter.comap m (↑g : Filter β)) ⊓ 𝓟 (m '' s)
Tactic: rw [map_principal]