awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.Hamming
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}
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}
⊢ hammingDist (β := β) x y = hammingNorm (β := β) (-x + y)

Tactic:
simp_rw [hammingNorm, hammingDist, Pi.add_apply, Pi.neg_apply, ne_eq, neg_add_eq_zero]

Premises used: hammingNorm, hammingDist, ne_eq, Pi.add_apply, neg_add_eq_zero, Pi.neg_apply
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Inhabited ι
inst_1 : ∀ (i : ι), Nonempty.{u_3 + 1} (β i)
inst_2 : Nontrivial.{u_3} (β default)
⊢ Nontrivial (Hamming β)

Tactic:
inferInstanceAs <| Nontrivial (∀ i, β i)

Premises used: _private.0.Hamming.instNontrivialOfNonemptyOfDefault._proof_1
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
⊢ Eq (α := Hamming β ≃ ((i : ι) → β i)) (Equiv.symm (toHamming (β := β))) (ofHamming (β := β))

Tactic:
rfl

Premises used: Hamming.ofHamming, Hamming, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
⊢ Eq (α := ((i : ι) → β i) ≃ Hamming β) (Equiv.symm (ofHamming (β := β))) (toHamming (β := β))

Tactic:
rfl

Premises used: Hamming, Equiv.symm, Hamming.toHamming, Equiv.refl, rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
x : Hamming β
⊢ (toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
x : (i : ι) → β i
⊢ (ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i)
      ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) x : Hamming β) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
x y : (i : ι) → β i
⊢ Eq (α := Hamming β) ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) x : Hamming β)
      ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) y : Hamming β) ↔
    x = y

Tactic:
Iff.rfl

Premises used: Iff.rfl, Hamming
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
x y : Hamming β
⊢ Eq (α := (i : ι) → β i) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x : (i : ι) → β i)
      ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y : (i : ι) → β i) ↔
    x = y

Tactic:
Iff.rfl

Premises used: Iff.rfl, Hamming
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Zero (β i)
⊢ Eq (α := Hamming β) ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Zero (β i)
⊢ Eq (α := (i : ι) → β i) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) 0 : (i : ι) → β i) (0 : (i : ι) → β i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Neg (β i)
x : (i : ι) → β i
⊢ Eq (α := Hamming β) ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) (-x) : Hamming β)
    (-(toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) x : Hamming β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Neg (β i)
x : Hamming β
⊢ Eq (α := (i : ι) → β i) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) (-x) : (i : ι) → β i)
    (-(ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x : (i : ι) → β i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Add (β i)
x y : (i : ι) → β i
⊢ (toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) (x + y) =
    HAdd.hAdd (α := Hamming β) (β := Hamming β) ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) x : Hamming β)
      ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) y : Hamming β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Add (β i)
x y : Hamming β
⊢ (ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) (x + y) =
    HAdd.hAdd (α := (i : ι) → β i) (β := (i : ι) → β i)
      ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x : (i : ι) → β i)
      ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y : (i : ι) → β i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Sub (β i)
x y : (i : ι) → β i
⊢ (toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) (x - y) =
    HSub.hSub (α := Hamming β) (β := Hamming β) ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) x : Hamming β)
      ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) y : Hamming β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → Sub (β i)
x y : Hamming β
⊢ (ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) (x - y) =
    HSub.hSub (α := (i : ι) → β i) (β := (i : ι) → β i)
      ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x : (i : ι) → β i)
      ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y : (i : ι) → β i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → SMul.{u_1, u_3} α (β i)
r : α
x : (i : ι) → β i
⊢ (toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) (r • x) =
    HSMul.hSMul (β := Hamming β) r ((toHamming (β := β) : (a : (i : ι) → β i) → Hamming β) x : Hamming β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : (i : ι) → SMul.{u_1, u_3} α (β i)
r : α
x : Hamming β
⊢ (ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) (r • x) =
    HSMul.hSMul (β := (i : ι) → β i) r ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x : (i : ι) → β i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : Hamming β
⊢ dist x y =
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
      ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β),
    Eq (α := ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)) :
        ℝ)
      0

Tactic:
mod_cast hammingDist_self

Premises used: hammingDist_self, congrArg, cast, hammingDist, Nat.cast, Hamming.ofHamming, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Eq, DFunLike.coe, Eq.trans, forall_congr
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ ∀ (x : Hamming β),
    Eq (α := ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)) :
        ℝ)
      0

Tactic:
exact mod_cast hammingDist_self

Premises used: hammingDist_self
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β),
    Eq (α := ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
        ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)) :
        ℝ)

Tactic:
mod_cast hammingDist_comm

Premises used: cast, Nat.cast_inj._simp_1, hammingDist_comm, Eq.symm, forall_congr
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y : Hamming β),
    Eq (α := ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
        ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)) :
        ℝ)

Tactic:
exact mod_cast hammingDist_comm

Premises used: hammingDist_comm
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β),
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) z)) :
        ℝ) ≤
      HAdd.hAdd (α := ℝ)
        (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
              ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
          ℝ)
        (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)
              ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) z)) :
          ℝ)

Tactic:
mod_cast hammingDist_triangle

Premises used: congrArg, hammingDist_triangle, Nat.cast_add._simp_1, cast, hammingDist, Nat.cast_le._simp_1, LE.le, Nat.cast, Hamming.ofHamming, Eq.symm, DFunLike.coe, Eq.trans, forall_congr
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β),
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) z)) :
        ℝ) ≤
      HAdd.hAdd (α := ℝ)
        (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
              ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
          ℝ)
        (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)
              ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) z)) :
          ℝ)

Tactic:
exact mod_cast hammingDist_triangle

