internlm/Lean-Github huggingface dataset:
Theorem: LoopProgram.ofLen_complete
Proof state before:
case succ.h₁
p✝ p : LoopProgram
x' : ℕ
this : len p + Nat.succ x' = len (loop { index := x' } p)
⊢ loop { index := x' } p ∈ ofLen (len (loop { index := x' } p))

case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
Tactic:
apply ofLen_complete
Proof state after:
case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
Theorem: LoopProgram.ofLen_complete
Proof state before:
case succ.h₂
p✝ p : LoopProgram
x' : ℕ
⊢ loop { index := Nat.succ x' } p ∈ extendLenOne (loop { index := x' } p)
Tactic:
simp [extendLenOne]
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ p : LoopProgram
h : len p = 0
⊢ loop { index := Nat.zero } p ∈ ofLen (0 + Nat.zero + 1)
Tactic:
exact False.elim $ Nat.ne_of_gt p.len_gt_zero h
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := Nat.zero } p ∈ ofLen (1 + Nat.zero + 1)
Tactic:
dsimp [ofLen, baseProgram]
Proof state after:
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    WellFounded.fix ofLen.proof_1
      (fun a a_1 =>
        (match (motive :=
            (x : ℕ) →
              ((y : ℕ) → (invImage (fun a => a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                Finset LoopProgram)
            a with
          | 0 => fun x => ∅
          | Nat.succ n => fun x =>
            Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                Finset.fold (fun x x_1 => x ∪ x_1) ∅
                  (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (x ↑x_1 ⋯) (x (n - ↑x_1) ⋯)))
                  (Finset.attach (Finset.range n)) ∪
              match n + 1 with
              | 0 => ∅
              | 1 => lenOne
              | 2 => Finset.image (loop { index := 0 }) lenOne
              | x => ∅)
          a_1)
      (1 + 1)
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    WellFounded.fix ofLen.proof_1
      (fun a a_1 =>
        (match (motive :=
            (x : ℕ) →
              ((y : ℕ) → (invImage (fun a => a) instWellFoundedRelation).1 y x → Finset LoopProgram) →
                Finset LoopProgram)
            a with
          | 0 => fun x => ∅
          | Nat.succ n => fun x =>
            Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (x n ⋯) ∪
                Finset.fold (fun x x_1 => x ∪ x_1) ∅
                  (fun x_1 => Finset.image (fun x => concat x.1 x.2) (Finset.product (x ↑x_1 ⋯) (x (n - ↑x_1) ⋯)))
                  (Finset.attach (Finset.range n)) ∪
              match n + 1 with
              | 0 => ∅
              | 1 => lenOne
              | 2 => Finset.image (loop { index := 0 }) lenOne
              | x => ∅)
          a_1)
      (1 + 1)
Tactic:
apply Finset.mem_union_right
Proof state after:
case h
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    match 1 + 1 with
    | 0 => ∅
    | 1 => lenOne
    | 2 => Finset.image (loop { index := 0 }) lenOne
    | x => ∅
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h
p✝ p : LoopProgram
h : len p = 1
⊢ loop { index := 0 } p ∈
    match 1 + 1 with
    | 0 => ∅
    | 1 => lenOne
    | 2 => Finset.image (loop { index := 0 }) lenOne
    | x => ∅
Tactic:
apply Finset.mem_image_of_mem
Proof state after:
case h.h
p✝ p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h.h
p✝ p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne
Tactic:
exact lenOne_complete _ h
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ ofLen (n + 1 + Nat.zero + 1)
Tactic:
apply ofLen_contains_extendLenOne_image
Proof state after:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (n + 1)

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (n + 1)

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram
Tactic:
rw [<- Nat.succ_eq_add_one, <- h]
Proof state after:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (len p)

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h₁
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ ?p ∈ ofLen (len p)

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram

case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne ?p

case p
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ LoopProgram
Tactic:
apply ofLen_complete
Proof state after:
case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne p
Theorem: LoopProgram.ofLen_complete
Proof state before:
case h₂
p✝ p : LoopProgram
n : ℕ
h : len p = Nat.succ n
⊢ loop { index := Nat.zero } p ∈ extendLenOne p
Tactic:
cases p <;> simp [extendLenOne]
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ p : LoopProgram
x' : ℕ
⊢ LoopProgram
Tactic:
exact loop (.mk x') p
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
p✝ p : LoopProgram
x' : ℕ
⊢ len p + Nat.succ x' = len (loop { index := x' } p)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoopProgram.ofLen_complete
Proof state before:
p a b : LoopProgram
⊢ concat a b ∈ ofLen (len (concat a b))
Tactic:
simp [len, ofLen]
Proof state after:
p a b : LoopProgram
⊢ concat a b ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (len a + len b)) ∨
    concat a b ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (len a + len b - ↑x))))
          (Finset.attach (Finset.range (len a + len b))) ∨
      concat a b ∈ baseProgram (len a + len b + 1)
