internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    (toList c).all f = true
Tactic:
simp_rw [List.all_eq_true, ← perm.mem_iff]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
perm : L.Perm (toList c)
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Tactic:
clear perm c
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          f' x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Tactic:
subst hf'
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          (fun x x => if f x = true then Except.ok () else Except.error ()) x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldl
        (fun acc x => do
          let x_1 ← acc
          (fun x x => if f x = true then Except.ok () else Except.error ()) x_1 x)
        (pure ()) L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Tactic:
rw [← List.foldlM_eq_foldl]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
L : List τ
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () L =
      Except.ok () ↔
    ∀ x ∈ L, f x = true
Tactic:
induction L with
| nil => simp_all [pure, Except.pure]
| cons hd tl ih =>
  simp [bind, Except.bind]
  by_cases f hd = true <;> simp_all
Proof state after:
no goals
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false) =
    (toList c).all f
Tactic:
rw [eq_comm]
Proof state after:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (toList c).all f =
    match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
⊢ (toList c).all f =
    match foldM c f' () with
    | Except.ok PUnit.unit => true
    | Except.error PUnit.unit => false
Tactic:
split
Proof state after:
case h_1
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).all f = true

case h_2
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f = false
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
case h_1
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.ok PUnit.unit
⊢ (toList c).all f = true
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
case h_2
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f = false
Tactic:
rw [Bool.eq_false_iff]
Proof state after:
case h_2
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f ≠ true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
case h_2
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
c : C
f' : Unit → τ → Except Unit Unit
hf' : (fun x x => if f x = true then Except.ok () else Except.error ()) = f'
this : foldM c f' () = Except.ok () ↔ (toList c).all f = true
x✝ : Except Unit Unit
heq✝ : foldM c f' () = Except.error PUnit.unit
⊢ (toList c).all f ≠ true
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
case nil
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () [] =
      Except.ok () ↔
    ∀ x ∈ [], f x = true
Tactic:
simp_all [pure, Except.pure]
Proof state after:
no goals
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
case cons
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () tl =
      Except.ok () ↔
    ∀ x ∈ tl, f x = true
⊢ List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () (hd :: tl) =
      Except.ok () ↔
    ∀ x ∈ hd :: tl, f x = true
Tactic:
simp [bind, Except.bind]
Proof state after:
case cons
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () tl =
      Except.ok () ↔
    ∀ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.ok () else Except.error () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.ok () else Except.error ()) v tl) =
      Except.ok () ↔
    f hd = true ∧ ∀ a ∈ tl, f a = true
Theorem: LeanColls.Fold.all_eq_all_toList
Proof state before:
case cons
C : Type u_1
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
inst✝¹ : LeanColls.ToList C τ
inst✝ : ToList C τ
f : τ → Bool
hd : τ
tl : List τ
ih :
  List.foldlM (fun x x_1 => (fun x x => if f x = true then Except.ok () else Except.error ()) x x_1) () tl =
      Except.ok () ↔
    ∀ x ∈ tl, f x = true
⊢ (match if f hd = true then Except.ok () else Except.error () with
      | Except.error err => Except.error err
      | Except.ok v => List.foldlM (fun x x => if f x = true then Except.ok () else Except.error ()) v tl) =
      Except.ok () ↔
    f hd = true ∧ ∀ a ∈ tl, f a = true