Premises used: hammingDist_triangle
-- Module: Mathlib.InformationTheory.Hamming
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
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
⊢ 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
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
hs : Membership.mem (γ := Filter (Hamming β × Hamming β)) (uniformity (Hamming β)) s
a b : Hamming β
hab :
  LT.lt (α := ℝ)
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) a)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) b)) :
      ℝ)
    1
⊢ Membership.mem (γ := Set (Hamming β × Hamming β)) SetRel.id (a, b)

Tactic:
simpa using hab
-- Module: Mathlib.InformationTheory.Hamming
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

Tactic:
refine fun hs ↦ ⟨1, zero_lt_one, fun hab ↦ hs <| by simpa using hab⟩
-- Module: Mathlib.InformationTheory.Hamming
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

Tactic:
hs (lt_of_eq_of_lt ?_ hε)

Premises used: lt_of_eq_of_lt
-- Module: Mathlib.InformationTheory.Hamming
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 β
mpr :
  Eq (α := ℝ)
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)) :
      ℝ)
    0
⊢ (fst, fst) ∈ s

Tactic:
refine hs (lt_of_eq_of_lt ?_ hε)

Premises used: lt_of_eq_of_lt
-- Module: Mathlib.InformationTheory.Hamming
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 β
⊢ Eq (α := ℝ)
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)) :
      ℝ)
    0

Tactic:
mod_cast hammingDist_self _

Premises used: hammingDist_self, congrArg, cast, hammingDist, Nat.cast, Hamming.ofHamming, Nat.cast_inj._simp_1, Nat.cast_zero, Eq.symm, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.InformationTheory.Hamming
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 β
⊢ Eq (α := ℝ)
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) fst)) :
      ℝ)
    0

Tactic:
exact mod_cast hammingDist_self _

Premises used: hammingDist_self
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
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
⊢ Eq (α := Set (Set (Hamming β))) (Filter.sets (Bornology.cobounded (Hamming β)))
    {s : Set (Hamming β) | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}

Tactic:
ext
-- Module: Mathlib.InformationTheory.Hamming
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

Tactic:
iff_of_true (Filter.mem_sets.mpr Filter.mem_bot) ⟨Fintype.card ι, fun _ _ _ _ => ?_⟩

Premises used: Iff.mpr, Filter.mem_sets, Filter.mem_bot, Fintype.card, Nat.cast, iff_of_true, Exists.intro
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : Set (Hamming β)
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 ι) : ℝ)
⊢ 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

Tactic:
refine iff_of_true (Filter.mem_sets.mpr Filter.mem_bot) ⟨Fintype.card ι, fun _ _ _ _ => ?_⟩

Premises used: Iff.mpr, Filter.mem_sets, Filter.mem_bot, iff_of_true
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : Set (Hamming β)
x_1 : Hamming β
h : x_1 ∈ xᶜ
x_2 : Hamming β
h_1 : x_2 ∈ xᶜ
⊢ LE.le (α := ℝ)
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x_1)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x_2)) :
      ℝ)
    (↑(Fintype.card ι) : ℝ)

Tactic:
mod_cast hammingDist_le_card_fintype

Premises used: cast, Nat.cast_le._simp_1, Eq.symm, hammingDist_le_card_fintype
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : Set (Hamming β)
x_1 : Hamming β
h : x_1 ∈ xᶜ
x_2 : Hamming β
h_1 : x_2 ∈ xᶜ
⊢ LE.le (α := ℝ)
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x_1)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x_2)) :
      ℝ)
    (↑(Fintype.card ι) : ℝ)

Tactic:
exact mod_cast hammingDist_le_card_fintype

Premises used: hammingDist_le_card_fintype
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : Hamming β
⊢ nndist x y =
    (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
          ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
      NNReal)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
⊢ DiscreteTopology (Hamming β)

Tactic:
⟨rfl⟩

Premises used: DiscreteTopology.mk, rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : Hamming β
⊢ ‖x‖ = (↑(hammingNorm (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
⊢ ∀ (x y : Hamming β),
    Eq (α := ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
        ℝ)
      (↑(hammingNorm (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) (-x + y))) : ℝ)

Tactic:
mod_cast hammingDist_eq_hammingNorm

Premises used: cast, Nat.cast_inj._simp_1, Eq.symm, hammingDist_eq_hammingNorm, forall_congr
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
⊢ ∀ (x y : Hamming β),
    Eq (α := ℝ)
      (↑(hammingDist (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)
            ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) y)) :
        ℝ)
      (↑(hammingNorm (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) (-x + y))) : ℝ)

Tactic:
exact mod_cast hammingDist_eq_hammingNorm

Premises used: hammingDist_eq_hammingNorm
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → AddGroup (β i)
x : Hamming β
⊢ ‖x‖₊ = (↑(hammingNorm (β := β) ((ofHamming (β := β) : (a : Hamming β) → (i : ι) → β i) x)) : NNReal)

Tactic:
rfl

Premises used: NNReal.mk, rfl
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
rw :
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)
⊢ klDiv μ ν = ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)

Tactic:
rw [klDiv_def]

Premises used: InformationTheory.klDiv_def
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)

Tactic:
if_pos ⟨h1, h2⟩

Premises used: if_pos
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h1 : μ ≪ ν
h2 : Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)

Tactic:
exact if_pos ⟨h1, h2⟩

Premises used: if_pos
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
rw :
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ∞
⊢ klDiv μ ν = ∞

Tactic:
rw [klDiv_def]

Premises used: InformationTheory.klDiv_def
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ∞

Tactic:
if_neg (not_and_of_not_left _ h)

Premises used: not_and_of_not_left, if_neg