Theorem: LoopProgram.ofLen_complete
Proof state before:
p a b : LoopProgram
⊢ concat a b ∈ Finset.fold (fun a b => a ∪ b) ∅ extendLenOne (ofLen (len a + len b)) ∨
    concat a b ∈
        Finset.fold (fun x x_1 => x ∪ x_1) ∅
          (fun x => Finset.image (fun x => concat x.1 x.2) (Finset.product (ofLen ↑x) (ofLen (len a + len b - ↑x))))
          (Finset.attach (Finset.range (len a + len b))) ∨
      concat a b ∈ baseProgram (len a + len b + 1)
Tactic:
refine' .inr $ .inl (Finset.mem_fold_union_iff.mpr ⟨⟨a.len, _⟩, _⟩)
Proof state after:
case refine'_1
p a b : LoopProgram
⊢ len a ∈ Finset.range (len a + len b)

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ?refine'_1 } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ?refine'_1 })
          (ofLen (len a + len b - ↑{ val := len a, property := ?refine'_1 })))
Theorem: LoopProgram.ofLen_complete
Proof state before:
case refine'_1
p a b : LoopProgram
⊢ len a ∈ Finset.range (len a + len b)

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ?refine'_1 } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ?refine'_1 })
          (ofLen (len a + len b - ↑{ val := len a, property := ?refine'_1 })))
Tactic:
rw [Finset.mem_range]
Proof state after:
case refine'_1
p a b : LoopProgram
⊢ len a < len a + len b

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))
Theorem: LoopProgram.ofLen_complete
Proof state before:
case refine'_1
p a b : LoopProgram
⊢ len a < len a + len b

case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))
Tactic:
simp [len_gt_zero]
Proof state after:
case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))
Theorem: LoopProgram.ofLen_complete
Proof state before:
case refine'_2
p a b : LoopProgram
⊢ { val := len a, property := ⋯ } ∈ Finset.attach (Finset.range (len a + len b)) ∧
    concat a b ∈
      Finset.image (fun x => concat x.1 x.2)
        (Finset.product (ofLen ↑{ val := len a, property := ⋯ })
          (ofLen (len a + len b - ↑{ val := len a, property := ⋯ })))
Tactic:
simp
Proof state after:
case refine'_2
p a b : LoopProgram
⊢ (a, b) ∈ Finset.product (ofLen (len a)) (ofLen (len b))
Theorem: LoopProgram.ofLen_complete
Proof state before:
case refine'_2
p a b : LoopProgram
⊢ (a, b) ∈ Finset.product (ofLen (len a)) (ofLen (len b))
Tactic:
apply Finset.mem_product.mpr
Proof state after:
case refine'_2
p a b : LoopProgram
⊢ (a, b).1 ∈ ofLen (len a) ∧ (a, b).2 ∈ ofLen (len b)
Theorem: LoopProgram.ofLen_complete
Proof state before:
case refine'_2
p a b : LoopProgram
⊢ (a, b).1 ∈ ofLen (len a) ∧ (a, b).2 ∈ ofLen (len b)
Tactic:
exact ⟨ofLen_complete _, ofLen_complete _⟩
Proof state after:
no goals
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
⊢ ∀ (p : LoopProgram), toFunction p ≠ diagonal
Tactic:
intro p h
Proof state after:
p : LoopProgram
h : toFunction p = diagonal
⊢ False
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
p : LoopProgram
h : toFunction p = diagonal
⊢ False
Tactic:
apply Nat.ne_of_lt
Proof state after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a = ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ

case b
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a = ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ

