awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos_1 : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin qlength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin qlength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin qlength), x ∈ range (qemb m)
hpq :
  embSigma n
      { length := plength, partSize := psize, partSize_pos := partSize_pos, emb := pemb,
        emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover :
        OrderedFinpartition n } =
    embSigma n
      { length := qlength, partSize := qsize, partSize_pos := partSize_pos_1, emb := qemb,
        emb_strictMono := emb_strictMono_1, parts_strictMono := parts_strictMono_1, disjoint := disjoint_1,
        cover := cover_1 }
⊢ { length := plength, partSize := psize, partSize_pos := partSize_pos, emb := pemb, emb_strictMono := emb_strictMono,
      parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover : OrderedFinpartition n } =
    { length := qlength, partSize := qsize, partSize_pos := partSize_pos_1, emb := qemb,
      emb_strictMono := emb_strictMono_1, parts_strictMono := parts_strictMono_1, disjoint := disjoint_1,
      cover := cover_1 }
have simp_all : ∀
  (hpq :
    plength = qlength ∧
      HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
        (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
          (fun (m : Fin plength) ↦ ⟨psize m, sorry⟩) fun (j : Fin plength) ↦ pemb j)
        (β := (p : Fin qlength → Fin (n + 1)) × ((i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n))
        (Sigma.mk (β := fun (p : Fin qlength → Fin (n + 1)) ↦ (i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n)
          (fun (m : Fin qlength) ↦ ⟨qsize m, sorry⟩) fun (j : Fin qlength) ↦ qemb j)),
  psize ≍ qsize ∧ pemb ≍ qemb
Tactic: simp_all only [Sigma.mk.inj_iff, true_and, mk.injEq, Fin.mk.injEq, embSigma]
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos_1 : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin qlength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin qlength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin qlength), x ∈ range (qemb m)
hpq :
  plength = qlength ∧
    HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
      (β := (p : Fin qlength → Fin (n + 1)) × ((i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin qlength → Fin (n + 1)) ↦ (i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin qlength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin qlength) ↦ qemb j)
⊢ psize ≍ qsize ∧ pemb ≍ qemb
have this : plength = qlength
Tactic: have : plength = qlength := hpq.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qlength : ℕ
qsize : Fin qlength → ℕ
partSize_pos_1 : ∀ (m : Fin qlength), 0 < qsize m
qemb : (m : Fin qlength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin qlength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin qlength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin qlength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin qlength), x ∈ range (qemb m)
hpq :
  plength = qlength ∧
    HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
      (β := (p : Fin qlength → Fin (n + 1)) × ((i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin qlength → Fin (n + 1)) ↦ (i : Fin qlength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin qlength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin qlength) ↦ qemb j)
this : plength = qlength
⊢ psize ≍ qsize ∧ pemb ≍ qemb
have subst : ∀ (qsize : Fin plength → ℕ) (partSize_pos_2 : ∀ (m : Fin plength), 0 < qsize m)
  (qemb : (m : Fin plength) → Fin (qsize m) → Fin n) (emb_strictMono_2 : ∀ (m : Fin plength), StrictMono (qemb m))
  (parts_strictMono_2 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, sorry⟩ : Fin (qsize m)))
  (disjoint_2 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m))
  (cover_2 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m))
  (hpq :
    plength = plength ∧
      HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
        (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
          (fun (m : Fin plength) ↦ ⟨psize m, sorry⟩) fun (j : Fin plength) ↦ pemb j)
        (β := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
        (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
          (fun (m : Fin plength) ↦ ⟨qsize m, sorry⟩) fun (j : Fin plength) ↦ qemb j)),
  psize ≍ qsize ∧ pemb ≍ qemb
Tactic: subst this
Cleared hypotheses: qlength, qsize, partSize_pos_1, qemb, emb_strictMono_1, parts_strictMono_1, disjoint_1, cover_1, hpq, this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos_1 : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m)
hpq :
  plength = plength ∧
    HEq (α := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (j : Fin plength) ↦ pemb j)
      (β := (p : Fin plength → Fin (n + 1)) × ((i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n))
      (Sigma.mk (β := fun (p : Fin plength → Fin (n + 1)) ↦ (i : Fin plength) → Fin (↑(p i) : ℕ) → Fin n)
        (fun (m : Fin plength) ↦ ⟨qsize m, ⋯⟩) fun (j : Fin plength) ↦ qemb j)
⊢ psize ≍ qsize ∧ pemb ≍ qemb
have simp_all : ∀
  (hpq :
    (Eq (α := Fin plength → Fin (n + 1)) (fun (m : Fin plength) ↦ ⟨psize m, sorry⟩) fun (m : Fin plength) ↦ ⟨qsize m, sorry⟩) ∧
      HEq (α := (i : Fin plength) → Fin (psize i) → Fin n) fun (j : Fin plength) ↦ pemb j (β :=
        (i : Fin plength) → Fin (qsize i) → Fin n) fun (j : Fin plength) ↦ qemb j),
  psize = qsize
Tactic: simp_all only [Sigma.mk.inj_iff, heq_eq_eq, true_and, and_true]
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono : StrictMono (β := Fin n) fun (m : Fin plength) ↦ pemb m (⟨psize m - 1, ⋯⟩ : Fin (psize m))
disjoint : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (pemb m)
cover : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos_1 : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono_1 : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono_1 : StrictMono (β := Fin n) fun (m : Fin plength) ↦ qemb m (⟨qsize m - 1, ⋯⟩ : Fin (qsize m))
disjoint_1 : PairwiseDisjoint (α := Set (Fin n)) univ fun (m : Fin plength) ↦ range (qemb m)
cover_1 : ∀ (x : Fin n), ∃ (m : Fin plength), x ∈ range (qemb m)
hpq :
  (Eq (α := Fin plength → Fin (n + 1)) (fun (m : Fin plength) ↦ ⟨psize m, ⋯⟩) fun (m : Fin plength) ↦ ⟨qsize m, ⋯⟩) ∧
    HEq (α := (i : Fin plength) → Fin (psize i) → Fin n) fun (j : Fin plength) ↦ pemb j (β :=
      (i : Fin plength) → Fin (qsize i) → Fin n) fun (j : Fin plength) ↦ qemb j
⊢ psize = qsize
have h : ∀ (i : Fin plength), psize i = qsize i
Tactic: ext i
-- 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 : OrderedFinpartition n
⊢ Unique (OrderedFinpartition 0)
have this : Subsingleton (OrderedFinpartition 0)
Tactic: have : Subsingleton (OrderedFinpartition 0) :=
    Fintype.card_le_one_iff_subsingleton.mp (Fintype.card_le_of_injective _ (injective_embSigma 0))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
j : Fin n
⊢ ∃ (p : (m : Fin c.length) × Fin (c.partSize m)),
    c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
        (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))) =
      j
