awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
a b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
hab : a < b
inl :
  ∀
    (a b :
      Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0)))
    (hab : a < b),
    LT.lt (α := Fin n)
      ((fun
            (j :
              Fin
                (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                  (c.index 0))) ↦
          (if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
            else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯ :
            Fin n))
        a)
      ((fun
            (j :
              Fin
                (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                  (c.index 0))) ↦
          (if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
            else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯ :
            Fin n))
        b)
⊢ LT.lt (α := Fin n)
    ((fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯ : Fin n))
      a)
    ((fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯ : Fin n))
      b)
have inr : ∀ (hi : i ≠ c.index 0),
  LT.lt (α := Fin n)
    ((fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (if h : i = c.index 0 then (c.emb i (Fin.cast sorry j.succ)).pred sorry else (c.emb i (Fin.cast sorry j)).pred sorry : Fin n))
      a)
    ((fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (if h : i = c.index 0 then (c.emb i (Fin.cast sorry j.succ)).pred sorry else (c.emb i (Fin.cast sorry j)).pred sorry : Fin n))
      b)
Tactic: rcases eq_or_ne i (c.index 0) with rfl | hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
a b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))
hab : a < b
⊢ LT.lt (α := Fin n)
    ((fun
          (j :
            Fin
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                (c.index 0))) ↦
        (if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
          else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯ :
          Fin n))
      a)
    ((fun
          (j :
            Fin
              (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                (c.index 0))) ↦
        (if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
          else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯ :
          Fin n))
      b)
have inl : c.emb (c.index 0) (Fin.cast sorry a.succ) < c.emb (c.index 0) (Fin.cast sorry b.succ)
Tactic: simp only [↓reduceDIte, Nat.succ_eq_add_one, pred_lt_pred_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i : Fin c.length
a b : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
hab : a < b
hi : i ≠ c.index 0
⊢ LT.lt (α := Fin n)
    ((fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯ : Fin n))
      a)
    ((fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)) ↦
        (if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯ : Fin n))
      b)
have inr : c.emb i (Fin.cast sorry a) < c.emb i (Fin.cast sorry b)
Tactic: simp only [hi, ↓reduceDIte, pred_lt_pred_iff, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
⊢ (↑(if h : i = c.index 0 then
            (c.emb i
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i -
                            1,
                          ⋯⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            i)).succ)).pred
              ⋯
          else
            (c.emb i
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i -
                          1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          i)))).pred
              ⋯) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) i) : ℕ)
have h : ∀ (hij : c.index 0 < j),
  (↑(if h : c.index 0 = c.index 0 then
            (c.emb (c.index 0)
                  (Fin.cast (n :=
                    update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0) +
                      1)
                    sorry
                    (succ
                      (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                              (c.index 0) -
                            1,
                          sorry⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0)))))).pred
              sorry
          else
            (c.emb (c.index 0)
                  (Fin.cast sorry
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0) -
                          1,
                        sorry⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0))))).pred
              sorry) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, sorry⟩ : Fin (c.partSize m))) (c.index 0)) : ℕ)
Tactic: rcases eq_or_ne i (c.index 0) with rfl | hi
Cleared hypotheses: i, hij
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
⊢ (↑(if h : c.index 0 = c.index 0 then
            (c.emb (c.index 0)
                  (Fin.cast (n :=
                    update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        (c.index 0) +
                      1)
                    ⋯
                    (succ
                      (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                              (c.index 0) -
                            1,
                          ⋯⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0)))))).pred
              ⋯
          else
            (c.emb (c.index 0)
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            (c.index 0) -
                          1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          (c.index 0))))).pred
              ⋯) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) (c.index 0)) : ℕ)
