internlm/Lean-Github huggingface dataset:
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case h.a.mp
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
hite : (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one
⊢ x ∈ ↑pw
Tactic:
split_ifs at hite with hi
Proof state after:
case pos
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
hite : binary.one = binary.one
⊢ x ∈ ↑pw
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case pos
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
hite : binary.one = binary.one
⊢ x ∈ ↑pw
Tactic:
simp only [Set.powerset_univ, set_coe_cast] at hi
Proof state after:
case pos
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
hite : binary.one = binary.one
hi : x ∈ ↑pw
⊢ x ∈ ↑pw
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case pos
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
hite : binary.one = binary.one
hi : x ∈ ↑pw
⊢ x ∈ ↑pw
Tactic:
exact hi
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case h.a.mpr
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
⊢ x ∈ ↑pw → (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one
Tactic:
intro el
Proof state after:
case h.a.mpr
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
⊢ (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case h.a.mpr
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
⊢ (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one
Tactic:
split_ifs with hi
Proof state after:
case pos
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ binary.one = binary.one

case neg
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
hi : x ∉ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ False
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case pos
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ binary.one = binary.one
Tactic:
rfl
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case neg
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
hi : x ∉ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ False
Tactic:
simp only [Set.powerset_univ, set_coe_cast] at hi
Proof state after:
case neg
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
hi : x ∉ ↑pw
⊢ False
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
case neg
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
hi : x ∉ ↑pw
⊢ False
Tactic:
exact hi el
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat
Proof state before:
⊢ Cardinal.mk ↑(𝒫 Set.univ) = Cardinal.mk ↑(𝒫 Set.univ)
Tactic:
simp only [Cardinal.mk_powerset,
           Cardinal.mk_univ,
           Cardinal.mk_eq_aleph0,
           Cardinal.two_power_aleph0]
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
m n q p : ℕ
h : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ m = p ∧ n = q
Tactic:
apply_fun Nat.factorization at h
Proof state after:
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ m = p ∧ n = q
Tactic:
rw [Nat.factorization_mul, Nat.factorization_mul] at h
Proof state after:
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p) + Nat.factorization (3 ^ q)
⊢ m = p ∧ n = q

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ p ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ q ≠ 0

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ m ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ n ≠ 0
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ p ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ q ≠ 0

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ m ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ n ≠ 0
Tactic:
all_goals positivity
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p) + Nat.factorization (3 ^ q)
⊢ m = p ∧ n = q
Tactic:
simp_rw [Nat.factorization_pow] at h
Proof state after:
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p ∧ n = q
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p ∧ n = q
Tactic:
constructor
Proof state after:
case left
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p

case right
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ n = q
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case left
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p
Tactic:
replace h := FunLike.congr_fun h 2
Proof state after:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
⊢ m = p
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
⊢ m = p
Tactic:
have : ¬ 2 ∣ 3 := by norm_num
Proof state after:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
this : ¬2 ∣ 3
⊢ m = p
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
this : ¬2 ∣ 3
⊢ m = p
Tactic:
simp_rw [Finsupp.add_apply, Finsupp.smul_apply, Nat.prime_two.factorization_self,
  nsmul_one, Nat.factorization_eq_zero_of_not_dvd this, smul_zero, add_zero] at h
Proof state after:
case left
m n q p : ℕ
this : ¬2 ∣ 3
h : ↑m = ↑p
⊢ m = p
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case left
m n q p : ℕ
this : ¬2 ∣ 3
h : ↑m = ↑p
⊢ m = p
Tactic:
exact h
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
⊢ ¬2 ∣ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case right
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ n = q
Tactic:
replace h := FunLike.congr_fun h 3
Proof state after:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ n = q
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ n = q
Tactic:
have : ¬ 3 ∣ 2 := Nat.not_dvd_of_pos_of_lt (by simp) (by simp)
Proof state after:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
this : ¬3 ∣ 2
⊢ n = q
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
this : ¬3 ∣ 2
⊢ n = q
Tactic:
simp_rw [Finsupp.add_apply, Finsupp.smul_apply, Nat.prime_three.factorization_self,
  nsmul_one, Nat.factorization_eq_zero_of_not_dvd this, smul_zero, zero_add] at h
Proof state after:
case right
m n q p : ℕ
this : ¬3 ∣ 2
h : ↑n = ↑q
⊢ n = q
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case right
m n q p : ℕ
this : ¬3 ∣ 2
h : ↑n = ↑q
⊢ n = q
Tactic:
exact h
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ 2 < 3
Tactic:
simp
Proof state after:
no goals
Theorem: two_pow_three_pow_unique_factorization
Proof state before:
case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ n ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
⊢ ∃ fg, Function.Bijective fg
Tactic:
let f : (𝒫 (Set.univ : Set (ℕ × ℕ))) → (𝒫 (Set.univ : Set ℕ)) := by
  intro a_set_of_nxn
  exact {
    val := {2^x.1 * 3^x.2 | x ∈ a_set_of_nxn.val}
    property := by simp only [Set.powerset_univ, Set.mem_univ]
  }
Proof state after:
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
⊢ ∃ fg, Function.Bijective fg
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
hf : Function.Injective f
⊢ ∃ fg, Function.Bijective fg
Tactic:
let g : (𝒫 (Set.univ : Set ℕ)) → (𝒫 (Set.univ : Set (ℕ × ℕ))) := by
  intro a_set_of_n
  have a_set_of_nxn : Set (ℕ × ℕ) := a_set_of_n.val ×ˢ a_set_of_n.val
  exact { val := a_set_of_nxn, property := by simp }
Proof state after:
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
hf : Function.Injective f
g : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_n =>
    let_fun a_set_of_nxn := ↑a_set_of_n ×ˢ ↑a_set_of_n;
    { val := a_set_of_nxn, property := (_ : a_set_of_nxn ∈ 𝒫 Set.univ) }
⊢ ∃ fg, Function.Bijective fg
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
hf : Function.Injective f
g : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_n =>
    let_fun a_set_of_nxn := ↑a_set_of_n ×ˢ ↑a_set_of_n;
    { val := a_set_of_nxn, property := (_ : a_set_of_nxn ∈ 𝒫 Set.univ) }
hg : Function.Injective g
⊢ ∃ fg, Function.Bijective fg
Tactic:
exact Function.Embedding.schroeder_bernstein hf hg
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
⊢ ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ)
Tactic:
intro a_set_of_nxn
Proof state after:
a_set_of_nxn : ↑(𝒫 Set.univ)
⊢ ↑(𝒫 Set.univ)
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
a_set_of_nxn : ↑(𝒫 Set.univ)
⊢ ↑(𝒫 Set.univ)
Tactic:
exact {
  val := {2^x.1 * 3^x.2 | x ∈ a_set_of_nxn.val}
  property := by simp only [Set.powerset_univ, Set.mem_univ]
}
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
a_set_of_nxn : ↑(𝒫 Set.univ)
⊢ {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ
Tactic:
simp only [Set.powerset_univ, Set.mem_univ]
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
⊢ Function.Injective f
Tactic:
rintro ⟨p, _⟩ ⟨q, _⟩ heq
Proof state after:
case mk.mk
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
p : Set (ℕ × ℕ)
property✝¹ : p ∈ 𝒫 Set.univ
q : Set (ℕ × ℕ)
property✝ : q ∈ 𝒫 Set.univ
heq : f { val := p, property := property✝¹ } = f { val := q, property := property✝ }
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
p : Set (ℕ × ℕ)
property✝¹ : p ∈ 𝒫 Set.univ
q : Set (ℕ × ℕ)
property✝ : q ∈ 𝒫 Set.univ
heq : f { val := p, property := property✝¹ } = f { val := q, property := property✝ }
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }
Tactic:
simp only [f, Prod.exists, Subtype.mk.injEq, Set.ext_iff, Set.mem_setOf_eq] at heq
Proof state after:
case mk.mk
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
p : Set (ℕ × ℕ)
property✝¹ : p ∈ 𝒫 Set.univ
q : Set (ℕ × ℕ)
property✝ : q ∈ 𝒫 Set.univ
heq : ∀ (x : ℕ), (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = x) ↔ ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = x
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }