awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
unfold :
  card.{u_2} (α := ι) {i : ι | x i ≠ z i} ≤
    card.{u_2} (α := ι) {i : ι | x i ≠ y i} + card.{u_2} (α := ι) {i : ι | y i ≠ z i}
⊢ hammingDist (β := β) x z ≤ hammingDist (β := β) x y + hammingDist (β := β) y z
have unfold₁ : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} ({i : ι | x i ≠ y i} ∪ {i : ι | y i ≠ z i})
Tactic: classical
    unfold hammingDist
    refine le_trans (card_mono ?_) (card_union_le _ _)
    rw [← filter_or]
    exact monotone_filter_right _ fun i _ h ↦ (h.ne_or_ne _).imp_right Ne.symm
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
unfold :
  card.{u_2} (α := ι) {i : ι | x i ≠ z i} ≤
    card.{u_2} (α := ι) {i : ι | x i ≠ y i} + card.{u_2} (α := ι) {i : ι | y i ≠ z i}
unfold₁ : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} ({i : ι | x i ≠ y i} ∪ {i : ι | y i ≠ z i})
⊢ hammingDist (β := β) x z ≤ hammingDist (β := β) x y + hammingDist (β := β) y z
have unfold₂ : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} {a : ι | x a ≠ y a ∨ y a ≠ z a}
Tactic: classical
    unfold hammingDist
    refine le_trans (card_mono ?_) (card_union_le _ _)
    rw [← filter_or]
    exact monotone_filter_right _ fun i _ h ↦ (h.ne_or_ne _).imp_right Ne.symm
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist (β := β) x y ≤ hammingDist (β := β) z x + hammingDist (β := β) z y
have rw : hammingDist (β := β) x y ≤ hammingDist (β := β) x z + hammingDist (β := β) z y
Tactic: rw [hammingDist_comm z]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist (β := β) x y ≤ hammingDist (β := β) x z + hammingDist (β := β) y z
have rw : hammingDist (β := β) x y ≤ hammingDist (β := β) x z + hammingDist (β := β) z y
Tactic: rw [hammingDist_comm y]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ Eq (α := (y x : (i : ι) → β i) → ℕ) (swap (φ := fun (x y : (i : ι) → β i) ↦ ℕ) (hammingDist (β := β)))
    (hammingDist (β := β))
have h : ∀ (x y : (i : ι) → β i), swap (φ := fun (x y : (i : ι) → β i) ↦ ℕ) (hammingDist (β := β)) x y = hammingDist (β := β) x y
Tactic: funext x y
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist (β := β) x y = 0 → x = y
have simp_rw : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = 0 → x = y
Tactic: simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
simp_rw : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = 0 → x = y
⊢ hammingDist (β := β) x y = 0 → x = y
have simp_rw₁ : Eq.{u_2 + 1} (α := Finset ι) {i : ι | x i ≠ y i} ∅ → x = y
Tactic: simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
simp_rw : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = 0 → x = y
simp_rw₁ : Eq.{u_2 + 1} (α := Finset ι) {i : ι | x i ≠ y i} ∅ → x = y
⊢ hammingDist (β := β) x y = 0 → x = y
have simp_rw₂ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ y x_1) → x = y
Tactic: simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
simp_rw : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = 0 → x = y
simp_rw₁ : Eq.{u_2 + 1} (α := Finset ι) {i : ι | x i ≠ y i} ∅ → x = y
simp_rw₂ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ y x_1) → x = y
⊢ hammingDist (β := β) x y = 0 → x = y
have simp_rw₃ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → x x_1 = y x_1) → x = y
Tactic: simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
simp_rw : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = 0 → x = y
simp_rw₁ : Eq.{u_2 + 1} (α := Finset ι) {i : ι | x i ≠ y i} ∅ → x = y
simp_rw₂ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ y x_1) → x = y
simp_rw₃ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → x x_1 = y x_1) → x = y
⊢ hammingDist (β := β) x y = 0 → x = y
have simp_rw₄ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1
Tactic: simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
simp_rw : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = 0 → x = y
simp_rw₁ : Eq.{u_2 + 1} (α := Finset ι) {i : ι | x i ≠ y i} ∅ → x = y
simp_rw₂ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ y x_1) → x = y
simp_rw₃ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → x x_1 = y x_1) → x = y
simp_rw₄ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1
⊢ hammingDist (β := β) x y = 0 → x = y
have simp_rw₅ : (∀ ⦃x_1 : ι⦄, True → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1
Tactic: simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
simp_rw : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = 0 → x = y
simp_rw₁ : Eq.{u_2 + 1} (α := Finset ι) {i : ι | x i ≠ y i} ∅ → x = y
simp_rw₂ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ y x_1) → x = y
simp_rw₃ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → x x_1 = y x_1) → x = y
simp_rw₄ : (∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1
simp_rw₅ : (∀ ⦃x_1 : ι⦄, True → x x_1 = y x_1) → ∀ (x_1 : ι), x x_1 = y x_1
⊢ hammingDist (β := β) x y = 0 → x = y
have simp_rw₆ : (∀ ⦃x_1 : ι⦄, x x_1 = y x_1) → ∀ ⦃x_1 : ι⦄, x x_1 = y x_1
Tactic: simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
    forall_true_left, imp_self]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist (β := β) x y = 0