have h : (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, sorry⟩ : Fin (c.partSize (c.index 0)))) : ℕ) - 1 + 1 =
  (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, sorry⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
Tactic: simp only [↓reduceDIte, update_self, succ_mk, cast_mk, val_pred]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
⊢ (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ) - 1 + 1 =
    (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
have A : 1 < c.partSize (c.index 0)
Tactic: have A := c.one_lt_partSize_index_zero hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ) - 1 + 1 =
    (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
have h : (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, sorry⟩ : Fin (c.partSize (c.index 0)))) : ℕ) =
  (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, sorry⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
Tactic: rw [Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
h :
  (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ) =
    (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
⊢ (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ) - 1 + 1 =
    (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
have h₁ : 1 ≤ (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, sorry⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
Tactic: rw [Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ) =
    (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
have h : c.partSize (c.index 0) - 1 - 1 + 1 = c.partSize (c.index 0) - 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
| 0
have rw : (↑(c.emb (c.index 0) 0) : ℕ)
Tactic: rw [show (0 : ℕ) = c.emb (c.index 0) 0 by simp [emb_zero]]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ 0 < (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
have h : (↑(c.emb (c.index 0) 0) : ℕ) <
  (↑(c.emb (c.index 0) (⟨c.partSize (c.index 0) - 1 - 1 + 1, sorry⟩ : Fin (c.partSize (c.index 0)))) : ℕ)
Tactic: conv_lhs => rw [show (0 : ℕ) = c.emb (c.index 0) 0 by simp [emb_zero]]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ c.emb (c.index 0) 0 < c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩
have h : LT.lt (α := Fin (c.partSize (c.index 0))) 0 ⟨c.partSize (c.index 0) - 1 - 1 + 1, sorry⟩
Tactic: apply c.emb_strictMono
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
hi : i ≠ c.index 0
⊢ (↑(if h : i = c.index 0 then
            (c.emb i
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i -
                            1,
                          ⋯⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            i)).succ)).pred
              ⋯
          else
            (c.emb i
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i -
                          1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          i)))).pred
              ⋯) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) i) : ℕ)
have h : (↑(c.emb i (⟨c.partSize i - 1, sorry⟩ : Fin (c.partSize i))) : ℕ) - 1 + 1 =
  (↑(c.emb i (⟨c.partSize i - 1, sorry⟩ : Fin (c.partSize i))) : ℕ)
Tactic: simp only [hi, ↓reduceDIte, ne_eq, not_false_eq_true, update_of_ne, cast_mk, val_pred]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
hi : i ≠ c.index 0
⊢ (↑(c.emb i (⟨c.partSize i - 1, ⋯⟩ : Fin (c.partSize i))) : ℕ) - 1 + 1 =
    (↑(c.emb i (⟨c.partSize i - 1, ⋯⟩ : Fin (c.partSize i))) : ℕ)
have h : 1 ≤ (↑(c.emb i (⟨c.partSize i - 1, sorry⟩ : Fin (c.partSize i))) : ℕ)
Tactic: apply Nat.sub_add_cancel
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
hi : i ≠ c.index 0
⊢ 1 ≤ (↑(c.emb i (⟨c.partSize i - 1, ⋯⟩ : Fin (c.partSize i))) : ℕ)
have this : c.emb i (⟨c.partSize i - 1, sorry⟩ : Fin (c.partSize i)) ≠ c.emb (c.index 0) 0
Tactic: have : c.emb i ⟨c.partSize i - 1, Nat.sub_one_lt_of_lt (c.partSize_pos i)⟩
            ≠ c.emb (c.index 0) 0 := c.emb_ne_emb_of_ne hi
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c_1 : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
hi : i ≠ c.index 0
this : c.emb i (⟨c.partSize i - 1, ⋯⟩ : Fin (c.partSize i)) ≠ c.emb (c.index 0) 0
⊢ 1 ≤ (↑(c.emb i (⟨c.partSize i - 1, ⋯⟩ : Fin (c.partSize i))) : ℕ)
have this₁ : ¬(↑(c.emb i (⟨c.partSize i - 1, sorry⟩ : Fin (c.partSize i))) : ℕ) = 0
Tactic: simp only [c.emb_zero, ne_eq, ← val_eq_val, val_zero] at this
Cleared hypotheses: this