have rcases : ∀ (m : Fin c.length) (r : Fin (c.partSize m)) (hmr : c.emb m r = j),
  ∃ (p : (m : Fin c.length) × Fin (c.partSize m)),
    c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
        (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))) =
      j
Tactic: rcases c.cover j with ⟨m, r, hmr⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
⊢ m = m'
have contrapose! : ∀ (h : m ≠ m'), c.emb m r ≠ c.emb m' r'
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : m ≠ m'
⊢ c.emb m r ≠ c.emb m' r'
have A : Disjoint (range (c.emb m)) (range (c.emb m'))
Tactic: have A : Disjoint (range (c.emb m)) (range (c.emb m')) :=
      c.disjoint (mem_univ m) (mem_univ m') h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
⊢ Eq (α := (m : Fin c.length) × Fin (c.partSize m)) (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r)
    (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m' r')
have this : m = m'
Tactic: have : m = m' := by
    contrapose! h
    have A : Disjoint (range (c.emb m)) (range (c.emb m')) :=
      c.disjoint (mem_univ m) (mem_univ m') h
    apply disjoint_iff_forall_ne.1 A (mem_range_self r) (mem_range_self r')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
r : Fin (c.partSize m)
m' : Fin c.length
r' : Fin (c.partSize m')
h : c.emb m r = c.emb m' r'
this : m = m'
⊢ Eq (α := (m : Fin c.length) × Fin (c.partSize m)) (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r)
    (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m' r')
have subst : ∀ (r' : Fin (c.partSize m)) (h : c.emb m r = c.emb m r'),
  Eq (α := (m : Fin c.length) × Fin (c.partSize m)) (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r)
    (Sigma.mk (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)) m r')
Tactic: subst this
Cleared hypotheses: m', r', h, 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 : OrderedFinpartition n
x : (i : Fin c.length) × Fin (c.partSize i)
⊢ (fun (i : Fin n) ↦
        (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)) (c.index i) (c.invEmbedding i) :
          (i : Fin c.length) × Fin (c.partSize i)))
      ((fun (p : (i : Fin c.length) × Fin (c.partSize i)) ↦
          c.emb (p.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
            (p.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i))))
        x) =
    x
have a : Eq (α := Fin n)
  ((fun (p : (m : Fin c.length) × Fin (c.partSize m)) ↦
      c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
        (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))))
    ((fun (i : Fin n) ↦
        (Sigma.mk (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)) (c.index i) (c.invEmbedding i) :
          (i : Fin c.length) × Fin (c.partSize i)))
      ((fun (p : (i : Fin c.length) × Fin (c.partSize i)) ↦
          c.emb (p.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
            (p.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i))))
        x)))
  ((fun (p : (m : Fin c.length) × Fin (c.partSize m)) ↦
      c.emb (p.fst (β := fun (m : Fin c.length) ↦ Fin (c.partSize m)))
        (p.snd (β := fun (m : Fin c.length) ↦ Fin (c.partSize m))))
    x)
Tactic: apply c.emb_injective
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
α : Type u_5
inst : CommMonoid α
v : Fin n → α
⊢ Eq.{u_5 + 1} (α := α) (∏ m : Fin c.length, ∏ r : Fin (c.partSize m), v (c.emb m r)) (∏ i : Fin n, v i)
have rw : Eq.{u_5 + 1} (α := α)
  (∏
    x ∈
      Finset.sigma (α := fun (a : Fin c.length) ↦ Fin (c.partSize a)) Finset.univ fun (m : Fin c.length) ↦ Finset.univ,
    v
      (c.emb (x.fst (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))
        (x.snd (β := fun (i : Fin c.length) ↦ Fin (c.partSize i)))))
  (∏ i : Fin n, v i)
Tactic: rw [Finset.prod_sigma']
-- 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 1
⊢ c = default
have h₁ : c.length = 1
Tactic: have h₁ : c.length = 1 := le_antisymm c.length_le (c.length_pos Nat.zero_lt_one)
-- 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 1
h₁ : c.length = 1
⊢ c = default
have h₂ : ∀ (i : Fin c.length), c.partSize i = 1
Tactic: have h₂ (i) : c.partSize i = 1 := le_antisymm (c.partSize_le _) (c.partSize_pos _)
-- 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 1
h₁ : c.length = 1
h₂ : ∀ (i : Fin c.length), c.partSize i = 1
⊢ c = default
have h₃ : ∀ (i : Fin c.length) (j : Fin (c.partSize i)), c.emb i j = 0
Tactic: have h₃ (i j) : c.emb i j = 0 := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
inst : NeZero n
⊢ c.emb (c.index 0) 0 = 0
have apply : c.emb (c.index 0) 0 ≤ 0
Tactic: apply le_antisymm _ (Fin.zero_le _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
inst : NeZero n
| 0
have rw : c.emb (c.index 0) (c.invEmbedding 0)
Tactic: rw [← c.emb_invEmbedding 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition n
inst : NeZero n
⊢ c.emb (c.index 0) 0 ≤ 0
have conv_rhs : c.emb (c.index 0) 0 ≤ c.emb (c.index 0) (c.invEmbedding 0)
Tactic: conv_rhs => rw [← c.emb_invEmbedding 0]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition n
i : Fin c.length
j : Fin n
hc : range (c.emb i) = {j}
⊢ c.partSize i = 1
have this : Fintype.card (↑(range (c.emb i)) : Type) = Fintype.card (Fin (c.partSize i))
Tactic: have : Fintype.card (range (c.emb i)) = Fintype.card (Fin (c.partSize i)) :=
    card_range_of_injective (c.emb_strictMono i).injective
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
⊢ c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have rw : c.partSize (c.index 0) = Nat.card (Fin (c.partSize (c.index 0)))
Tactic: rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
⊢ 1 < c.partSize (c.index 0)
have this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
Tactic: have : c.partSize (c.index 0) = Nat.card (range (c.emb (c.index 0))) := by
    rw [Nat.card_range_of_injective (c.emb_strictMono _).injective]; simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
⊢ 1 < c.partSize (c.index 0)
have rw : 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
⊢ 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have inl : ∀ (h : c.index 0 = 0), 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
Tactic: rcases eq_or_ne (c.index 0) 0 with h | h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
inl : ∀ (h : c.index 0 = 0), 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
⊢ 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have inr : ∀ (h : c.index 0 ≠ 0), 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
Tactic: rcases eq_or_ne (c.index 0) 0 with h | h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize 0)) (c.emb 0) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
⊢ 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have hc₁ : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
Tactic: rw [← h] at hc
Cleared hypotheses: hc, this, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (goal)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
⊢ {0} ⊂ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
have apply : {0} ⊆ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
Tactic: apply ssubset_of_subset_of_ne ?_ hc.symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno (hypothesis)
Goal:
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0)) ≠ {0}
this : c.partSize (c.index 0) = Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
h : c.index 0 = 0
⊢ 1 < Nat.card (↑(range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))) : Type)
have this₁ : {0} ⊂ range (ι := Fin (c.partSize (c.index 0))) (c.emb (c.index 0))
Tactic: have : {0} ⊂ range (c.emb (c.index 0)) := by
      apply ssubset_of_subset_of_ne ?_ hc.symm
      simpa only [singleton_subset_iff, mem_range] using ⟨0, emb_zero c⟩