have rw : hammingDist (β := β) y y = 0
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ 0 = hammingDist (β := β) x y ↔ x = y
have rw : hammingDist (β := β) x y = 0 ↔ x = y
Tactic: rw [eq_comm, hammingDist_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
rw : hammingDist (β := β) x y = 0 ↔ x = y
⊢ 0 = hammingDist (β := β) x y ↔ x = y
have rw₁ : x = y ↔ x = y
Tactic: rw [eq_comm, hammingDist_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ 0 < hammingDist (β := β) x y ↔ x ≠ y
have rw : 0 < hammingDist (β := β) x y ↔ hammingDist (β := β) x y ≠ 0
Tactic: rw [← hammingDist_ne_zero, iff_not_comm, not_lt, Nat.le_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
rw : 0 < hammingDist (β := β) x y ↔ hammingDist (β := β) x y ≠ 0
⊢ 0 < hammingDist (β := β) x y ↔ x ≠ y
have rw₁ : hammingDist (β := β) x y = 0 ↔ ¬0 < hammingDist (β := β) x y
Tactic: rw [← hammingDist_ne_zero, iff_not_comm, not_lt, Nat.le_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
rw : 0 < hammingDist (β := β) x y ↔ hammingDist (β := β) x y ≠ 0
rw₁ : hammingDist (β := β) x y = 0 ↔ ¬0 < hammingDist (β := β) x y
⊢ 0 < hammingDist (β := β) x y ↔ x ≠ y
have rw₂ : hammingDist (β := β) x y = 0 ↔ hammingDist (β := β) x y ≤ 0
Tactic: rw [← hammingDist_ne_zero, iff_not_comm, not_lt, Nat.le_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
rw : 0 < hammingDist (β := β) x y ↔ hammingDist (β := β) x y ≠ 0
rw₁ : hammingDist (β := β) x y = 0 ↔ ¬0 < hammingDist (β := β) x y
rw₂ : hammingDist (β := β) x y = 0 ↔ hammingDist (β := β) x y ≤ 0
⊢ 0 < hammingDist (β := β) x y ↔ x ≠ y
have rw₃ : hammingDist (β := β) x y = 0 ↔ hammingDist (β := β) x y = 0
Tactic: rw [← hammingDist_ne_zero, iff_not_comm, not_lt, Nat.le_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist (β := β) x y < 1 ↔ x = y
have rw : hammingDist (β := β) x y = 0 ↔ x = y
Tactic: rw [Nat.lt_one_iff, hammingDist_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
rw : hammingDist (β := β) x y = 0 ↔ x = y
⊢ hammingDist (β := β) x y < 1 ↔ x = y
have rw₁ : x = y ↔ x = y
Tactic: rw [Nat.lt_one_iff, hammingDist_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst_2 : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
⊢ (hammingDist (β := β) (fun (i : ι) ↦ f i (x i)) fun (i : ι) ↦ f i (y i)) ≤ hammingDist (β := γ) x y
have dsimp : card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)} ≤ card.{u_2} (α := ι) {i : ι | ¬x i = y i}
Tactic: dsimp [hammingDist]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst_2 : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
⊢ card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)} ≤ card.{u_2} (α := ι) {i : ι | ¬x i = y i}
have a : ∀ (a : ι), Membership.mem (γ := Finset ι) univ a → x a = y a → f a (x a) = f a (y a)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst_2 : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ hammingDist (β := γ) x y ≤ hammingDist (β := β) (fun (i : ι) ↦ f i (x i)) fun (i : ι) ↦ f i (y i)
have dsimp : card.{u_2} (α := ι) {i : ι | ¬x i = y i} ≤ card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)}
Tactic: dsimp [hammingDist]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst_2 : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ card.{u_2} (α := ι) {i : ι | ¬x i = y i} ≤ card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)}
have a : ∀ (a : ι), Membership.mem (γ := Finset ι) univ a → f a (x a) = f a (y a) → x a = y a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingDist (β := β) 0 x = hammingNorm (β := β) x
have rw : hammingDist (β := β) x 0 = hammingNorm (β := β) x
Tactic: rw [hammingDist_comm, hammingDist_zero_right]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
rw : hammingDist (β := β) x 0 = hammingNorm (β := β) x
⊢ hammingDist (β := β) 0 x = hammingNorm (β := β) x
have rw₁ : hammingNorm (β := β) x = hammingNorm (β := β) x
Tactic: rw [hammingDist_comm, hammingDist_zero_right]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
⊢ hammingDist (β := β) x y = hammingNorm (β := β) (-x + y)
have simp_rw : hammingDist (β := β) x y = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
Tactic: simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
simp_rw : hammingDist (β := β) x y = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
⊢ hammingDist (β := β) x y = hammingNorm (β := β) (-x + y)
have simp_rw₁ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
Tactic: simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
simp_rw : hammingDist (β := β) x y = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
simp_rw₁ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
⊢ hammingDist (β := β) x y = hammingNorm (β := β) (-x + y)
have simp_rw₂ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {x_1 : ι | (-x) x_1 + y x_1 ≠ 0}
Tactic: simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
simp_rw : hammingDist (β := β) x y = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
simp_rw₁ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
simp_rw₂ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {x_1 : ι | (-x) x_1 + y x_1 ≠ 0}
⊢ hammingDist (β := β) x y = hammingNorm (β := β) (-x + y)
have simp_rw₃ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {x_1 : ι | -x x_1 + y x_1 ≠ 0}
Tactic: simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
x y : (i : ι) → β i
simp_rw : hammingDist (β := β) x y = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
simp_rw₁ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {i : ι | (-x + y) i ≠ 0}
simp_rw₂ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {x_1 : ι | (-x) x_1 + y x_1 ≠ 0}
simp_rw₃ : card.{u_2} (α := ι) {i : ι | x i ≠ y i} = card.{u_2} (α := ι) {x_1 : ι | -x x_1 + y x_1 ≠ 0}
⊢ hammingDist (β := β) x y = hammingNorm (β := β) (-x + y)
have simp_rw₄ : card.{u_2} (α := ι) {x_1 : ι | ¬x x_1 = y x_1} = card.{u_2} (α := ι) {x_1 : ι | ¬-x x_1 + y x_1 = 0}
Tactic: simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ Membership.mem (γ := Filter (Hamming β × Hamming β)) (uniformity (Hamming β)) s ↔
    ∃ ε > 0,
      ∀ {a b : Hamming β},
        (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) a)
                  ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) b)) :
              ℝ) <
            ε →
          (a, b) ∈ s