Tactic:
by_cases f hd = true <;> simp_all
Proof state after:
no goals
Theorem: LeanColls.Fold.any_iff_exists
Proof state before:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ any f c = true ↔ ∃ x ∈ c, f x = true
Tactic:
rw [any_eq_any_toList]
Proof state after:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ (toList c).any f = true ↔ ∃ x ∈ c, f x = true
Theorem: LeanColls.Fold.any_iff_exists
Proof state before:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ (toList c).any f = true ↔ ∃ x ∈ c, f x = true
Tactic:
simp [Mem.ToList.mem_iff_mem_toList]
Proof state after:
no goals
Theorem: LeanColls.Fold.all_iff_exists
Proof state before:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ all f c = true ↔ ∀ x ∈ c, f x = true
Tactic:
rw [all_eq_all_toList]
Proof state after:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ (toList c).all f = true ↔ ∀ x ∈ c, f x = true
Theorem: LeanColls.Fold.all_iff_exists
Proof state before:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ (toList c).all f = true ↔ ∀ x ∈ c, f x = true
Tactic:
simp [Mem.ToList.mem_iff_mem_toList]
Proof state after:
no goals
Theorem: LeanColls.IndexType.toFin_inj
Proof state before:
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j ↔ i = j
Tactic:
constructor
Proof state after:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j → i = j

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ i = j → toFin i = toFin j
Theorem: LeanColls.IndexType.toFin_inj
Proof state before:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j → i = j
Tactic:
apply LawfulIndexType.leftInv.injective
Proof state after:
no goals
Theorem: LeanColls.IndexType.toFin_inj
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ i = j → toFin i = toFin j
Tactic:
rintro rfl
Proof state after:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : ι
⊢ toFin i = toFin i
Theorem: LeanColls.IndexType.toFin_inj
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : ι
⊢ toFin i = toFin i
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanColls.IndexType.fromFin_inj
Proof state before:
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j ↔ i = j
Tactic:
constructor
Proof state after:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j → i = j

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ i = j → fromFin i = fromFin j
Theorem: LeanColls.IndexType.fromFin_inj
Proof state before:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j → i = j
Tactic:
apply LawfulIndexType.rightInv.injective
Proof state after:
no goals
Theorem: LeanColls.IndexType.fromFin_inj
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ i = j → fromFin i = fromFin j
Tactic:
rintro rfl
Proof state after:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : Fin (card ι)
⊢ fromFin i = fromFin i
Theorem: LeanColls.IndexType.fromFin_inj
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : Fin (card ι)
⊢ fromFin i = fromFin i
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanColls.IndexType.toFin_eq_iff
Proof state before:
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : ι
⊢ toFin x = toFin y ↔ x = y
Tactic:
constructor
Proof state after:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : ι
⊢ toFin x = toFin y → x = y

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : ι
⊢ x = y → toFin x = toFin y
Theorem: LeanColls.IndexType.toFin_eq_iff
Proof state before:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : ι
⊢ toFin x = toFin y → x = y
Tactic:
apply toEquiv.injective
Proof state after:
no goals
Theorem: LeanColls.IndexType.toFin_eq_iff
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : ι
⊢ x = y → toFin x = toFin y
Tactic:
rintro rfl
Proof state after:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x : ι
⊢ toFin x = toFin x
Theorem: LeanColls.IndexType.toFin_eq_iff
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x : ι
⊢ toFin x = toFin x
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanColls.IndexType.fromFin_eq_iff
Proof state before:
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : Fin (card ι)
⊢ fromFin x = fromFin y ↔ x = y
Tactic:
constructor
Proof state after:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : Fin (card ι)
⊢ fromFin x = fromFin y → x = y

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : Fin (card ι)
⊢ x = y → fromFin x = fromFin y
Theorem: LeanColls.IndexType.fromFin_eq_iff
Proof state before:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : Fin (card ι)
⊢ fromFin x = fromFin y → x = y
Tactic:
apply toEquiv.symm.injective
Proof state after:
no goals
Theorem: LeanColls.IndexType.fromFin_eq_iff
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : Fin (card ι)
⊢ x = y → fromFin x = fromFin y
Tactic:
rintro rfl
Proof state after:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x : Fin (card ι)
⊢ fromFin x = fromFin x
Theorem: LeanColls.IndexType.fromFin_eq_iff
Proof state before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x : Fin (card ι)
⊢ fromFin x = fromFin x
Tactic:
rfl
Proof state after:
no goals
Theorem: LeanColls.IndexType.length_toList_univ
Proof state before:
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (toList (univ α)).length = card α
Tactic:
rw [LawfulIndexType.toList_eq_ofFn]
Proof state after:
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (List.ofFn fromFin).length = card α
Theorem: LeanColls.IndexType.length_toList_univ
Proof state before:
ι : Type ?u.1606
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
⊢ (List.ofFn fromFin).length = card α
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.IndexType.get_toList_univ
Proof state before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type ?u.1841
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ (toList (univ α)).length = card α
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.IndexType.get_toList_univ
Proof state before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ (toList (univ α)).get i = fromFin (Fin.cast ⋯ i)
Tactic:
suffices ∀ L i (hL : L = toList (univ α)), List.get L i = fromFin (i.cast (by simp [hL]))
  from this _ _ rfl
Proof state after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ ∀ (L : List α) (i : Fin L.length) (hL : L = toList (univ α)), L.get i = fromFin (Fin.cast ⋯ i)
Theorem: LeanColls.IndexType.get_toList_univ
Proof state before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i : Fin (toList (univ α)).length
⊢ ∀ (L : List α) (i : Fin L.length) (hL : L = toList (univ α)), L.get i = fromFin (Fin.cast ⋯ i)
Tactic:
intro L i hL
Proof state after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL : L = toList (univ α)
⊢ L.get i = fromFin (Fin.cast ⋯ i)
Theorem: LeanColls.IndexType.get_toList_univ
Proof state before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL : L = toList (univ α)
⊢ L.get i = fromFin (Fin.cast ⋯ i)
Tactic:
rw [LawfulIndexType.toList_eq_ofFn] at hL
Proof state after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL✝ : L = toList (univ α)
hL : L = List.ofFn fromFin
⊢ L.get i = fromFin (Fin.cast ⋯ i)
Theorem: LeanColls.IndexType.get_toList_univ
Proof state before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL✝ : L = toList (univ α)
hL : L = List.ofFn fromFin
⊢ L.get i = fromFin (Fin.cast ⋯ i)
Tactic:
subst hL
Proof state after:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
i : Fin (List.ofFn fromFin).length
hL : List.ofFn fromFin = toList (univ α)
⊢ (List.ofFn fromFin).get i = fromFin (Fin.cast ⋯ i)
Theorem: LeanColls.IndexType.get_toList_univ
Proof state before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
i : Fin (List.ofFn fromFin).length
hL : List.ofFn fromFin = toList (univ α)
⊢ (List.ofFn fromFin).get i = fromFin (Fin.cast ⋯ i)
Tactic:
simp
Proof state after:
no goals
Theorem: LeanColls.IndexType.get_toList_univ
Proof state before:
ι : Type ?u.1822
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
i✝ : Fin (toList (univ α)).length
L : List α
i : Fin L.length
hL : L = toList (univ α)
⊢ L.length = card α
Tactic:
simp [hL]
Proof state after:
no goals
Theorem: LeanColls.IndexType.mem_toList_univ
Proof state before:
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ x ∈ toList (univ α)
Tactic:
simp [LawfulIndexType.toList_eq_ofFn, List.mem_ofFn]
Proof state after:
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ ∃ y, fromFin y = x
Theorem: LeanColls.IndexType.mem_toList_univ
Proof state before:
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ ∃ y, fromFin y = x
Tactic:
use toFin x
Proof state after:
case h
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ fromFin (toFin x) = x
Theorem: LeanColls.IndexType.mem_toList_univ
Proof state before:
case h
ι : Type ?u.2325
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
α : Type u_1
inst✝¹ : IndexType α
inst✝ : LawfulIndexType α
x : α
⊢ fromFin (toFin x) = x
Tactic:
simp
Proof state after:
no goals
Theorem: nnnorm_eq_of_mem_circle
Proof state before:
z : ↥circle
⊢ ↑‖↑z‖₊ = 1
Tactic:
simp
Proof state after:
no goals
Theorem: nnnorm_circle_smul
Proof state before:
z : ↥circle
s : ℂ
⊢ ‖z • s‖₊ = ‖s‖₊
Tactic:
simp [show z • s = z.val * s from rfl]
Proof state after:
no goals
Theorem: hasDerivAt_e
Proof state before:
u x : ℝ
⊢ HasDerivAt (⇑(e u)) (-2 * ↑π * ↑u * I * (e u) x) x
Tactic:
have l2 : HasDerivAt (fun v => -v * u) (-u) x := by simpa only [neg_mul_comm] using hasDerivAt_mul_const (-u)
Proof state after:
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ HasDerivAt (⇑(e u)) (-2 * ↑π * ↑u * I * (e u) x) x