internlm/Lean-Github huggingface dataset:
Theorem: from_above
Proof state before:
p q r : Prop
⊢ ∀ (x : ℕ), ∃ y, x < y
Tactic:
sorry
Proof state after:
no goals
Theorem: other_order
Proof state before:
p q r : Prop
⊢ ∃ x, ∀ (y : ℕ), x ≤ y
Tactic:
sorry
Proof state after:
no goals
Theorem: two_imp
Proof state before:
p q r : Prop
h1 : p → q
h2 : q → ¬r
⊢ r → ¬p
Tactic:
sorry
Proof state after:
no goals
Theorem: quantifier_switch
Proof state before:
p q r : Prop
P : ℕ → Prop
⊢ (¬∃ x, P x) → ∀ (x : ℕ), ¬P x
Tactic:
sorry
Proof state after:
no goals
Theorem: div_by_5
Proof state before:
p q r : Prop
⊢ ∀ (n : ℕ), 5 ∣ 11 ^ n - 6
Tactic:
intro n
Proof state after:
p q r : Prop
n : ℕ
⊢ 5 ∣ 11 ^ n - 6
Theorem: div_by_5
Proof state before:
p q r : Prop
n : ℕ
⊢ 5 ∣ 11 ^ n - 6
Tactic:
induction' n with k ih
Proof state after:
case zero
p q r : Prop
⊢ 5 ∣ 11 ^ Nat.zero - 6

case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6
Theorem: div_by_5
Proof state before:
case zero
p q r : Prop
⊢ 5 ∣ 11 ^ Nat.zero - 6

case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6
Tactic:
. simp
Proof state after:
case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6
Theorem: div_by_5
Proof state before:
case succ
p q r : Prop
k : ℕ
ih : 5 ∣ 11 ^ k - 6
⊢ 5 ∣ 11 ^ Nat.succ k - 6
Tactic:
. cases' ih with w hw
  have : 11 ^ k = 5*w + 6 
  . sorry
  simp [Nat.pow_succ, this, add_mul]
  use w*11
  ring
Proof state after:
no goals
Theorem: sets_eq
Proof state before:
p q r : Prop
s t u : Set ℕ
⊢ (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
Tactic:
ext x
Proof state after:
case h
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u ↔ x ∈ s ∩ u ∪ t ∩ u
Theorem: sets_eq
Proof state before:
case h
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u ↔ x ∈ s ∩ u ∪ t ∩ u
Tactic:
constructor
Proof state after:
case h.mp
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u → x ∈ s ∩ u ∪ t ∩ u

case h.mpr
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ s ∩ u ∪ t ∩ u → x ∈ (s ∪ t) ∩ u
Theorem: foo
Proof state before:
n : ℕ
⊢ a n = 2 ^ n + 3 ^ n
Tactic:
induction' n using Nat.two_step_induction with n h1 h2
Proof state after:
case H1

⊢ a 0 = 2 ^ 0 + 3 ^ 0

case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Theorem: foo
Proof state before:
case H1

⊢ a 0 = 2 ^ 0 + 3 ^ 0

case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Tactic:
. rfl
Proof state after:
case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Theorem: foo
Proof state before:
case H2

⊢ a 1 = 2 ^ 1 + 3 ^ 1

case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Tactic:
. rfl
Proof state after:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Theorem: foo
Proof state before:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (Nat.succ n) = 2 ^ Nat.succ n + 3 ^ Nat.succ n
⊢ a (Nat.succ (Nat.succ n)) = 2 ^ Nat.succ (Nat.succ n) + 3 ^ Nat.succ (Nat.succ n)
Tactic:
simp [Nat.succ_eq_add_one] at *
Proof state after:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ a (n + 1 + 1) = 2 ^ (n + 1 + 1) + 3 ^ (n + 1 + 1)
Theorem: foo
Proof state before:
case H3
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ a (n + 1 + 1) = 2 ^ (n + 1 + 1) + 3 ^ (n + 1 + 1)
Tactic:
calc
  a (n + 2) 
    = (5 : ℤ) * (2 ^ (n + 1) + 3 ^ (n + 1)) - 
        6 * (2 ^ n + 3 ^ n) := by linarith [helper n]
  _ = (2 : ℤ) ^ (n + 2) + 3 ^ (n + 2) := by ring
Proof state after:
no goals
Theorem: foo
Proof state before:
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ a (n + 2) = 5 * (2 ^ (n + 1) + 3 ^ (n + 1)) - 6 * (2 ^ n + 3 ^ n)
Tactic:
linarith [helper n]
Proof state after:
no goals
Theorem: foo
Proof state before:
n : ℕ
h1 : a n = 2 ^ n + 3 ^ n
h2 : a (n + 1) = 2 ^ (n + 1) + 3 ^ (n + 1)
⊢ 5 * (2 ^ (n + 1) + 3 ^ (n + 1)) - 6 * (2 ^ n + 3 ^ n) = 2 ^ (n + 2) + 3 ^ (n + 2)
Tactic:
ring
Proof state after:
no goals
Theorem: bar2
Proof state before:
n : ℕ
⊢ odd (a (n + 1))
Tactic:
induction' n with n h1 h2
Proof state after:
case zero

⊢ odd (a (Nat.zero + 1))

case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))
Theorem: bar2
Proof state before:
case zero

