awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
pos : ∀ (hn : Nat.card G = 1), (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
neg : ∀ (hn : ¬Nat.card G = 1), (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)

Tactic:
by_cases hn : Nat.card G = 1

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : Nat.card G = 1
this : Subsingleton G
pos : IsComplement'.{u_3} (G := G) ⊥ ⊤
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)

Tactic:
rw [Subsingleton.elim (MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)).ker ⊥,
      Subsingleton.elim P.1 ⊤]

Premises used: Sylow.toSubgroup, Bot.bot, MonoidHom.ker, MonoidHom.transferSylow, Subsingleton.elim, Top.top, IsCyclic.normalizer_le_centralizer, rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : Nat.card G = 1
this : Subsingleton G
⊢ IsComplement'.{u_3} (G := G) ⊥ ⊤

Tactic:
isComplement'_bot_top

Premises used: Subgroup.isComplement'_bot_top
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : Nat.card G = 1
this : Subsingleton G
⊢ IsComplement'.{u_3} (G := G) ⊥ ⊤

Tactic:
exact isComplement'_bot_top

Premises used: Subgroup.isComplement'_bot_top
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)

Tactic:
MonoidHom.ker_transferSylow_isComplement' P (hP.normalizer_le_centralizer rfl)

Premises used: MonoidHom.ker_transferSylow_isComplement', IsCyclic.normalizer_le_centralizer, rfl
-- Module: Mathlib.GroupTheory.Transfer
Goal:
G : Type u_3
inst : Group G
inst_1 : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic.{u_3} ↥(↑P : Subgroup G)
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' (↑P : Subgroup G)

Tactic:
exact MonoidHom.ker_transferSylow_isComplement' P (hP.normalizer_le_centralizer rfl)

Premises used: MonoidHom.ker_transferSylow_isComplement', IsCyclic.normalizer_le_centralizer, rfl
-- Module: Mathlib.InformationTheory.Coding.UniquelyDecodable
Goal:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
⊢ ¬[] ∈ S

Tactic:
simpa using h [[]] [[], []]

Premises used: List.cons, List.nil
-- Module: Mathlib.InformationTheory.Coding.UniquelyDecodable
Goal:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }
hflat :
  Eq.{u_1 + 1} (α := List α)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₁)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₂)
a : (↑L₁ : List (List α)) = (↑L₂ : List (List α))
⊢ L₁ = L₂

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.InformationTheory.Coding.UniquelyDecodable
Goal:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }
hflat :
  Eq.{u_1 + 1} (α := List α)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₁)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₂)
⊢ (↑L₁ : List (List α)) = (↑L₂ : List (List α))

Tactic:
h L₁.val L₂.val L₁.prop L₂.prop hflat

Premises used: Subtype.prop, Subtype.val
-- Module: Mathlib.InformationTheory.Coding.UniquelyDecodable
Goal:
α : Type u_1
S : Set (List α)
h : UniquelyDecodable S
L₁ L₂ : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }
hflat :
  Eq.{u_1 + 1} (α := List α)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₁)
    ((fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) ↦ (↑L : List (List α)).flatten) L₂)
⊢ (↑L₁ : List (List α)) = (↑L₂ : List (List α))

Tactic:
exact h L₁.val L₂.val L₁.prop L₂.prop hflat

Premises used: Subtype.prop, Subtype.val
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
rw : ∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ x x_1
⊢ hammingDist (β := β) x x = 0

Tactic:
rw [hammingDist, card_eq_zero, filter_eq_empty_iff]

Premises used: hammingDist, Finset.filter_eq_empty_iff, Finset.card_eq_zero
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ x x_1

Tactic:
fun _ _ H => H rfl

Premises used: Not, rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, Membership.mem (γ := Finset ι) univ x_1 → ¬x x_1 ≠ x x_1

Tactic:
exact fun _ _ H => H rfl
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ 0 ≤ hammingDist (β := β) x y

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ card.{u_2} (α := ι) {i : ι | x i ≠ z i} ≤
    card.{u_2} (α := ι) {i : ι | x i ≠ y i} + card.{u_2} (α := ι) {i : ι | y i ≠ z i}

Tactic:
le_trans (card_mono ?_) (card_union_le _ _)

