awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
n : ℕ
⊢ (z / (↑n : ℂ)).re = z.re / (↑n : ℝ)
have rw : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.re = z.re / (↑n : ℝ)
Tactic: rw [div_natCast]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
n : ℕ
⊢ (z / (↑n : ℂ)).im = z.im / (↑n : ℝ)
have rw : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.im = z.im / (↑n : ℝ)
Tactic: rw [div_natCast]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
n : ℤ
⊢ (z / (↑n : ℂ)).re = z.re / (↑n : ℝ)
have rw : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.re = z.re / (↑n : ℝ)
Tactic: rw [div_intCast]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
n : ℤ
⊢ (z / (↑n : ℂ)).im = z.im / (↑n : ℝ)
have rw : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.im = z.im / (↑n : ℝ)
Tactic: rw [div_intCast]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
x : ℚ
⊢ (z / (↑x : ℂ)).re = z.re / (↑x : ℝ)
have rw : { re := z.re / (↑x : ℝ), im := z.im / (↑x : ℝ) : ℂ }.re = z.re / (↑x : ℝ)
Tactic: rw [div_ratCast]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
z : ℂ
x : ℚ
⊢ (z / (↑x : ℂ)).im = z.im / (↑x : ℝ)
have rw : { re := z.re / (↑x : ℝ), im := z.im / (↑x : ℝ) : ℂ }.im = z.im / (↑x : ℝ)
Tactic: rw [div_ratCast]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
α : Type u_1
n : ℕ
h : Eq (α := ℂ) (↑n : ℂ) 0
⊢ n = 0
have rwa : ∀ (h : (↑(↑n : ℝ) : ℂ) = 0), n = 0
Tactic: rwa [← ofReal_natCast, ofReal_eq_zero, Nat.cast_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
α : Type u_1
n : ℕ
h : Eq (α := ℂ) (↑n : ℂ) 0
rwa : ∀ (h : (↑(↑n : ℝ) : ℂ) = 0), n = 0
⊢ n = 0
have rwa₁ : ∀ (h : Eq (α := ℝ) (↑n : ℝ) 0), n = 0
Tactic: rwa [← ofReal_natCast, ofReal_eq_zero, Nat.cast_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
α : Type u_1
n : ℕ
h : Eq (α := ℂ) (↑n : ℂ) 0
rwa : ∀ (h : (↑(↑n : ℝ) : ℂ) = 0), n = 0
rwa₁ : ∀ (h : Eq (α := ℝ) (↑n : ℝ) 0), n = 0
⊢ n = 0
have rwa₂ : ∀ (h : n = 0), n = 0
Tactic: rwa [← ofReal_natCast, ofReal_eq_zero, Nat.cast_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
have rw : Subset (α := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s ×ˢ t) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s₁ ×ˢ t₁) ↔
  s ×ˢ t ⊆ s₁ ×ˢ t₁
Tactic: rw [← @preimage_equivRealProd_prod s t, ← @preimage_equivRealProd_prod s₁ t₁]
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
have h : s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
Tactic: convert! prod_subset_prod_iff
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a₁ a₂ b : ℝ
⊢ Eq (α := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]])
    ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b})
have h : ∀ (x : ℂ),
  Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a₁ a₂ b : ℝ
x : ℂ
⊢ Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
have h : Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x →
  Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a₁ a₂ b : ℝ
x : ℂ
h :
  Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x →
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
⊢ Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
have h₁ : Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x →
  Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a₁ a₂ b : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
have h : ∀ (x₁ : ℝ) (hx₁ : x₁ ∈ [[a₁, a₂]]) (hx₁' : (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) x₁ = x),
  Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
Tactic: obtain ⟨x₁, hx₁, hx₁'⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a₁ a₂ b : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
⊢ Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x
have h : ∀ (x₁ : ((equivRealProd : (a : ℂ) → ℝ × ℝ) x).1 ∈ [[a₁, a₂]]),
  Membership.mem (γ := Set ℂ)
    ((fun (x_1 : ℝ) ↦ (↑x_1 : ℂ) + (↑((equivRealProd : (a : ℂ) → ℝ × ℝ) x).2 : ℂ) * I) '' [[a₁, a₂]]) x
Tactic: obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
Cleared hypotheses: b, hx
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b₁ b₂ : ℝ
⊢ Eq (α := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]])
    ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]])