⊢ odd (a (Nat.zero + 1))

case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))
Tactic:
. use 2
  rfl
Proof state after:
case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))
Theorem: bar2
Proof state before:
case succ
n : ℕ
h1 : odd (a (n + 1))
⊢ odd (a (Nat.succ n + 1))
Tactic:
cases' h1 with k hk
Proof state after:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ odd (a (Nat.succ n + 1))
Theorem: bar2
Proof state before:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ odd (a (Nat.succ n + 1))
Tactic:
use 5*k - 3*a n + 2
Proof state after:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ a (Nat.succ n + 1) = 2 * (5 * k - 3 * a n + 2) + 1
Theorem: bar2
Proof state before:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ a (Nat.succ n + 1) = 2 * (5 * k - 3 * a n + 2) + 1
Tactic:
rw [helper]
Proof state after:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ 5 * a (n + 1) - 6 * a n = 2 * (5 * k - 3 * a n + 2) + 1
Theorem: bar2
Proof state before:
case succ.intro
n : ℕ
k : ℤ
hk : a (n + 1) = 2 * k + 1
⊢ 5 * a (n + 1) - 6 * a n = 2 * (5 * k - 3 * a n + 2) + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: bar
Proof state before:
n : ℕ
⊢ n ≥ 1 → odd (_root_.a n)
Tactic:
induction' n using Nat.two_step_induction with n h1 h2
Proof state after:
case H1

⊢ 0 ≥ 1 → odd (_root_.a 0)

case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Theorem: bar
Proof state before:
case H1

⊢ 0 ≥ 1 → odd (_root_.a 0)

case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Tactic:
. norm_num
Proof state after:
case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Theorem: bar
Proof state before:
case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Tactic:
. intro h
  use 2
  rfl