Premises used: Finset.card_union_le, Finset.card_mono, le_trans
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
refine : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} ({i : ι | x i ≠ y i} ∪ {i : ι | y i ≠ z i})
⊢ card.{u_2} (α := ι) {i : ι | x i ≠ z i} ≤
    card.{u_2} (α := ι) {i : ι | x i ≠ y i} + card.{u_2} (α := ι) {i : ι | y i ≠ z i}

Tactic:
refine le_trans (card_mono ?_) (card_union_le _ _)

Premises used: Finset.card_union_le, Finset.card_mono, le_trans
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
rw : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} {a : ι | x a ≠ y a ∨ y a ≠ z a}
⊢ LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} ({i : ι | x i ≠ y i} ∪ {i : ι | y i ≠ z i})

Tactic:
rw [← filter_or]

Premises used: Finset.filter_or
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} {a : ι | x a ≠ y a ∨ y a ≠ z a}

Tactic:
monotone_filter_right _ fun i _ h ↦ (h.ne_or_ne _).imp_right Ne.symm

Premises used: Finset.monotone_filter_right, Ne.symm, Or.imp_right, Ne.ne_or_ne
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} {a : ι | x a ≠ y a ∨ y a ≠ z a}

Tactic:
exact monotone_filter_right _ fun i _ h ↦ (h.ne_or_ne _).imp_right Ne.symm

Premises used: Finset.monotone_filter_right
-- Module: Mathlib.InformationTheory.Hamming
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})
unfold₂ : LE.le.{u_2} (α := Finset ι) {i : ι | x i ≠ z i} {a : ι | x a ≠ y a ∨ y a ≠ z a}
⊢ hammingDist (β := β) x z ≤ hammingDist (β := β) x y + hammingDist (β := β) y z

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

Premises used: hammingDist, Finset.monotone_filter_right, Finset.card_union_le, Finset.filter_or, Finset.card_mono, le_trans
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
rw : hammingDist (β := β) x y ≤ hammingDist (β := β) x z + hammingDist (β := β) z y
⊢ hammingDist (β := β) x y ≤ hammingDist (β := β) z x + hammingDist (β := β) z y

Tactic:
rw [hammingDist_comm z]

Premises used: hammingDist_comm
-- Module: Mathlib.InformationTheory.Hamming
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 (β := β) z y

Tactic:
hammingDist_triangle _ _ _

Premises used: hammingDist_triangle
-- Module: Mathlib.InformationTheory.Hamming
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 (β := β) z y

Tactic:
exact hammingDist_triangle _ _ _

Premises used: hammingDist_triangle
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
rw : hammingDist (β := β) x y ≤ hammingDist (β := β) x z + hammingDist (β := β) z y
⊢ hammingDist (β := β) x y ≤ hammingDist (β := β) x z + hammingDist (β := β) y z

Tactic:
rw [hammingDist_comm y]

Premises used: hammingDist_comm
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
h :
  ∀ (x y : (i : ι) → β i),
    swap (φ := fun (x y : (i : ι) → β i) ↦ ℕ) (hammingDist (β := β)) x y = hammingDist (β := β) x y
⊢ Eq (α := (y x : (i : ι) → β i) → ℕ) (swap (φ := fun (x y : (i : ι) → β i) ↦ ℕ) (hammingDist (β := β)))
    (hammingDist (β := β))

Tactic:
funext x y
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ swap (φ := fun (x y : (i : ι) → β i) ↦ ℕ) (hammingDist (β := β)) x y = hammingDist (β := β) x y

Tactic:
hammingDist_comm _ _

Premises used: hammingDist_comm
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ swap (φ := fun (x y : (i : ι) → β i) ↦ ℕ) (hammingDist (β := β)) x y = hammingDist (β := β) x y

Tactic:
exact hammingDist_comm _ _

Premises used: hammingDist_comm
-- Module: Mathlib.InformationTheory.Hamming
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
simp_rw₆ : (∀ ⦃x_1 : ι⦄, x x_1 = y x_1) → ∀ ⦃x_1 : ι⦄, x x_1 = y x_1
⊢ hammingDist (β := β) x y = 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]

Premises used: Finset.mem_univ, forall_true_left, Classical.not_not, funext_iff, hammingDist, Finset.filter_eq_empty_iff, imp_self, Finset.card_eq_zero
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
rw : hammingDist (β := β) y y = 0
⊢ hammingDist (β := β) x y = 0

