harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma natDegree_coeff_Φ_ofNat (n : ℕ) :
    (W.Φ n).natDegree ≤ n ^ 2 ∧ (W.Φ n).coeff (n ^ 2) = 1

Proof state:
case succ.succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} => coeff_mul_of_natDegree_le
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' :
  (n + 1 + 1) ^ 2 =
    WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ (W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1

Tactic:
have hc : (1 : ℤ) = 1 * expCoeff (n + 2) ^ 2 * (if Even (n + 1) then 1 else 4) -
    expCoeff (n + 3) * expCoeff (n + 1) * (if Even (n + 1) then 4 else 1) := by
  push_cast [← @Int.cast_inj ℚ, expCoeff_cast, Nat.even_add_one, ite_not]
  split_ifs <;> ring1

Result:
case succ.succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} => natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} => natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} => coeff_mul_of_natDegree_le
h : ∀ {n : ℕ},
  (W.preΨ' n).natDegree ≤ WeierstrassCurve.expDegree n ∧
    (W.preΨ' n).coeff (WeierstrassCurve.expDegree n) = ↑(WeierstrassCurve.expCoeff n) :=
  fun {n} => WeierstrassCurve.natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * WeierstrassCurve.expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' :
  (n + 1 + 1) ^ 2 =
    WeierstrassCurve.expDegree (n + 3) + WeierstrassCurve.expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * WeierstrassCurve.expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      WeierstrassCurve.expCoeff (n + 3) * WeierstrassCurve.expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ (W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_le [LinearOrderedSemiring α] {m n : PosNum} : (m : α) ≤ n ↔ m ≤ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : PosNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Result:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : PosNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
exact not_congr cast_lt

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.integrable_smul_right_of_hasCompactSupport
    [NormedSpace ℝ E] [OpensMeasurableSpace X] [T2Space X] {f : X → ℝ} (hf : LocallyIntegrable f μ)
    {g : X → E} (hg : Continuous g) (h'g : HasCompactSupport g) :
    Integrable (fun x ↦ f x • g x) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
hx : x ∉ K
⊢ f x • g x = 0

Tactic:
simp [image_eq_zero_of_nmem_tsupport hx]

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
⊢ Integrable (fun x => f x • g x) μ

Tactic:
let K := tsupport g

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
⊢ Integrable (fun x => f x • g x) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ (K.indicator fun x => f x • g x) = fun x => f x • g x

Tactic:
apply indicator_eq_self.2

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ (support fun x => f x • g x) ⊆ K
-- Mathlib/Topology/Sheaves/Presheaf.lean
theorem pushforwardEq_hom_app {X Y : TopCat.{w}} {f g : X ⟶ Y}
    (h : f = g) (ℱ : X.Presheaf C) (U) :
    (pushforwardEq h ℱ).hom.app U = ℱ.map (eqToHom (by aesop_cat))

Proof state:
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (pushforwardEq h ℱ).hom.app U = ℱ.map (eqToHom ⋯)

Tactic:
simp [pushforwardEq]

Result:
no goals

Proof state:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u_1
inst✝² : Category.{?u.46617, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map f).op.obj U = (Opens.map g).op.obj U

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
@[simp]
protected lemma zero (μ : Measure α) : 0 ≪ μ := fun _ _ ↦ by simp

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
x✝¹ : Set α
x✝ : μ x✝¹ = 0
⊢ 0 x✝¹ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_mul {a b : ℤ√d} (ha : Nonneg a) (hb : Nonneg b) : Nonneg (a * b) :=
  match a, b, nonneg_cases ha, nonneg_cases hb, ha, hb with
  | _, _, ⟨_, _, Or.inl rfl⟩, ⟨_, _, Or.inl rfl⟩, _, _ => trivial
  | _, _, ⟨x, y, Or.inl rfl⟩, ⟨z, w, Or.inr <| Or.inr rfl⟩, _, hb => nonneg_mul_lem hb
  | _, _, ⟨x, y, Or.inl rfl⟩, ⟨z, w, Or.inr <| Or.inl rfl⟩, _, hb => nonneg_mul_lem hb
  | _, _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ⟨z, w, Or.inl rfl⟩, ha, _ => by
    rw [mul_comm]; exact nonneg_mul_lem ha
  | _, _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ⟨z, w, Or.inl rfl⟩, ha, _ => by
    rw [mul_comm]; exact nonneg_mul_lem ha
  | _, _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ⟨z, w, Or.inr <| Or.inr rfl⟩, ha, hb => by
    rw [calc
          (⟨-x, y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨x * z + d * y * w, -(x * w + y * z)⟩

Proof state:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := ↑z, im := ↑w }).Nonneg

Tactic:
rw [mul_comm]

Result:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := ↑x, im := -↑y }).Nonneg
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.Represents.one : (1 : Matrix ι ι R).Represents b 1

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ Represents b 1 1

Tactic:
delta Matrix.Represents PiToModule.fromMatrix

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b) ∘ₗ algEquivMatrix'.symm.toLinearMap) 1 =
    (PiToModule.fromEnd R b) 1

Proof state:
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
i✝ : ι
⊢ (((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b)) 1 ∘ₗ LinearMap.single R (fun i => R) i✝)
      1 =
    ((PiToModule.fromEnd R b) 1 ∘ₗ LinearMap.single R (fun i => R) i✝) 1

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b)) 1 = (PiToModule.fromEnd R b) 1

