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 c : OrderedFinpartition n
k : Fin c.length
⊢ ∃ (m : Fin c.length),
    Membership.mem (γ := Set (Fin (n + 1)))
      (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            ⋯;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
      0
have refine_1 : ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
  Eq (α := Fin (n + 1))
    ((if h : m = k then
        (fun (i : Fin (c.partSize k + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
          Fin.cast sorry
      else succ ∘ c.emb m ∘ Fin.cast sorry)
      y)
    0
Tactic: simp only [mem_range]
-- 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 c : OrderedFinpartition n
k : Fin c.length
i : Fin n
⊢ ∃ (m : Fin c.length),
    Membership.mem (γ := Set (Fin (n + 1)))
      (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m))
        (if h : m = k then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize k + 1 :=
            ⋯;
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m = c.partSize m := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
      i.succ
have refine_2 : ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
  (if h : m = k then
        (fun (i : Fin (c.partSize k + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
          Fin.cast sorry
      else succ ∘ c.emb m ∘ Fin.cast sorry)
      y =
    i.succ
Tactic: simp only [mem_range]
-- 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 c : OrderedFinpartition n
k : Fin c.length
i : Fin n
⊢ ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    (if h : m = k then
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ
have refine_2 : ∃ (m : Fin c.length) (y :
  Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index i) (c.partSize (c.index i) + 1) m)),
  (if h : m = c.index i then
        (fun (i_1 : Fin (c.partSize (c.index i) + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize (c.index i) + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb (c.index i))
              i_1) ∘
          Fin.cast sorry
      else succ ∘ c.emb m ∘ Fin.cast sorry)
      y =
    i.succ
Tactic: rcases eq_or_ne (c.index i) k with rfl | hi
Cleared hypotheses: k
-- 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 c : OrderedFinpartition n
k : Fin c.length
i : Fin n
refine_2 :
  ∃ (m : Fin c.length) (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index i) (c.partSize (c.index i) + 1) m)),
    (if h : m = c.index i then
          (fun (i_1 : Fin (c.partSize (c.index i) + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize (c.index i) + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb (c.index i))
                i_1) ∘
            Fin.cast ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ
⊢ ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    (if h : m = k then
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ
have refine_2₁ : ∀ (hi : c.index i ≠ k),
  ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    (if h : m = k then
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast sorry
        else succ ∘ c.emb m ∘ Fin.cast sorry)
        y =
      i.succ
Tactic: rcases eq_or_ne (c.index i) k with rfl | 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 c : OrderedFinpartition n
i : Fin n
⊢ ∃ (m : Fin c.length) (y :
    Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index i) (c.partSize (c.index i) + 1) m)),
    (if h : m = c.index i then
          (fun (i_1 : Fin (c.partSize (c.index i) + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize (c.index i) + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb (c.index i))
                i_1) ∘
            Fin.cast ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ
have A : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) =
  c.partSize (c.index i) + 1
Tactic: have A : update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) =
          c.partSize (c.index i) + 1 := by simp
-- 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 c : OrderedFinpartition n
k : Fin c.length
i : Fin n
hi : c.index i ≠ k
⊢ ∃ (m : Fin c.length) (y : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) m)),
    (if h : m = k then
          (fun (i : Fin (c.partSize k + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize k + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb k) i) ∘
            Fin.cast ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ
have A : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i)
Tactic: have A : update c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i) := by
          simp [hi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
⊢ (c.extendMiddle i).index 0 = i
have this : (c.extendMiddle i).emb i 0 = 0
Tactic: have : (c.extendMiddle i).emb i 0 = 0 := by simp [extendMiddle]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).emb i 0 = 0
| 0
have rw : (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
Tactic: rw [← (c.extendMiddle i).emb_invEmbedding 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this : (c.extendMiddle i).emb i 0 = 0
⊢ (c.extendMiddle i).index 0 = i
have this₁ : (c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
Tactic: conv_rhs at this => rw [← (c.extendMiddle i).emb_invEmbedding 0]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
this :
  (c.extendMiddle i).emb i 0 = (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
⊢ (c.extendMiddle i).index 0 = i
have contrapose! : ∀ (this : (c.extendMiddle i).index 0 ≠ i),
  (c.extendMiddle i).emb i 0 ≠ (c.extendMiddle i).emb ((c.extendMiddle i).index 0) ((c.extendMiddle i).invEmbedding 0)
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
⊢ False
have inl : ∀ (h : range ((c.extendMiddle j).emb j) = {0}), False
Tactic: rcases eq_or_ne j i with rfl | hij
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
inl : ∀ (h : range ((c.extendMiddle j).emb j) = {0}), False
⊢ False
have inr : ∀ (hij : j ≠ i), False
Tactic: rcases eq_or_ne j i with rfl | hij
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ Membership.mem (γ := Set (Fin n.succ)) {0} (c.emb j 0).succ
have rw : (c.emb j 0).succ ∈ range ((c.extendMiddle j).emb j)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ ∃ (y : Fin ((c.extendMiddle j).partSize j)), (c.extendMiddle j).emb j y = (c.emb j 0).succ
have A : (c.extendMiddle j).partSize j = c.partSize j + 1
Tactic: have A : (c.extendMiddle j).partSize j = c.partSize j + 1 := by simp [extendMiddle]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
A : (c.extendMiddle j).partSize j = c.partSize j + 1
⊢ ∃ (y : Fin ((c.extendMiddle j).partSize j)), (c.extendMiddle j).emb j y = (c.emb j 0).succ
have refine : (c.extendMiddle j).emb j (Fin.cast sorry (succ 0)) = (c.emb j 0).succ
Tactic: refine ⟨Fin.cast A.symm (succ 0), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
⊢ False
have this : Membership.mem (γ := Set (Fin n.succ)) {0} (c.emb j 0).succ
Tactic: have : Fin.succ (c.emb j 0) ∈ ({0} : Set (Fin n.succ)) := by
      rw [← h]
      simp only [Nat.succ_eq_add_one, mem_range]
      have A : (c.extendMiddle j).partSize j = c.partSize j + 1 := by simp [extendMiddle]
      refine ⟨Fin.cast A.symm (succ 0), ?_⟩
      simp only [extendMiddle, ↓reduceDIte, comp_apply, Fin.cast_cast, cast_eq_self, cases_succ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : Membership.mem (γ := Set (Fin n.succ)) {0} (c.emb j 0).succ
⊢ False
have this₁ : (c.emb j 0).succ = 0
Tactic: simp only [mem_singleton_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
⊢ False
have this : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j)
Tactic: have : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j) :=
      mem_range_self 0
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.extendMiddle i).emb j 0 ∈ range ((c.extendMiddle i).emb j)
⊢ False
have this₁ : Membership.mem (γ := Set (Fin (n + 1))) {0} ((c.extendMiddle i).emb j 0)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : Membership.mem (γ := Set (Fin (n + 1))) {0} ((c.extendMiddle i).emb j 0)
⊢ False
have this₁ : (c.emb j (Fin.cast sorry 0)).succ = 0
Tactic: simp only [extendMiddle, hij, ↓reduceDIte, comp_apply, mem_singleton_iff] at this
Cleared hypotheses: this
-- 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}
⊢ Fin (c.length - 1) → ℕ
have this : c.length - 1 + 1 = c.length
Tactic: have : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
-- 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 - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
⊢ Fin n
have this : c.length - 1 + 1 = c.length
Tactic: have : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
-- 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 - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this : c.length - 1 + 1 = c.length
⊢ Fin n
have refine : c.emb (Fin.cast this i.succ) j ≠ 0
Tactic: refine Fin.pred (c.emb (Fin.cast this (succ i)) j) ?_
-- 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 - 1)
j : Fin (c.partSize (Fin.cast ⋯ i.succ))
this : c.length - 1 + 1 = c.length
⊢ c.emb (Fin.cast this i.succ) j ≠ 0
have this₁ : onFun (β := Set (Fin (n + 1))) Disjoint (fun (m : Fin c.length) ↦ range (c.emb m)) (Fin.cast this i.succ) 0
Tactic: have := c.disjoint (mem_univ (Fin.cast this (succ i))) (mem_univ 0) (ne_of_beq_false rfl)
-- 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 - 1)
a b : Fin (c.partSize (Fin.cast ⋯ i.succ))
hab : a < b
⊢ LT.lt (α := Fin n)
    ((fun (j : Fin (c.partSize (Fin.cast ⋯ i.succ))) ↦
        have this := ⋯;
        (c.emb (Fin.cast this i.succ) j).pred ⋯)
      a)
    ((fun (j : Fin (c.partSize (Fin.cast ⋯ i.succ))) ↦
        have this := ⋯;
        (c.emb (Fin.cast this i.succ) j).pred ⋯)
      b)
have simp : c.emb (Fin.cast sorry i.succ) a < c.emb (Fin.cast sorry i.succ) b
Tactic: simp only [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 - 1)
hij : i < j
⊢ LT.lt (α := Fin n)
    ((fun (m : Fin (c.length - 1)) ↦
        have this := ⋯;
        (c.emb (Fin.cast this m.succ)
              (⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩ : Fin (c.partSize (Fin.cast ⋯ m.succ)))).pred
          ⋯)
      i)
    ((fun (m : Fin (c.length - 1)) ↦
        have this := ⋯;
        (c.emb (Fin.cast this m.succ)
              (⟨c.partSize (Fin.cast ⋯ m.succ) - 1, ⋯⟩ : Fin (c.partSize (Fin.cast ⋯ m.succ)))).pred
          ⋯)
      j)
have simp : c.emb (Fin.cast sorry i.succ) (⟨c.partSize (Fin.cast sorry i.succ) - 1, sorry⟩ : Fin (c.partSize (Fin.cast sorry i.succ))) <
  c.emb (Fin.cast sorry j.succ) ⟨c.partSize (Fin.cast sorry j.succ) - 1, sorry⟩
Tactic: simp only [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 : Fin (c.length - 1)
h : Membership.mem (γ := Set (Fin (c.length - 1))) univ i
j : Fin (c.length - 1)
h_1 : Membership.mem (γ := Set (Fin (c.length - 1))) univ j
hij : i ≠ j
⊢ onFun (β := Set (Fin n)) Disjoint
    (fun (m : Fin (c.length - 1)) ↦
      range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
        have this := ⋯;
        (c.emb (Fin.cast this m.succ) j).pred ⋯)
    i j
have apply : ∀ ⦃a : Fin n⦄,
  Membership.mem (γ := Set (Fin n))
      ((fun (m : Fin (c.length - 1)) ↦
          (range fun (j : Fin (c.partSize (Fin.cast sorry m.succ))) ↦
              have this := sorry;
              (c.emb (Fin.cast this m.succ) j).pred sorry :
            Set (Fin n)))
        i)
      a →
    ∀ ⦃b : Fin n⦄,
      Membership.mem (γ := Set (Fin n))
          ((fun (m : Fin (c.length - 1)) ↦
              (range fun (j : Fin (c.partSize (Fin.cast sorry m.succ))) ↦
                  have this := sorry;
                  (c.emb (Fin.cast this m.succ) j).pred sorry :
                Set (Fin n)))
            j)
          b →
        a ≠ b
Tactic: apply Set.disjoint_iff_forall_ne.2
-- 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 - 1)
h : Membership.mem (γ := Set (Fin (c.length - 1))) univ i
j : Fin (c.length - 1)
h_1 : Membership.mem (γ := Set (Fin (c.length - 1))) univ j
hij : i ≠ j
⊢ ∀ ⦃a : Fin n⦄,
    Membership.mem (γ := Set (Fin n))
        ((fun (m : Fin (c.length - 1)) ↦
            (range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
                have this := ⋯;
                (c.emb (Fin.cast this m.succ) j).pred ⋯ :
              Set (Fin n)))
          i)
        a →
      ∀ ⦃b : Fin n⦄,
        Membership.mem (γ := Set (Fin n))
            ((fun (m : Fin (c.length - 1)) ↦
                (range fun (j : Fin (c.partSize (Fin.cast ⋯ m.succ))) ↦
                    have this := ⋯;
                    (c.emb (Fin.cast this m.succ) j).pred ⋯ :
                  Set (Fin n)))
              j)
            b →
          a ≠ b
have simp : ∀ (a : Fin (c.partSize (Fin.cast sorry i.succ))) (a_1 : Fin (c.partSize (Fin.cast sorry j.succ))),
  ¬c.emb (Fin.cast sorry i.succ) a = c.emb (Fin.cast sorry j.succ) a_1
Tactic: simp only [mem_range, ne_eq, forall_exists_index, forall_apply_eq_imp_iff, pred_inj]
-- 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}
x : Fin n
⊢ ∃ (m : Fin (c.length - 1)) (y : Fin (c.partSize (Fin.cast ⋯ m.succ))), (c.emb (Fin.cast ⋯ m.succ) y).pred ⋯ = x
have obtain : ∀ (i : Fin c.length) (j : Fin (c.partSize i)) (hij : c.emb i j = x.succ),
  ∃ (m : Fin (c.length - 1)) (y : Fin (c.partSize (Fin.cast sorry m.succ))), (c.emb (Fin.cast sorry m.succ) y).pred sorry = x
Tactic: obtain ⟨i, j, hij⟩ : ∃ (i : Fin c.length), ∃ (j : Fin (c.partSize i)), c.emb i j = succ x :=
      ⟨c.index (succ x), c.invEmbedding (succ x), by simp⟩