Tactic:
rw [H]
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist (β := β) y y = 0

Tactic:
hammingDist_self _

Premises used: hammingDist_self
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
H : x = y
⊢ hammingDist (β := β) y y = 0

Tactic:
exact hammingDist_self _

Premises used: hammingDist_self
-- Module: Mathlib.InformationTheory.Hamming
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
rw₁ rw₂ : x = y ↔ x = y
⊢ 0 = hammingDist (β := β) x y ↔ x = y

Tactic:
rw [eq_comm, hammingDist_eq_zero]

Premises used: hammingDist_eq_zero, eq_comm
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist (β := β) x y ≠ 0 ↔ x ≠ y

Tactic:
hammingDist_eq_zero.not

Premises used: hammingDist_eq_zero, Iff.not
-- Module: Mathlib.InformationTheory.Hamming
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
rw₃ rw₄ : hammingDist (β := β) x y = 0 ↔ hammingDist (β := β) x y = 0
⊢ 0 < hammingDist (β := β) x y ↔ x ≠ y

Tactic:
rw [← hammingDist_ne_zero, iff_not_comm, not_lt, Nat.le_zero]

Premises used: iff_not_comm, Nat.le_zero, not_lt, hammingDist_ne_zero
-- Module: Mathlib.InformationTheory.Hamming
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
rw₁ rw₂ : x = y ↔ x = y
⊢ hammingDist (β := β) x y < 1 ↔ x = y

Tactic:
rw [Nat.lt_one_iff, hammingDist_eq_zero]

Premises used: hammingDist_eq_zero, Nat.lt_one_iff
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist (β := β) x y ≤ Fintype.card ι

Tactic:
card_le_univ _

Premises used: hammingDist, Finset.card_le_univ
-- Module: Mathlib.InformationTheory.Hamming
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
dsimp : card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)} ≤ card.{u_2} (α := ι) {i : ι | ¬x i = y i}
⊢ (hammingDist (β := β) (fun (i : ι) ↦ f i (x i)) fun (i : ι) ↦ f i (y i)) ≤ hammingDist (β := γ) x y

Tactic:
dsimp [hammingDist]

Premises used: hammingDist
-- Module: Mathlib.InformationTheory.Hamming
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
a : ∀ (a : ι), Membership.mem (γ := Finset ι) univ a → x a = y a → f a (x a) = f a (y a)
⊢ card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)} ≤ card.{u_2} (α := ι) {i : ι | ¬x i = y i}

Tactic:
gcongr
-- Module: Mathlib.InformationTheory.Hamming
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
a : ι
h : Membership.mem (γ := Finset ι) univ a
⊢ x a = y a → f a (x a) = f a (y a)

Tactic:
simp +contextual
-- Module: Mathlib.InformationTheory.Hamming
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)
dsimp : card.{u_2} (α := ι) {i : ι | ¬x i = y i} ≤ card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)}
⊢ hammingDist (β := γ) x y ≤ hammingDist (β := β) (fun (i : ι) ↦ f i (x i)) fun (i : ι) ↦ f i (y i)

Tactic:
dsimp [hammingDist]

Premises used: hammingDist
-- Module: Mathlib.InformationTheory.Hamming
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)
a : ∀ (a : ι), Membership.mem (γ := Finset ι) univ a → f a (x a) = f a (y a) → x a = y a
⊢ card.{u_2} (α := ι) {i : ι | ¬x i = y i} ≤ card.{u_2} (α := ι) {i : ι | ¬f i (x i) = f i (y i)}

Tactic:
gcongr
-- Module: Mathlib.InformationTheory.Hamming
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)
a : ι
h : Membership.mem (γ := Finset ι) univ a
⊢ f a (x a) = f a (y a) → x a = y a

Tactic:
@hf _ _ _
-- Module: Mathlib.InformationTheory.Hamming
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)
a : ι
h : Membership.mem (γ := Finset ι) univ a
⊢ f a (x a) = f a (y a) → x a = y a

Tactic:
exact @hf _ _ _
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → SMul.{u_1, u_3} α (β i)
k : α
x y : (i : ι) → β i
⊢ hammingDist (β := β) (k • x) (k • y) ≤ hammingDist (β := β) x y

Tactic:
hammingDist_comp_le_hammingDist fun i => (k • · : β i → β i)