have mp : Membership.mem (γ := Filter (Hamming β × Hamming β)) (uniformity (Hamming β)) s →
  ∃ ε > 0,
    ∀ {a b : Hamming β},
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) a)
                ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) b)) :
            ℝ) <
          ε →
        (a, b) ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
mp :
  Membership.mem (γ := Filter (Hamming β × Hamming β)) (uniformity (Hamming β)) s →
    ∃ ε > 0,
      ∀ {a b : Hamming β},
        (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) a)
                  ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) b)) :
              ℝ) <
            ε →
          (a, b) ∈ s
⊢ Membership.mem (γ := Filter (Hamming β × Hamming β)) (uniformity (Hamming β)) s ↔
    ∃ ε > 0,
      ∀ {a b : Hamming β},
        (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) a)
                  ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) b)) :
              ℝ) <
            ε →
          (a, b) ∈ s
have mpr : (∃ ε > 0,
    ∀ {a b : Hamming β},
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) a)
                ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) b)) :
            ℝ) <
          ε →
        (a, b) ∈ s) →
  Membership.mem (γ := Filter (Hamming β × Hamming β)) (uniformity (Hamming β)) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
w : ℝ
hε : w > 0
hs :
  ∀ {a b : Hamming β},
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) a)
              ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) b)) :
          ℝ) <
        w →
      (a, b) ∈ s