case b
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ
Tactic:
. show p.toFunction p.len < diagonal p.len
  unfold diagonal
  rw [Nat.lt_add_one_iff, Finset.le_fold_max]
  apply Or.inr
  exists p; constructor
  apply ofLen_complete
  rfl
Proof state after:
case a
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) = diagonal (len p)
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case a
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) = diagonal (len p)
Tactic:
. apply congrFun
  assumption
Proof state after:
no goals
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b
Tactic:
show p.toFunction p.len < diagonal p.len
Proof state after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < diagonal (len p)
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < diagonal (len p)
Tactic:
unfold diagonal
Proof state after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < Finset.fold max 0 (fun p_1 => toFunction p_1 (len p)) (ofLen (len p)) + 1
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < Finset.fold max 0 (fun p_1 => toFunction p_1 (len p)) (ofLen (len p)) + 1
Tactic:
rw [Nat.lt_add_one_iff, Finset.le_fold_max]
Proof state after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ 0 ∨ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ 0 ∨ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
Tactic:
apply Or.inr
Proof state after:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
Tactic:
exists p
Proof state after:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p) ∧ toFunction p (len p) ≤ toFunction p (len p)
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p) ∧ toFunction p (len p) ≤ toFunction p (len p)
Tactic:
constructor
Proof state after:
case h.h.left
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p)

case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h.h.left
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p)