have h : ∀ (x : ℂ),
  Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b₁ b₂ : ℝ
x : ℂ
⊢ Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
have h : Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x →
  Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b₁ b₂ : ℝ
x : ℂ
h :
  Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x →
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
have h₁ : Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x →
  Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b₁ b₂ : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
have h : ∀ (x₁ : ℝ) (hx₁ : x₁ ∈ [[b₁, b₂]]) (hx₁' : (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) x₁ = x),
  Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
Tactic: obtain ⟨x₁, hx₁, hx₁'⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (hypothesis)
Goal:
a b₁ b₂ : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
have hx₁ : x.im ∈ [[b₁, b₂]] ∧ a = x.re
Tactic: simp only [equivRealProd_apply, singleton_prod, mem_image, Prod.mk.injEq,
      exists_eq_right_right, mem_preimage] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b₁ b₂ : ℝ
x : ℂ
hx : x.im ∈ [[b₁, b₂]] ∧ a = x.re
⊢ Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
have h : ∀ (x₁ : x.im ∈ [[b₁, b₂]]), Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑x.re : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
Tactic: obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
Cleared hypotheses: a, hx
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Sort u
⊢ Uncountable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
have rw : ¬Countable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
Tactic: rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff]
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Sort u
rw : ¬Countable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
⊢ Uncountable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
have rw₁ : ¬Nonempty.{max 1 u} (α ↪ ℕ) ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
Tactic: rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff]
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Sort u
rw : ¬Countable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
rw₁ : ¬Nonempty.{max 1 u} (α ↪ ℕ) ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
⊢ Uncountable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
have rw₂ : IsEmpty.{max 1 u} (α ↪ ℕ) ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
Tactic: rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff]
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
⊢ Countable (α ⊕ β)
have rcases : ∀ (f : α → ℕ) (hf : Injective f), Countable (α ⊕ β)
Tactic: rcases exists_injective_nat α with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α ⊕ β)
have rcases : ∀ (g : β → ℕ) (hg : Injective g), Countable (α ⊕ β)
Tactic: rcases exists_injective_nat β with ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
⊢ Countable (α × β)
have rcases : ∀ (f : α → ℕ) (hf : Injective f), Countable (α × β)
Tactic: rcases exists_injective_nat α with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α × β)
have rcases : ∀ (g : β → ℕ) (hg : Injective g), Countable (α × β)
Tactic: rcases exists_injective_nat β with ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Uncountable α
inst_1 : Nonempty β
⊢ Uncountable (α × β)
have inhabit : ∀ (inhabited_h : Inhabited β), Uncountable (α × β)
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : Uncountable β
⊢ Uncountable (α × β)
have inhabit : ∀ (inhabited_h : Inhabited α), Uncountable (α × β)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty β
h : Countable (α × β)
⊢ Countable α
have contrapose! : ∀ (h : Uncountable α), Uncountable (α × β)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Nonempty α
h : Countable (α × β)
⊢ Countable β
have contrapose! : ∀ (h : Uncountable β), Uncountable (α × β)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : ∀ (a : α), Countable.{w + 1} (π a)
⊢ Countable (Sigma π)
have rcases : ∀ (f : α → ℕ) (hf : Injective f), Countable (Sigma π)
Tactic: rcases exists_injective_nat α with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Countable α
inst_1 : ∀ (a : α), Countable.{w + 1} (π a)
f : α → ℕ
hf : Injective f
⊢ Countable (Sigma π)
have choose : ∀ (g : (a : α) → π a → ℕ) (hg : ∀ (a : α), Injective (g a)), Countable (Sigma π)
Tactic: choose g hg using fun a => exists_injective_nat (π a)
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Type u
β : Type v
π : α → Type w
inst : Nonempty α
inst_1 : ∀ (a : α), Uncountable.{w + 1} (π a)
⊢ Uncountable (Sigma π)
have inhabit : ∀ (inhabited_h : Inhabited α), Uncountable (Sigma π)
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
n : ℕ
⊢ Countable (Fin n → ℕ)
have zero : Countable (Fin 0 → ℕ)
Tactic: induction n with
    | zero => infer_instance
    | succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
n : ℕ
zero : Countable (Fin 0 → ℕ)
⊢ Countable (Fin n → ℕ)
have succ : ∀ (n : ℕ) (ihn : Countable (Fin n → ℕ)), Countable (Fin (n + 1) → ℕ)
Tactic: induction n with
    | zero => infer_instance
    | succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (hypothesis)
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
⊢ Countable ((a : α) → π a)
have this : ∀ (n : ℕ), Countable (Fin n → ℕ)
Tactic: have (n : ℕ) : Countable (Fin n → ℕ) := by
    induction n with
    | zero => infer_instance
    | succ n ihn => exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Fin.consEquiv fun _ ↦ ℕ)
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
⊢ Countable ((a : α) → π a)
have rcases : ∀ (n : ℕ) (e : α ≃ Fin n), Countable ((a : α) → π a)
Tactic: rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.Data.Countable.Basic (goal)
Goal:
α : Sort u
β : Sort v
π : α → Sort w
inst : Finite α
inst_1 : ∀ (a : α), Countable.{w} (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
⊢ Countable ((a : α) → π a)
have have : ∀ (f : (a : α) → Embedding.{w, 1} (π a) ℕ), Countable ((a : α) → π a)
Tactic: have f := fun a => (nonempty_embedding_nat (π a)).some
-- Lean 4 proof step from Mathlib.Data.Countable.Defs (goal)
Goal:
α : Sort u
⊢ ¬Uncountable α ↔ Countable α
have rw : ¬¬Countable α ↔ Countable α
Tactic: rw [uncountable_iff_not_countable, not_not]
-- Lean 4 proof step from Mathlib.Data.Countable.Defs (goal)
Goal:
α : Sort u
rw : ¬¬Countable α ↔ Countable α
⊢ ¬Uncountable α ↔ Countable α
have rw₁ : Countable α ↔ Countable α
Tactic: rw [uncountable_iff_not_countable, not_not]
-- Lean 4 proof step from Mathlib.Data.Countable.Defs (goal)
Goal:
α : Sort u
inst : Nonempty α
⊢ Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f
have rw : ¬Countable α ↔ ∀ (f : ℕ → α), ¬Surjective f
Tactic: rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]
-- Lean 4 proof step from Mathlib.Data.Countable.Defs (goal)
Goal:
α : Sort u
inst : Nonempty α
rw : ¬Countable α ↔ ∀ (f : ℕ → α), ¬Surjective f
⊢ Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f
have rw₁ : (¬∃ (f : ℕ → α), Surjective f) ↔ ∀ (f : ℕ → α), ¬Surjective f
Tactic: rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]
-- Lean 4 proof step from Mathlib.Data.Countable.Defs (goal)
Goal:
α : Sort u
inst : Nonempty α
rw : ¬Countable α ↔ ∀ (f : ℕ → α), ¬Surjective f
rw₁ : (¬∃ (f : ℕ → α), Surjective f) ↔ ∀ (f : ℕ → α), ¬Surjective f
⊢ Uncountable α ↔ ∀ (f : ℕ → α), ¬Surjective f
have rw₂ : (∀ (x : ℕ → α), ¬Surjective x) ↔ ∀ (f : ℕ → α), ¬Surjective f
Tactic: rw [← not_countable_iff, countable_iff_exists_surjective, not_exists]
-- Lean 4 proof step from Mathlib.Data.Countable.Small (goal)
Goal:
α : Type v
h : ¬Small.{w, v} α
⊢ Uncountable α
have rw : ¬Countable α
Tactic: rw [uncountable_iff_not_countable]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support (β := β) ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
⊢ Eq.{w + 1} (α := γ) (∏ i ∈ f.support (β := β), g i ((f : (a : ι) → β a) i)) (∏ i ∈ s, g i ((f : (a : ι) → β a) i))
have apply : ∀ x ∈ s, x ∉ f.support (β := β) → g x ((f : (a : ι) → β a) x) = 1
Tactic: apply Finset.prod_subset hs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f : Π₀ (i : ι), β i
g : (i : ι) → β i → γ
s : Finset ι
hs : f.support (β := β) ⊆ s
map_zero : ∀ i ∈ s, g i 0 = 1
i : ι
hi : i ∈ s
hi' : i ∉ f.support (β := β)
⊢ g i ((f : (a : ι) → β a) i) = 1
have hi'₁ : (f : (a : ι) → β a) i = 0
Tactic: simp only [DFinsupp.mem_support_toFun, ne_eq, not_not] at hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → Zero (β i)
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst_3 : CommMonoid γ
f1 f2 : Π₀ (i : ι), β i
g1 g2 : (i : ι) → β i → γ
h : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x ((f1 : (a : ι) → β a) x) = g2 x ((f2 : (a : ι) → β a) x)
h1 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g1 x 0 = 1
h2 : ∀ x ∈ f1.support (β := β) ∪ f2.support (β := β), g2 x 0 = 1
⊢ f1.prod (β := β) g1 = f2.prod (β := β) g2
have rw : Eq.{w + 1} (α := γ) (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g1 i ((f1 : (a : ι) → β a) i))
  (∏ i ∈ f1.support (β := β) ∪ f2.support (β := β), g2 i ((f2 : (a : ι) → β a) i))
