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 i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
inl :
  ∀ (h : i ≠ j),
    onFun (β := Set (Fin (n + 1))) Disjoint
      (fun (m : Fin c.length) ↦
        range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m))
          (if h : m = j then
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m = c.partSize j + 1 :=
              ⋯;
            (fun (i : Fin (c.partSize j + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
              Fin.cast this
          else
            have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m = c.partSize m := ⋯;
            succ ∘ c.emb m ∘ Fin.cast this))
      i j
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      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 j
have inr : ∀ (hj : j ≠ k),
  onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      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 :=
            sorry;
          (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 := sorry;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
Tactic: rcases eq_or_ne j k with rfl | hj
-- 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
i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij h : i ≠ j
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m))
        (if h : m = j then
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m = c.partSize j + 1 :=
            ⋯;
          (fun (i : Fin (c.partSize j + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
            Fin.cast this
        else
          have this : update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) m = c.partSize m := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j
have inl : Disjoint (α := Set (Fin (n + 1)))
  (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
    (if h : i = j then
      (fun (i : Fin (c.partSize j + 1)) ↦
          cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
        Fin.cast sorry
    else succ ∘ c.emb i ∘ Fin.cast sorry))
  (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
    ((fun (i : Fin (c.partSize j + 1)) ↦
        cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
      Fin.cast sorry))
Tactic: simp only [onFun, ↓reduceDIte]
-- 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
i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij h : i ≠ j
this :
  ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
    (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
⊢ Disjoint (α := Set (Fin (n + 1)))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
      (if h : i = j then
        (fun (i : Fin (c.partSize j + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
          Fin.cast ⋯
      else succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
      ((fun (i : Fin (c.partSize j + 1)) ↦
          cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
        Fin.cast ⋯))
have apply : ∀ ⦃a : Fin (n + 1)⦄,
  Membership.mem (γ := Set (Fin (n + 1)))
      (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
        (if h : i = j then
          (fun (i : Fin (c.partSize j + 1)) ↦
              cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
            Fin.cast sorry
        else succ ∘ c.emb i ∘ Fin.cast sorry))
      a →
    ∀ ⦃b : Fin (n + 1)⦄,
      Membership.mem (γ := Set (Fin (n + 1)))
          (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
            ((fun (i : Fin (c.partSize j + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
              Fin.cast sorry))
          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 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij h : i ≠ j
this :
  ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
    (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
⊢ ∀ ⦃a : Fin (n + 1)⦄,
    Membership.mem (γ := Set (Fin (n + 1)))
        (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
          (if h : i = j then
            (fun (i : Fin (c.partSize j + 1)) ↦
                cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
              Fin.cast ⋯
          else succ ∘ c.emb i ∘ Fin.cast ⋯))
        a →
      ∀ ⦃b : Fin (n + 1)⦄,
        Membership.mem (γ := Set (Fin (n + 1)))
            (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
              ((fun (i : Fin (c.partSize j + 1)) ↦
                  cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
                Fin.cast ⋯))
            b →
          a ≠ b
have simp : ∀ (a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
  (a_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j)),
  ¬(c.emb i (Fin.cast sorry a)).succ =
      cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) (Fin.cast sorry a_1)
Tactic: simp only [hij, ↓reduceDIte, mem_range, comp_apply, ne_eq, forall_exists_index,
          forall_apply_eq_imp_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 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij h : i ≠ j
⊢ Disjoint (α := Set (Fin (n + 1)))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) i))
      (if h : i = j then
        (fun (i : Fin (c.partSize j + 1)) ↦
            cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
          Fin.cast ⋯
      else succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize j (c.partSize j + 1) j))
      ((fun (i : Fin (c.partSize j + 1)) ↦
          cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) i) ∘
        Fin.cast ⋯))
have inl : ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
  (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
Tactic: suffices ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)),
          succ (c.emb i a') ≠ cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b' by
        apply Set.disjoint_iff_forall_ne.2
        simp only [hij, ↓reduceDIte, mem_range, comp_apply, ne_eq, forall_exists_index,
          forall_apply_eq_imp_iff]
        intro a b
        apply 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 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij h : i ≠ j
a' : Fin (c.partSize i)
b' : Fin (c.partSize j)
h_1 :
  (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.castSucc
⊢ (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.succ
have inl : ¬c.emb i a' = c.emb j b'
Tactic: simp only [cases_succ, comp_apply, ne_eq, succ_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 c : OrderedFinpartition n
i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij h : i ≠ j
a' : Fin (c.partSize i)
b' : Fin (c.partSize j + 1)
⊢ (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
have inl : (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) 0
Tactic: induction b' using Fin.induction with
      | zero => simp
      | succ b' =>
        simp only [cases_succ, comp_apply, ne_eq, succ_inj]
        apply c.emb_ne_emb_of_ne hij
Cleared hypotheses: b'
-- 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
i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj : Membership.mem (γ := Set (Fin c.length)) univ j
hij h : i ≠ j
a' : Fin (c.partSize i)
b' : Fin (c.partSize j + 1)
inl : (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) 0
⊢ (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'
have inl₁ : ∀ (b' : Fin (c.partSize j)),
  (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.castSucc →
    (c.emb i a').succ ≠ cases (motive := fun (x : Fin (c.partSize j + 1)) ↦ Fin (n + 1)) 0 (succ ∘ c.emb j) b'.succ
Tactic: induction b' using Fin.induction with
      | zero => simp
      | succ b' =>
        simp only [cases_succ, comp_apply, ne_eq, succ_inj]
        apply c.emb_ne_emb_of_ne hij
Cleared hypotheses: b'
-- 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 i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
⊢ onFun (β := Set (Fin (n + 1))) Disjoint
    (fun (m : Fin c.length) ↦
      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 j
have inr : Disjoint
  (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
    (succ ∘ c.emb i ∘ Fin.cast sorry))
  (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
    (succ ∘ c.emb j ∘ Fin.cast sorry))
Tactic: simp only [onFun, h, ↓reduceDIte, hj]
-- 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 i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
⊢ Disjoint
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
      (succ ∘ c.emb i ∘ Fin.cast ⋯))
    (range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
      (succ ∘ c.emb j ∘ Fin.cast ⋯))
have inr : ∀ ⦃a : Fin (n + 1)⦄,
  a ∈
      range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
        (succ ∘ c.emb i ∘ Fin.cast sorry) →
    ∀ ⦃b : Fin (n + 1)⦄,
      b ∈
          range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
            (succ ∘ c.emb j ∘ Fin.cast sorry) →
        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 c : OrderedFinpartition n
k i : Fin c.length
hi : Membership.mem (γ := Set (Fin c.length)) univ i
j : Fin c.length
hj_1 : Membership.mem (γ := Set (Fin c.length)) univ j
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
⊢ ∀ ⦃a : Fin (n + 1)⦄,
    a ∈
        range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
          (succ ∘ c.emb i ∘ Fin.cast ⋯) →
      ∀ ⦃b : Fin (n + 1)⦄,
        b ∈
            range (ι := Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j))
              (succ ∘ c.emb j ∘ Fin.cast ⋯) →
          a ≠ b
have inr : ∀ (a : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) i))
  (a_1 : Fin (update (β := fun (a : Fin c.length) ↦ ℕ) c.partSize k (c.partSize k + 1) j)),
  ¬c.emb i (Fin.cast sorry a) = c.emb j (Fin.cast sorry a_1)
Tactic: simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
        succ_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 c : OrderedFinpartition n
k : Fin c.length
⊢ ∀ (x : Fin (n + 1)),
    ∃ (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))
        x
have refine_1 : ∃ (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 := sorry;
        (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 := sorry;
        succ ∘ c.emb m ∘ Fin.cast this))
    0
Tactic: refine Fin.cases ?_ (fun i ↦ ?_)
-- 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
refine_1 :
  ∃ (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
⊢ ∀ (x : Fin (n + 1)),
    ∃ (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))
        x
have refine_2 : ∀ (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 :=
            sorry;
          (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 := sorry;
          succ ∘ c.emb m ∘ Fin.cast this))
      i.succ
Tactic: refine Fin.cases ?_ (fun i ↦ ?_)