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 j : Fin c.length
hij : i < j
⊢ (↑(if h : j = c.index 0 then
            (c.emb j
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j -
                            1,
                          ⋯⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            j)).succ)).pred
              ⋯
          else
            (c.emb j
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j -
                          1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          j)))).pred
              ⋯) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) j) : ℕ)
have h : ∀ (hij : i < c.index 0),
  (↑(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 j (c.index 0) with rfl | hj
Cleared hypotheses: j, 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}
i : Fin c.length
hij : i < c.index 0
⊢ (↑(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}
i : Fin c.length
hij : i < 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 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}
i : Fin c.length
hij : i < c.index 0
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}
i : Fin c.length
hij : i < c.index 0
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}
i : Fin c.length
hij : i < c.index 0
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}
i : Fin c.length
hij : i < c.index 0
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}
i : Fin c.length
hij : i < c.index 0
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}
i : Fin c.length
hij : i < c.index 0
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
hj : j ≠ c.index 0
⊢ (↑(if h : j = c.index 0 then
            (c.emb j
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j -
                            1,
                          ⋯⟩ :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            j)).succ)).pred
              ⋯
          else
            (c.emb j
                  (Fin.cast ⋯
                    (⟨update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j -
                          1,
                        ⋯⟩ :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          j)))).pred
              ⋯) :
        ℕ) +
      1 =
    (↑((fun (m : Fin c.length) ↦ c.emb m (⟨c.partSize m - 1, ⋯⟩ : Fin (c.partSize m))) j) : ℕ)
have h : (↑(c.emb j (⟨c.partSize j - 1, sorry⟩ : Fin (c.partSize j))) : ℕ) - 1 + 1 =
  (↑(c.emb j (⟨c.partSize j - 1, sorry⟩ : Fin (c.partSize j))) : ℕ)
Tactic: simp only [hj, ↓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
hj : j ≠ c.index 0
⊢ (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ) - 1 + 1 =
    (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ)
have h : 1 ≤ (↑(c.emb j (⟨c.partSize j - 1, sorry⟩ : Fin (c.partSize j))) : ℕ)
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
hj : j ≠ c.index 0
⊢ 1 ≤ (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ)
have this : c.emb j (⟨c.partSize j - 1, sorry⟩ : Fin (c.partSize j)) ≠ c.emb (c.index 0) 0
Tactic: have : c.emb j ⟨c.partSize j - 1, Nat.sub_one_lt_of_lt (c.partSize_pos j)⟩
            ≠ c.emb (c.index 0) 0 := c.emb_ne_emb_of_ne hj
-- 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
hj : j ≠ c.index 0
this : c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j)) ≠ c.emb (c.index 0) 0
⊢ 1 ≤ (↑(c.emb j (⟨c.partSize j - 1, ⋯⟩ : Fin (c.partSize j))) : ℕ)
have this₁ : ¬(↑(c.emb j (⟨c.partSize j - 1, sorry⟩ : Fin (c.partSize j))) : ℕ) = 0
Tactic: simp only [c.emb_zero, ne_eq, ← val_eq_val, val_zero] at this
Cleared hypotheses: this
-- 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
h : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)) ↦
        if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j
have inr : ∀
  (this :
    ∀ (i : Fin c.length),
      Membership.mem (γ := Set (Fin c.length)) univ i →
        ∀ (j : Fin c.length),
          Membership.mem (γ := Set (Fin c.length)) univ j →
            ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
              onFun (β := Set (Fin n)) Disjoint
                (fun (m : Fin c.length) ↦
                  range
                    fun
                      (j :
                        Fin
                          (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                            m)) ↦
                    if h : m = c.index 0 then (c.emb m (Fin.cast sorry j.succ)).pred sorry else (c.emb m (Fin.cast sorry j)).pred sorry)
                i j)
  (h : ¬i ≠ c.index 0),
  onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)) ↦
        if h : m = c.index 0 then (c.emb m (Fin.cast sorry j.succ)).pred sorry else (c.emb m (Fin.cast sorry j)).pred sorry)
    i j
Tactic: wlog h : i ≠ c.index 0 generalizing i j
-- 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
h : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
inr :
  ∀
    (this :
      ∀ (i : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ i →
          ∀ (j : Fin c.length),
            Membership.mem (γ := Set (Fin c.length)) univ j →
              ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
                onFun (β := Set (Fin n)) Disjoint
                  (fun (m : Fin c.length) ↦
                    range
                      fun
                        (j :
                          Fin
                            (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0)
                              (c.partSize (c.index 0) - 1) m)) ↦
                      if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯
                      else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
                  i j)
    (h : ¬i ≠ c.index 0),
    onFun (β := Set (Fin n)) Disjoint
      (fun (m : Fin c.length) ↦
        range
          fun
            (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)) ↦
          if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
      i j
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)) ↦
        if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j
have wlog : ∀ (i : Fin c.length),
  Membership.mem (γ := Set (Fin c.length)) univ i →
    ∀ (j : Fin c.length),
      Membership.mem (γ := Set (Fin c.length)) univ j →
        ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
          onFun (β := Set (Fin n)) Disjoint
            (fun (m : Fin c.length) ↦
              range
                fun
                  (j :
                    Fin
                      (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                        m)) ↦
                if h : m = c.index 0 then (c.emb m (Fin.cast sorry j.succ)).pred sorry else (c.emb m (Fin.cast sorry j)).pred sorry)
            i j
Tactic: wlog h : i ≠ c.index 0 generalizing i j
Cleared hypotheses: i, h, j, h_1, 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}
i : Fin c.length
h_1 : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
h_2 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
this :
  ∀ (i : Fin c.length),
    Membership.mem (γ := Set (Fin c.length)) univ i →
      ∀ (j : Fin c.length),
        Membership.mem (γ := Set (Fin c.length)) univ j →
          ∀ (hij : i ≠ j) (h : i ≠ c.index 0),
            onFun (β := Set (Fin n)) Disjoint
              (fun (m : Fin c.length) ↦
                range
                  fun
                    (j :
                      Fin
                        (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1)
                          m)) ↦
                  if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
              i j
h : ¬i ≠ c.index 0
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin c.length) ↦
      range
        fun (j : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index 0) (c.partSize (c.index 0) - 1) m)) ↦
        if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j
have apply : j ≠ c.index 0
Tactic: apply Disjoint.symm
        (this j (mem_univ j) i (mem_univ i) hij.symm ?_)