Tactic: rw [prod_of_support_subset Finset.subset_union_left h1,
    prod_of_support_subset Finset.subset_union_right h2]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf g).prod (β := β₂) h = g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)
have rw : prod (β := β₂)
    (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
      f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
    h =
  g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)
Tactic: rw [mapRange_def]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ prod (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
      h =
    g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)
have refine_1 : ∀ x ∈ g.support (β := β₁),
  x ∉
      support (β := β₂)
        (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
          f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι))) →
    h x
        ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
              f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
            (a : ι) → β₂ a)
          x) =
      1
Tactic: refine (Finset.prod_subset support_mk_subset ?_).trans ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (goal)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
refine_1 :
  ∀ x ∈ g.support (β := β₁),
    x ∉
        support (β := β₂)
          (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι))) →
      h x
          ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
                f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
              (a : ι) → β₂ a)
            x) =
        1
⊢ prod (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
      h =
    g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b)
have refine_2 : Eq.{w + 1} (α := γ)
  (∏ x ∈ g.support (β := β₁),
    h x
      ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        x))
  (g.prod (β := β₁) fun (i : ι) (b : β₁ i) ↦ h i (f i b))
Tactic: refine (Finset.prod_subset support_mk_subset ?_).trans ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h1 : i ∈ g.support (β := β₁)
h2 :
  i ∉
    support (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
⊢ h i
      ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        i) =
    1
have h1₁ : ¬(g : (a : ι) → β₁ a) i = 0
Tactic: simp only [mem_support_toFun, ne_eq] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.DFinsupp.BigOperators (hypothesis)
Goal:
ι : Type u
γ : Type w
inst : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst_1 : (i : ι) → Zero (β₁ i)
inst_2 : (i : ι) → Zero (β₂ i)
inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst_5 : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
i : ι
h2 :
  i ∉
    support (β := β₂)
      (mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
        f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)))
h1 : ¬(g : (a : ι) → β₁ a) i = 0
⊢ h i
      ((mk (β := β₂) (g.support (β := β₁)) fun (i : (↑(↑(g.support (β := β₁)) : Set ι) : Type u)) ↦
            f (↑i : ι) ((g : (a : ι) → β₁ a) (↑i : ι)) :
          (a : ι) → β₂ a)
        i) =
    1
have h2₁ : f i ((g : (a : ι) → β₁ a) i) = 0
Tactic: simp only [Finset.coe_sort_coe, mem_support_toFun, mk_apply, ne_eq, h1, not_false_iff,
      dite_eq_ite, ite_true, not_not] at h2
Cleared hypotheses: h2