Proof state after:
case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Theorem: bar
Proof state before:
case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))
Tactic:
simp only [Nat.succ_eq_add_one] at *
Proof state after:
case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : n + 1 ≥ 1 → odd (_root_.a (n + 1))
⊢ n + 1 + 1 ≥ 1 → odd (_root_.a (n + 1 + 1))
Theorem: problem1
Proof state before:
a b : ℚ
h1 : a - b = 4
h2 : a * b = 1
⊢ (a + b) ^ 2 = (a - b) ^ 2 + 4 * (a * b)
Tactic:
ring
Proof state after:
no goals
Theorem: problem1
Proof state before:
a b : ℚ
h1 : a - b = 4
h2 : a * b = 1
⊢ (a - b) ^ 2 + 4 * (a * b) = 4 ^ 2 + 4 * 1
Tactic:
rw [h1, h2]
Proof state after:
no goals
Theorem: problem1
Proof state before:
a b : ℚ
h1 : a - b = 4
h2 : a * b = 1
⊢ 4 ^ 2 + 4 * 1 = 20
Tactic:
ring
Proof state after:
no goals
Theorem: problem2
Proof state before:
a : ℚ
h : ∃ b, a = b ^ 2
⊢ a ≥ 0
Tactic:
cases' h with b hb
Proof state after:
case intro
a b : ℚ
hb : a = b ^ 2
⊢ a ≥ 0
Theorem: problem2
Proof state before:
case intro
a b : ℚ
hb : a = b ^ 2
⊢ a ≥ 0
Tactic:
calc a = b ^ 2 := hb
_ ≥ 0 := by apply sq_nonneg
Proof state after:
no goals
Theorem: problem2
Proof state before:
a b : ℚ
hb : a = b ^ 2
⊢ b ^ 2 ≥ 0
Tactic:
apply sq_nonneg
Proof state after:
no goals
Theorem: you_might_use_this_theorem_in_your_answer
Proof state before:
⊢ 1 + 1 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: problem3
Proof state before:
⊢ ∃ n, 12 * n = 84
Tactic:
existsi 7
Proof state after:
⊢ 12 * 7 = 84
Theorem: problem3
Proof state before:
⊢ 12 * 7 = 84
Tactic:
norm_num
Proof state after:
no goals
Theorem: Finset.sup_filter_eq_sup_univ_subtype_coe
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup univ fun i => f ↑i
Tactic:
rw [← Finset.subtype_univ]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (Finset.subtype (fun a => p a) univ) fun i => f ↑i
Theorem: Finset.sup_filter_eq_sup_univ_subtype_coe
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (Finset.subtype (fun a => p a) univ) fun i => f ↑i
Tactic:
rw [Finset.subtype]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup
      (map
        { toFun := fun x => { val := ↑x, property := (_ : p ↑x) },
          inj' :=
            (_ :
              ∀ (x y : { x // x ∈ filter (fun a => p a) univ }),
                (fun x => { val := ↑x, property := (_ : p ↑x) }) x =
                    (fun x => { val := ↑x, property := (_ : p ↑x) }) y →
                  x = y) }
        (attach (filter (fun a => p a) univ)))
      fun i => f ↑i
Theorem: Finset.sup_filter_eq_sup_univ_subtype_coe
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup
      (map
        { toFun := fun x => { val := ↑x, property := (_ : p ↑x) },
          inj' :=
            (_ :
              ∀ (x y : { x // x ∈ filter (fun a => p a) univ }),
                (fun x => { val := ↑x, property := (_ : p ↑x) }) x =
                    (fun x => { val := ↑x, property := (_ : p ↑x) }) y →
                  x = y) }
        (attach (filter (fun a => p a) univ)))
      fun i => f ↑i
Tactic:
simp
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup (attach (filter (fun a => p a) univ)) ((fun i => f ↑i) ∘ fun x => { val := ↑x, property := (_ : p ↑x) })
Theorem: Finset.sup_filter_eq_sup_univ_subtype_coe
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) =
    sup (attach (filter (fun a => p a) univ)) ((fun i => f ↑i) ∘ fun x => { val := ↑x, property := (_ : p ↑x) })
Tactic:
conv => rhs; arg 2; intro x; simp
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (attach (filter (fun a => p a) univ)) fun x => f ↑x
Theorem: Finset.sup_filter_eq_sup_univ_subtype_coe
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : DecidableEq ι
i : ι
p : ι → Prop
inst✝⁵ : DecidablePred p
α : ι → Type u_3
inst✝⁴ : (j : ι) → NormedAddCommGroup (α j)
inst✝³ : (j : ι) → NormedSpace 𝕜 (α j)
inst✝² : Fintype ι
R : Type u_4
inst✝¹ : SemilatticeSup R
inst✝ : OrderBot R
f : ι → R
⊢ (sup (filter p univ) fun i => f i) = sup (attach (filter (fun a => p a) univ)) fun x => f ↑x
Tactic:
rw [sup_attach]
Proof state after:
no goals
Theorem: Function.update_piSplitAt_symm
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u = (Equiv.piSplitAt i α).symm (u, x)
Tactic:
ext j
Proof state after:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Theorem: Function.update_piSplitAt_symm
Proof state before:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
by_cases h : j = i
Proof state after:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j

case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Theorem: Function.update_piSplitAt_symm
Proof state before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j

case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
. rw [h]; simp
Proof state after:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Theorem: Function.update_piSplitAt_symm
Proof state before:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
. simp [h]
Proof state after:
no goals
Theorem: Function.update_piSplitAt_symm
Proof state before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
rw [h]
Proof state after:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u i = (Equiv.piSplitAt i α).symm (u, x) i
Theorem: Function.update_piSplitAt_symm
Proof state before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u i = (Equiv.piSplitAt i α).symm (u, x) i
Tactic:
simp
Proof state after:
no goals
Theorem: Function.update_piSplitAt_symm
Proof state before:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
a u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ update ((Equiv.piSplitAt i α).symm (a, x)) i u j = (Equiv.piSplitAt i α).symm (u, x) j
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Equiv.piSplitAt_symm_zero_add_single
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
⊢ (piSplitAt i α).symm (0, x) + Pi.single i u = (piSplitAt i α).symm (u, x)
Tactic:
ext j
Proof state after:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Theorem: Equiv.piSplitAt_symm_zero_add_single
Proof state before:
case h
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Tactic:
by_cases h : j = i
Proof state after:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j

case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Theorem: Equiv.piSplitAt_symm_zero_add_single
Proof state before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j

case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Tactic:
. rw [h]; simp
Proof state after:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Theorem: Equiv.piSplitAt_symm_zero_add_single
Proof state before:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Tactic:
. simp [h]
Proof state after:
no goals
Theorem: Equiv.piSplitAt_symm_zero_add_single
Proof state before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Tactic:
rw [h]
Proof state after:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) i = (piSplitAt i α).symm (u, x) i