fst : Hamming β
⊢ (fst, fst) ∈ s
have mpr : Eq (α := ℝ)
  (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)
        ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)) :
    ℝ)
  0
Tactic: refine hs (lt_of_eq_of_lt ?_ hε)
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ Eq (α := Set (Set (Hamming β))) (Filter.sets (Bornology.cobounded (Hamming β)))
    {s : Set (Hamming β) | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
have h : ∀ (x : Set (Hamming β)),
  Membership.mem (γ := Set (Set (Hamming β))) (Filter.sets (Bornology.cobounded (Hamming β))) x ↔
    Membership.mem (γ := Set (Set (Hamming β))) {s : Set (Hamming β) | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} x
Tactic: ext
-- Lean 4 proof step from Mathlib.InformationTheory.Hamming (goal)
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : Set (Hamming β)
⊢ Membership.mem (γ := Set (Set (Hamming β))) (Filter.sets ⊥) x ↔
    Membership.mem (γ := Set (Set (Hamming β)))
      {s : Set (Hamming β) |
        ∃ (C : ℝ),
          ∀ x ∈ sᶜ,
            ∀ y ∈ sᶜ,
              (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
                      ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
                  ℝ) ≤
                C}
      x
have h : ∀ x_1 ∈ xᶜ,
  ∀ x_3 ∈ xᶜ,
    LE.le (α := ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x_1)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x_3)) :
        ℝ)
      (↑(Fintype.card ι) : ℝ)
Tactic: refine iff_of_true (Filter.mem_sets.mpr Filter.mem_bot) ⟨Fintype.card ι, fun _ _ _ _ => ?_⟩
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
⊢ klDiv μ ν = ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)
have rw : (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
  ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)
Tactic: rw [klDiv_def]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ klDiv μ ν = ∞
have rw : (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) = ∞
Tactic: rw [klDiv_def]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ∞
have rw : (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) = ∞
Tactic: rw [klDiv_def]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ klDiv μ μ = 0
have h : llr μ μ =ᶠ[ae μ] 0
Tactic: have h := llr_self μ
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ klDiv μ μ = 0
have rw : ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + μ.real univ - μ.real univ) = 0
Tactic: rw [klDiv_def, if_pos]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
rw : ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + μ.real univ - μ.real univ) = 0
⊢ klDiv μ μ = 0
have hc : μ ≪ μ ∧ Integrable (llr μ μ) μ
Tactic: rw [klDiv_def, if_pos]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ μ ≪ μ ∧ Integrable (llr μ μ) μ
have hc : μ ≪ μ ∧ Integrable (ε := ℝ) 0 μ
Tactic: rw [integrable_congr h]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst : IsFiniteMeasure ν
⊢ klDiv 0 ν = (ν : (a : Set α) → ℝ≥0∞) univ
have h : (ν : (a : Set α) → ℝ≥0∞) univ =
  ENNReal.ofReal
    ((@integral _ _ _ _ mα 0 fun (x : α) ↦ llr 0 ν x) + ν.real univ - Measure.real.{u_1} (α := α) (m := mα) 0 univ)
Tactic: convert! klDiv_of_ac_of_integrable (Measure.AbsolutelyContinuous.zero _) integrable_zero_measure
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ klDiv μ ν = ∞ ↔ μ ≪ ν → ¬Integrable (llr μ ν) μ
have mp : klDiv μ ν = ∞ → μ ≪ ν → ¬Integrable (llr μ ν) μ
Tactic: constructor