case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)
Tactic:
apply ofLen_complete
Proof state after:
case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)
Tactic:
rfl
Proof state after:
no goals
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case a
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) = diagonal (len p)
Tactic:
apply congrFun
Proof state after:
case a.h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p = diagonal
Theorem: LoopProgram.diagonal_is_not_loop_computable
Proof state before:
case a.h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p = diagonal
Tactic:
assumption
Proof state after:
no goals
Theorem: FinDenumerable.encode_fin_eq_encode
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ ∀ (a : α), ↑(encode_fin a) = Encodable.encode a
Tactic:
simp [encode_fin]
Proof state after:
no goals
Theorem: FinDenumerable.encode_fin_injective
Proof state before:
α : Type u_1
inst : FinDenumerable α
⊢ Function.Injective encode_fin
Tactic:
intro x y
Proof state after:
α : Type u_1
inst : FinDenumerable α
x y : α
⊢ encode_fin x = encode_fin y → x = y
Theorem: FinDenumerable.encode_fin_injective
Proof state before:
α : Type u_1
inst : FinDenumerable α
x y : α
⊢ encode_fin x = encode_fin y → x = y
Tactic:
simp [Fin.ext_iff, encode_fin]
Proof state after:
no goals
Theorem: FinDenumerable.decode_partial_inv
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a ∈ Encodable.decode ↑n, Encodable.encode a = ↑n
Tactic:
have ⟨ a, pa, _ ⟩  := encode_fin_bijective.existsUnique n
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ ∃ a ∈ Encodable.decode ↑n, Encodable.encode a = ↑n
Theorem: FinDenumerable.decode_partial_inv
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ ∃ a ∈ Encodable.decode ↑n, Encodable.encode a = ↑n
Tactic:
exists a
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n
Theorem: FinDenumerable.decode_partial_inv
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
pa : (fun a => encode_fin a = n) a
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n
Tactic:
simp [Fin.ext_iff, encode_fin] at pa
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n
Theorem: FinDenumerable.decode_partial_inv
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n
Tactic:
simp [pa]
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ Encodable.decode ↑n = some a
Theorem: FinDenumerable.decode_partial_inv
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a : α
right✝ : ∀ (y : α), (fun a => encode_fin a = n) y → y = a
pa : Encodable.encode a = ↑n
⊢ Encodable.decode ↑n = some a
Tactic:
simp [<- pa]
Proof state after:
no goals
Theorem: FinDenumerable.decode_fin_is_some
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Option.isSome (Encodable.decode ↑n) = true
Tactic:
apply Option.isSome_iff_exists.2
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a, Encodable.decode ↑n = some a
Theorem: FinDenumerable.decode_fin_is_some
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∃ a, Encodable.decode ↑n = some a
Tactic:
apply (decode_partial_inv n).imp
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∀ (a : α), a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n → Encodable.decode ↑n = some a
Theorem: FinDenumerable.decode_fin_is_some
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ ∀ (a : α), a ∈ Encodable.decode ↑n ∧ Encodable.encode a = ↑n → Encodable.decode ↑n = some a
Tactic:
intro _ h
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a✝ : α
h : a✝ ∈ Encodable.decode ↑n ∧ Encodable.encode a✝ = ↑n
⊢ Encodable.decode ↑n = some a✝
Theorem: FinDenumerable.decode_fin_is_some
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
a✝ : α
h : a✝ ∈ Encodable.decode ↑n ∧ Encodable.encode a✝ = ↑n
⊢ Encodable.decode ↑n = some a✝
Tactic:
exact h.1
Proof state after:
no goals
Theorem: FinDenumerable.decode_fin_eq_option_get
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Option.get (Encodable.decode ↑n) ⋯ = decode_fin n
Tactic:
simp [decode_fin]
Proof state after:
no goals
Theorem: FinDenumerable.fin_decode_eq_decode₂
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode ↑n = Encodable.decode₂ α ↑n
Tactic:
rw [← Option.some_get (decode_fin_is_some n)]
Proof state after:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ some (Option.get (Encodable.decode ↑n) ⋯) = Encodable.decode₂ α ↑n
Theorem: FinDenumerable.fin_decode_eq_decode₂
Proof state before:
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ some (Option.get (Encodable.decode ↑n) ⋯) = Encodable.decode₂ α ↑n
Tactic:
apply Eq.symm
Proof state after:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode₂ α ↑n = some (Option.get (Encodable.decode ↑n) ⋯)
Theorem: FinDenumerable.fin_decode_eq_decode₂
Proof state before:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.decode₂ α ↑n = some (Option.get (Encodable.decode ↑n) ⋯)
Tactic:
rw [Encodable.decode₂_is_partial_inv]
Proof state after:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Theorem: FinDenumerable.fin_decode_eq_decode₂
Proof state before:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
have ⟨ _, h ⟩ := fin_preimage_exists n
Proof state after:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
w✝ : α
h : Encodable.encode w✝ = ↑n
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Theorem: FinDenumerable.fin_decode_eq_decode₂
Proof state before:
case h
α : Type u_1
inst : FinDenumerable α
n : Fin (Fintype.card α)
w✝ : α
h : Encodable.encode w✝ = ↑n
⊢ Encodable.encode (Option.get (Encodable.decode ↑n) ⋯) = ↑n
Tactic:
simp [<- h]
Proof state after:
no goals
Theorem: FinDenumerable.decode_fin_inj
Proof state before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₁ : a = decode_fin n
h₂ : b = decode_fin m
⊢ a = b ↔ n = m
Tactic:
have ⟨ _, p₁ ⟩ := fin_preimage_exists n
Proof state after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₁ : a = decode_fin n
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
⊢ a = b ↔ n = m
Theorem: FinDenumerable.decode_fin_inj
Proof state before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₁ : a = decode_fin n
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
⊢ a = b ↔ n = m
Tactic:
simp [FinDenumerable.decode_fin, <- p₁] at h₁
Proof state after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
h₁ : a = w✝
⊢ a = b ↔ n = m
Theorem: FinDenumerable.decode_fin_inj
Proof state before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝ : α
p₁ : Encodable.encode w✝ = ↑n
h₁ : a = w✝
⊢ a = b ↔ n = m
Tactic:
have ⟨ _, p₂ ⟩ := fin_preimage_exists m
Proof state after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
⊢ a = b ↔ n = m
Theorem: FinDenumerable.decode_fin_inj
Proof state before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
h₂ : b = decode_fin m
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
⊢ a = b ↔ n = m
Tactic:
simp [FinDenumerable.decode_fin, <- p₂] at h₂
Proof state after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ a = b ↔ n = m
Theorem: FinDenumerable.decode_fin_inj
Proof state before:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ a = b ↔ n = m
Tactic:
rw [h₁, h₂, Fin.ext_iff, ← p₁, ← p₂]
Proof state after:
α : Type u_1
a b : α
inst : FinDenumerable α
n m : Fin (Fintype.card α)
w✝¹ : α
p₁ : Encodable.encode w✝¹ = ↑n
h₁ : a = w✝¹
w✝ : α
p₂ : Encodable.encode w✝ = ↑m
h₂ : b = w✝
⊢ w✝¹ = w✝ ↔ Encodable.encode w✝¹ = Encodable.encode w✝