Tactic:
ext

Result:
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
i✝ : ι
⊢ (((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b)) 1 ∘ₗ LinearMap.single R (fun i => R) i✝)
      1 =
    ((PiToModule.fromEnd R b) 1 ∘ₗ LinearMap.single R (fun i => R) i✝) 1

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b) ∘ₗ algEquivMatrix'.symm.toLinearMap) 1 =
    (PiToModule.fromEnd R b) 1

Tactic:
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_one]

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ ((LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.linearCombination R R) b)) 1 = (PiToModule.fromEnd R b) 1
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorRightHomEquiv_symm_coevaluation_comp_whiskerRight {Y Y' Z : C} [ExactPairing Y Y']
    (f : Y ⟶ Z) : (tensorRightHomEquiv _ Y _ _).symm (η_ Y Y' ≫ f ▷ Y') = (λ_ _).hom ≫ f :=
  calc
    _ = η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ η_ Y Y' ▷ Y ⊗≫ (Y ◁ ε_ Y Y' ≫ f ▷ 𝟙_ C) ⊗≫ 𝟙 Z = (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom =
    η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f = (λ_ Y).hom ≫ f

Tactic:
rw [evaluation_coevaluation'']

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢  ⊗𝟙.hom ⊗≫ f = (λ_ Y).hom ≫ f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z = (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f

Tactic:
rw [← whisker_exchange]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ η_ Y Y' ▷ Y ⊗≫ (Y ◁ ε_ Y Y' ≫ f ▷ 𝟙_ C) ⊗≫ 𝟙 Z = (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (tensorRightHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ f ▷ Y') = η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z

Tactic:
dsimp [tensorRightHomEquiv]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom =
    η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢  ⊗𝟙.hom ⊗≫ f = (λ_ Y).hom ≫ f

Tactic:
monoidal

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasStrictFDerivAt_list_prod_attach' {l : List ι} {x : {i // i ∈ l} → 𝔸} :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.attach.map x).prod)
      (∑ i : Fin l.length, ((l.attach.take i).map x).prod •
        smulRight (proj l.attach[i.cast List.length_attach.symm])
          ((l.attach.drop (.succ i)).map x).prod) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ ∀ i ∈ Finset.univ,
    (List.map x (List.take (↑i) l.attach)).prod •
        (proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod =
      (List.map x (List.take (↑((finCongr ⋯) i)) l.attach)).prod •
        (proj l.attach[(finCongr ⋯) i]).smulRight (List.map x (List.drop (↑((finCongr ⋯) i)).succ l.attach)).prod

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ HasStrictFDerivAt (fun x => (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l.attach)).prod •
        (proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod)
    x

Tactic:
exact hasStrictFDerivAt_list_prod'.congr_fderiv <| Eq.symm <|
Finset.sum_equiv (finCongr List.length_attach.symm) (by simp) (by simp)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ HasStrictFDerivAt (fun x => (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l.attach)).prod •
        (proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod)
    x

Tactic:
classical exact hasStrictFDerivAt_list_prod'.congr_fderiv <| Eq.symm <|
  Finset.sum_equiv (finCongr List.length_attach.symm) (by simp) (by simp)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ ∀ (i : Fin l.length), i ∈ Finset.univ ↔ (finCongr ⋯) i ∈ Finset.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem disc_eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ P.a * -(x + y + z)) ^ 2 * (φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * φ P.a * (φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (φ P.a * -(x + y + z)) ^ 3 * (φ P.a * -(x * y * z)) -
        27 * φ P.a ^ 2 * (φ P.a * -(x * y * z)) ^ 2 +
      18 * φ P.a * (φ P.a * -(x + y + z)) * (φ P.a * (x * y + x * z + y * z)) * (φ P.a * -(x * y * z)) =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.b ^ 2 * φ P.c ^ 2 - 4 * φ P.a * φ P.c ^ 3 - 4 * φ P.b ^ 3 * φ P.d - 27 * φ P.a ^ 2 * φ P.d ^ 2 +
      18 * φ P.a * φ P.b * φ P.c * φ P.d =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
rw [b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ P.a * -(x + y + z)) ^ 2 * (φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * φ P.a * (φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (φ P.a * -(x + y + z)) ^ 3 * (φ P.a * -(x * y * z)) -
        27 * φ P.a ^ 2 * (φ P.a * -(x * y * z)) ^ 2 +
      18 * φ P.a * (φ P.a * -(x + y + z)) * (φ P.a * (x * y + x * z + y * z)) * (φ P.a * -(x * y * z)) =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
simp only [disc, RingHom.map_add, RingHom.map_sub, RingHom.map_mul, map_pow, map_ofNat]

Result:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.b ^ 2 * φ P.c ^ 2 - 4 * φ P.a * φ P.c ^ 3 - 4 * φ P.b ^ 3 * φ P.d - 27 * φ P.a ^ 2 * φ P.d ^ 2 +
      18 * φ P.a * φ P.b * φ P.c * φ P.d =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem coeff_eq_zero_of_lt_natTrailingDegree {p : R[X]} {n : ℕ} (h : n < p.natTrailingDegree) :
    p.coeff n = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < p.trailingDegree

Tactic:
rw [hp, trailingDegree_zero]

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < ⊤

Proof state:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
⊢ ↑n < p.trailingDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < p.trailingDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < p.trailingDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < p.trailingDegree

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < ↑p.natTrailingDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ ↑n < ↑p.natTrailingDegree

Tactic:
exact WithTop.coe_lt_coe.2 h

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < ⊤

Tactic:
exact WithTop.coe_lt_top n

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
⊢ p.coeff n = 0

Tactic:
apply coeff_eq_zero_of_lt_trailingDegree

Result:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
⊢ ↑n < p.trailingDegree
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem le_add_ge (a : Nat) {b c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b)

Proof state:
a b c : Nat
h : a ≥ c
⊢ (a ≤ b + c) = (a - c ≤ b)

Tactic:
have r := add_le_add_ge 0 b h

Result:
a b c : Nat
h : a ≥ c
r : (0 + a ≤ b + c) = (0 + (a - c) ≤ b)
⊢ (a ≤ b + c) = (a - c ≤ b)

Proof state:
a b c : Nat
h : a ≥ c
r : (0 + a ≤ b + c) = (0 + (a - c) ≤ b)
⊢ (a ≤ b + c) = (a - c ≤ b)

Tactic:
simp only [Nat.zero_add] at r

Result:
a b c : Nat
h : a ≥ c
r : (a ≤ b + c) = (a - c ≤ b)
⊢ (a ≤ b + c) = (a - c ≤ b)

Proof state:
a b c : Nat
h : a ≥ c
r : (a ≤ b + c) = (a - c ≤ b)
⊢ (a ≤ b + c) = (a - c ≤ b)

Tactic:
exact r

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addX_neg (P : Fin 3 → R) : W'.addX P (W'.neg P) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addX P (W'.neg P) = 0

Tactic:
rw [addX, neg_X, neg_Y, neg_Z, negY]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z + P x * P y ^ 2 * P z -
                                2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                              2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z -
                            W'.a₁ * P x ^ 2 * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                2 * W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z + P x * P y ^ 2 * P z -
                                2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                              2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z -
                            W'.a₁ * P x ^ 2 * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * P z ^ 2 +
                  W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z ^ 2 -
                2 * W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * P x ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0

Tactic:
ring1

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem fst_map_snd : (Submodule.fst R M M₂).map (LinearMap.snd R M M₂) = ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M₂
⊢ x ∈ map (snd R M M₂) (fst R M M₂) → x ∈ ⊥

Tactic:
simp only [fst, comap_bot, mem_map, mem_ker, snd_apply, eq_comm, Prod.exists, exists_eq_left,
  exists_const, mem_bot, imp_self]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (snd R M M₂) (fst R M M₂) = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (snd R M M₂) (fst R M M₂) ≤ ⊥

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (snd R M M₂) (fst R M M₂) ≤ ⊥

Tactic:
intro x

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M₂
⊢ x ∈ map (snd R M M₂) (fst R M M₂) → x ∈ ⊥