Premises used: hammingDist_comp_le_hammingDist, HSMul.hSMul
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → SMul.{u_1, u_3} α (β i)
k : α
x y : (i : ι) → β i
hk : ∀ (i : ι), IsSMulRegular.{u_1, u_3} (β i) k
⊢ hammingDist (β := β) (k • x) (k • y) = hammingDist (β := β) x y

Tactic:
hammingDist_comp (fun i => (k • · : β i → β i)) hk

Premises used: hammingDist_comp, HSMul.hSMul
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingDist (β := β) x 0 = hammingNorm (β := β) x

Tactic:
rfl

Premises used: hammingNorm, 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 : (i : ι) → β i
rw : hammingDist (β := β) x 0 = hammingNorm (β := β) x
rw₁ rw₂ : hammingNorm (β := β) x = hammingNorm (β := β) x
⊢ hammingDist (β := β) 0 x = hammingNorm (β := β) x

Tactic:
rw [hammingDist_comm, hammingDist_zero_right]

Premises used: hammingDist_zero_right, hammingDist_comm
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ 0 ≤ hammingNorm (β := β) x

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
⊢ hammingNorm (β := β) 0 = 0

Tactic:
hammingDist_self _

Premises used: hammingNorm, hammingDist_self
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingNorm (β := β) x = 0 ↔ x = 0

Tactic:
hammingDist_eq_zero

Premises used: hammingNorm, hammingDist_eq_zero
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingNorm (β := β) x ≠ 0 ↔ x ≠ 0

Tactic:
hammingNorm_eq_zero.not

Premises used: Iff.not, hammingNorm_eq_zero
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ 0 < hammingNorm (β := β) x ↔ x ≠ 0

Tactic:
hammingDist_pos

Premises used: hammingNorm, hammingDist_pos
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingNorm (β := β) x < 1 ↔ x = 0

Tactic:
hammingDist_lt_one

Premises used: hammingNorm, hammingDist_lt_one
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
x : (i : ι) → β i
⊢ hammingNorm (β := β) x ≤ Fintype.card ι

Tactic:
hammingDist_le_card_fintype

Premises used: hammingNorm, hammingDist_le_card_fintype
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst_2 : (i : ι) → DecidableEq (γ i)
inst_3 : (i : ι) → Zero (β i)
inst_4 : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm (β := β) fun (i : ι) ↦ f i (x i)) ≤ hammingNorm (β := γ) x

Tactic:
simpa only [← hammingDist_zero_right, hf] using hammingDist_comp_le_hammingDist f (y := fun _ ↦ 0)

Premises used: hammingDist_zero_right, hammingDist_comp_le_hammingDist
-- Module: Mathlib.InformationTheory.Hamming
Goal:
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst_2 : (i : ι) → DecidableEq (γ i)
inst_3 : (i : ι) → Zero (β i)
inst_4 : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf₁ : ∀ (i : ι), Injective (f i)
hf₂ : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm (β := β) fun (i : ι) ↦ f i (x i)) = hammingNorm (β := γ) x

Tactic:
simpa only [← hammingDist_zero_right, hf₂] using hammingDist_comp f hf₁ (y := fun _ ↦ 0)

Premises used: hammingDist_comp, hammingDist_zero_right
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
inst_3 : Zero α
inst_4 : (i : ι) → SMulWithZero.{u_1, u_3} α (β i)
k : α
x : (i : ι) → β i
i : ι
simp_rw simp_rw₁ : HSMul.hSMul (β := β i) k 0 = 0
⊢ Eq.{u_3 + 1} (α := β i) ((fun (i : ι) (c : β i) ↦ k • c) i 0) 0

Tactic:
simp_rw [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.InformationTheory.Hamming
Goal:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → DecidableEq (β i)
inst_2 : (i : ι) → Zero (β i)
inst_3 : Zero α
inst_4 : (i : ι) → SMulWithZero.{u_1, u_3} α (β i)
k : α
hk : ∀ (i : ι), IsSMulRegular.{u_1, u_3} (β i) k
x : (i : ι) → β i
i : ι
simp_rw simp_rw₁ : HSMul.hSMul (β := β i) k 0 = 0
⊢ Eq.{u_3 + 1} (α := β i) ((fun (i : ι) (c : β i) ↦ k • c) i 0) 0

Tactic:
simp_rw [smul_zero]

Premises used: smul_zero