internlm/Lean-Github huggingface dataset:
Theorem: LO.Gentzen.consistent_theory_iff_consistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
consis : System.Consistent 𝓣
⊢ System.theory 𝓣 ⊬! ⊥
Tactic:
rintro h
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
⊢ False
Theorem: LO.Gentzen.consistent_theory_iff_consistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
⊢ False
Tactic:
have : System.Inconsistent 𝓣 := System.inconsistent_iff_provable_bot.mpr <| System.StrongCut.cut! (by simp) h
Proof state after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
this : System.Inconsistent 𝓣
⊢ False
Theorem: LO.Gentzen.consistent_theory_iff_consistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
this : System.Inconsistent 𝓣
⊢ False
Tactic:
exact System.not_inconsistent_iff_consistent.mpr consis this
Proof state after:
no goals
Theorem: LO.Gentzen.consistent_theory_iff_consistent
Proof state before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
consis : System.Consistent 𝓣
h : System.theory 𝓣 ⊢! ⊥
⊢ 𝓣 ⊢!* Collection.set (System.theory 𝓣)
Tactic:
simp
Proof state after:
no goals
Theorem: List.mem_range2_iff
Proof state before:
n m i j : ℕ
⊢ (i, j) ∈ range2 n m ↔ i < n ∧ j < m
Tactic:
simp[range2, seq_eq_bind]
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivFinArrow_eq
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : ι → α
⊢ fintypeArrowEquivFinArrow f = fun i => f (fintypeEquivFin.symm i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivFinArrow_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : ι → α
i : Fin (Fintype.card ι)
⊢ fintypeArrowEquivFinArrow f i = f (fintypeEquivFin.symm i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivFinArrow_symm_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
i : ι
v : Fin (Fintype.card ι) → α
⊢ fintypeArrowEquivFinArrow.symm v i = v (fintypeEquivFin i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivFinArrow'_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
k : ℕ
hk : Fintype.card ι = k
f : ι → α
i : Fin k
⊢ (fintypeArrowEquivFinArrow' hk) f i = f (fintypeEquivFin.symm (Fin.cast ⋯ i))
Tactic:
rcases hk with rfl
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : ι → α
i : Fin (Fintype.card ι)
⊢ (fintypeArrowEquivFinArrow' ⋯) f i = f (fintypeEquivFin.symm (Fin.cast ⋯ i))
Theorem: Encodable.fintypeArrowEquivFinArrow'_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : ι → α
i : Fin (Fintype.card ι)
⊢ (fintypeArrowEquivFinArrow' ⋯) f i = f (fintypeEquivFin.symm (Fin.cast ⋯ i))
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivFinArrow'_symm_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
i : ι
k : ℕ
hk : Fintype.card ι = k
v : Fin k → α
⊢ (fintypeArrowEquivFinArrow' hk).symm v i = v (Fin.cast hk (fintypeEquivFin i))
Tactic:
rcases hk with rfl
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
i : ι
v : Fin (Fintype.card ι) → α
⊢ (fintypeArrowEquivFinArrow' ⋯).symm v i = v (Fin.cast ⋯ (fintypeEquivFin i))
Theorem: Encodable.fintypeArrowEquivFinArrow'_symm_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
i : ι
v : Fin (Fintype.card ι) → α
⊢ (fintypeArrowEquivFinArrow' ⋯).symm v i = v (Fin.cast ⋯ (fintypeEquivFin i))
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.cast_fintypeEquivFin_fin
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ Fin.cast ⋯ (fintypeEquivFin i) = i
Tactic:
ext
Proof state after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ ↑(Fin.cast ⋯ (fintypeEquivFin i)) = ↑i
Theorem: Encodable.cast_fintypeEquivFin_fin
Proof state before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ ↑(Fin.cast ⋯ (fintypeEquivFin i)) = ↑i
Tactic:
simp [Encodable.fintypeEquivFin, Fin.cast_eq_cast',
  Fin.encodable, List.Nodup.getEquivOfForallMemList,
  Encodable.sortedUniv, Encodable.encode']
Proof state after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ List.indexOf i (Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ) = ↑i
Theorem: Encodable.cast_fintypeEquivFin_fin
Proof state before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ List.indexOf i (Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ) = ↑i
Tactic:
convert List.indexOf_finRange i
Proof state after:
case h.e'_2.h.e'_4
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ = List.finRange k
Theorem: Encodable.cast_fintypeEquivFin_fin
Proof state before:
case h.e'_2.h.e'_4
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ Finset.sort (encode ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ = List.finRange k
Tactic:
exact Fin.sort_univ _
Proof state after:
no goals
Theorem: Encodable.fintypeEquivFin_false
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin false = 0
Tactic:
simp [fintypeEquivFin]
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ cast ⋯ ((List.Nodup.getEquivOfForallMemList (sortedUniv Bool) ⋯ ⋯).symm false) = 0
Theorem: Encodable.fintypeEquivFin_false
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ cast ⋯ ((List.Nodup.getEquivOfForallMemList (sortedUniv Bool) ⋯ ⋯).symm false) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeEquivFin_true
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin true = 1
Tactic:
simp [fintypeEquivFin]
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ cast ⋯ ((List.Nodup.getEquivOfForallMemList (sortedUniv Bool) ⋯ ⋯).symm true) = 1
Theorem: Encodable.fintypeEquivFin_true
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ cast ⋯ ((List.Nodup.getEquivOfForallMemList (sortedUniv Bool) ⋯ ⋯).symm true) = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeEquivFin_symm_zero
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin.symm 0 = false
Tactic:
simp [fintypeEquivFin]
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ (sortedUniv Bool).get (cast ⋯ 0) = false
Theorem: Encodable.fintypeEquivFin_symm_zero
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ (sortedUniv Bool).get (cast ⋯ 0) = false
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeEquivFin_symm_one
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin.symm 1 = true
Tactic:
simp [fintypeEquivFin]
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ (sortedUniv Bool).get (cast ⋯ 1) = true
Theorem: Encodable.fintypeEquivFin_symm_one
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ (sortedUniv Bool).get (cast ⋯ 1) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeEquivFin_symm_cast_fin
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
⊢ fintypeEquivFin.symm (Fin.cast ⋯ i) = i
Tactic:
have := congr_arg (fun j => fintypeEquivFin.symm (j.cast (Fintype.card_fin _).symm)) (cast_fintypeEquivFin_fin i)
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
this :
  (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) (Fin.cast ⋯ (fintypeEquivFin i)) =
    (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) i
⊢ fintypeEquivFin.symm (Fin.cast ⋯ i) = i
Theorem: Encodable.fintypeEquivFin_symm_cast_fin
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
k : ℕ
i : Fin k
this :
  (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) (Fin.cast ⋯ (fintypeEquivFin i)) =
    (fun j => fintypeEquivFin.symm (Fin.cast ⋯ j)) i
⊢ fintypeEquivFin.symm (Fin.cast ⋯ i) = i
Tactic:
simpa[-cast_fintypeEquivFin_fin] using this.symm
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivFinArrow'_symm_app_fin_arrow
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
k : ℕ
hk : Fintype.card (Fin k) = k
v : Fin k → α
⊢ (fintypeArrowEquivFinArrow' hk).symm v = v
Tactic:
funext i
Proof state after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
k : ℕ
hk : Fintype.card (Fin k) = k
v : Fin k → α
i : Fin k
⊢ (fintypeArrowEquivFinArrow' hk).symm v i = v i
Theorem: Encodable.fintypeArrowEquivFinArrow'_symm_app_fin_arrow
Proof state before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
k : ℕ
hk : Fintype.card (Fin k) = k
v : Fin k → α
i : Fin k
⊢ (fintypeArrowEquivFinArrow' hk).symm v i = v i
Tactic:
simp[hk]
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivVector_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
i : Fin (Fintype.card ι)
f : ι → α
⊢ (fintypeArrowEquivVector f).get i = f (fintypeEquivFin.symm i)
Tactic:
simp[fintypeArrowEquivVector, Equiv.vectorEquivFin]
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivVector_symm_app
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
i : ι
v : Vector α (Fintype.card ι)
⊢ fintypeArrowEquivVector.symm v i = v.get (fintypeEquivFin i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Encodable.fintypeArrowEquivFinArrow_fintypeEquivFin
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : Fin (Fintype.card ι) → α
⊢ (fintypeArrowEquivFinArrow fun i => f (fintypeEquivFin i)) = f
Tactic:
funext i
Proof state after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : Fin (Fintype.card ι) → α
i : Fin (Fintype.card ι)
⊢ fintypeArrowEquivFinArrow (fun i => f (fintypeEquivFin i)) i = f i
Theorem: Encodable.fintypeArrowEquivFinArrow_fintypeEquivFin
Proof state before:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Sort u_2
f : Fin (Fintype.card ι) → α
i : Fin (Fintype.card ι)
⊢ fintypeArrowEquivFinArrow (fun i => f (fintypeEquivFin i)) i = f i
Tactic:
simp
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ toFinArrowOpt f = none ↔ ∃ i, f i = none
Tactic:
simp[toFinArrowOpt, fintypeArrowEquivFinArrow]
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) ↔ ∃ i, f i = none
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) ↔ ∃ i, f i = none
Tactic:
constructor
Proof state after:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) → ∃ i, f i = none

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) → ∃ i, f i = none

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
{ rintro ⟨i, hi⟩; exact ⟨_, hi⟩ }
Proof state after:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
{ rintro ⟨i, hi⟩; exact ⟨fintypeEquivFin i, by simp[hi]⟩  }
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f (fintypeEquivFin.symm i) = none) → ∃ i, f i = none
Tactic:
rintro ⟨i, hi⟩
Proof state after:
case mp.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : Fin (Fintype.card ι)
hi : f (fintypeEquivFin.symm i) = none
⊢ ∃ i, f i = none
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
case mp.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : Fin (Fintype.card ι)
hi : f (fintypeEquivFin.symm i) = none
⊢ ∃ i, f i = none
Tactic:
exact ⟨_, hi⟩
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
⊢ (∃ i, f i = none) → ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
rintro ⟨i, hi⟩
Proof state after:
case mpr.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : ι
hi : f i = none
⊢ ∃ i, f (fintypeEquivFin.symm i) = none
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
case mpr.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : ι
hi : f i = none
⊢ ∃ i, f (fintypeEquivFin.symm i) = none
Tactic:
exact ⟨fintypeEquivFin i, by simp[hi]⟩
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_none_iff
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
i : ι
hi : f i = none
⊢ f (fintypeEquivFin.symm (fintypeEquivFin i)) = none
Tactic:
simp[hi]
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ toFinArrowOpt f = some g ↔ ∀ (i : ι), f i = some (g i)
Tactic:
simp[toFinArrowOpt, fintypeArrowEquivFinArrow]
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) ↔
    ∀ (i : ι), f i = some (g i)
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) ↔
    ∀ (i : ι), f i = some (g i)
Tactic:
constructor
Proof state after:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) →
    ∀ (i : ι), f i = some (g i)

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) →
    ∀ (i : ι), f i = some (g i)

case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
{ rintro ⟨a, ha, rfl⟩; simp; intro i
  simpa using ha (fintypeEquivFin i) }
Proof state after:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
{ intro hf; exact ⟨fun i => g (fintypeEquivFin.symm i), by { simp[hf]; funext i; simp }⟩ }
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mp
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g) →
    ∀ (i : ι), f i = some (g i)
Tactic:
rintro ⟨a, ha, rfl⟩
Proof state after:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a i)
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a i)
Tactic:
simp
Proof state after:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some (a (fintypeEquivFin i))
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
⊢ ∀ (i : ι), f i = some (a (fintypeEquivFin i))
Tactic:
intro i
Proof state after:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
i : ι
⊢ f i = some (a (fintypeEquivFin i))
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mp.intro.intro
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
a : Fin (Fintype.card ι) → α
ha : ∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)
i : ι
⊢ f i = some (a (fintypeEquivFin i))
Tactic:
simpa using ha (fintypeEquivFin i)
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
⊢ (∀ (i : ι), f i = some (g i)) →
    ∃ a,
      (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
        (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
intro hf
Proof state after:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ∃ a,
    (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
      (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
case mpr
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ∃ a,
    (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some (a i)) ∧
      (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) a = g
Tactic:
exact ⟨fun i => g (fintypeEquivFin.symm i), by { simp[hf]; funext i; simp }⟩
Proof state after:
no goals
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ (∀ (i : Fin (Fintype.card ι)), f (fintypeEquivFin.symm i) = some ((fun i => g (fintypeEquivFin.symm i)) i)) ∧
    ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) fun i => g (fintypeEquivFin.symm i)) = g
Tactic:
simp[hf]
Proof state after:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) fun i => g (fintypeEquivFin.symm i)) = g
Theorem: Encodable.toFinArrowOpt_eq_some_iff
Proof state before:
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
⊢ ((fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) fun i => g (fintypeEquivFin.symm i)) = g
Tactic:
funext i
Proof state after:
case h
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
α : Type u_2
f : ι → Option α
g : ι → α
hf : ∀ (i : ι), f i = some (g i)
i : ι
⊢ (fintypeEquivFin.symm.arrowCongr (Equiv.refl α)) (fun i => g (fintypeEquivFin.symm i)) i = g i