harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_prod [DecidableEq ι] {s : Multiset ι} {f : ι → R[X]} :
    derivative (Multiset.map f s).prod =
      (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum

Proof state:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ f i * derivative (Multiset.map f s).prod =
    (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
rw [h, ← AddMonoidHom.coe_mulLeft, (AddMonoidHom.mulLeft (f i)).map_multiset_sum _,
  AddMonoidHom.coe_mulLeft]

Result:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map (HMul.hMul (f i))
        (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s)).sum =
    (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Proof state:
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ (Multiset.map f s).prod * derivative (f i) + f i * derivative (Multiset.map f s).prod =
    (Multiset.map f s).prod * derivative (f i) +
      (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum

Tactic:
congr

Result:
case e_a
R : Type u
ι : Type y
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
s✝ : Multiset ι
f : ι → R[X]
i : ι
s : Multiset ι
h :
  derivative (Multiset.map f s).prod =
    (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
⊢ f i * derivative (Multiset.map f s).prod =
    (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitUnopIsoUnopColimit_inv_comp_π (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasColimit F] (j : J) :
    (limitUnopIsoUnopColimit F).inv ≫ limit.π F.unop j = (colimit.ι F (op j)).unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
inst✝ : HasColimit F
j : J
⊢ (limitUnopIsoUnopColimit F).inv ≫ limit.π F.unop j = (colimit.ι F (op j)).unop

Tactic:
simp [limitUnopIsoUnopColimit]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_prod_of_discrete_left [DiscreteTopology α]
    {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨x.1, ·⟩) {b | (x.1, b) ∈ s} x.2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2

Tactic:
rw [← x.eta]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 => f ((x.1, x.2).1, x_1)) {b | ((x.1, x.2).1, b) ∈ s} (x.1, x.2).2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (Prod.mk x.1) (𝓝 x.2 ⊓ 𝓟 (Prod.mk x.1 ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 => f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s (x.1, x.2) ↔
    ContinuousWithinAt (fun x_1 => f ((x.1, x.2).1, x_1)) {b | ((x.1, x.2).1, b) ∈ s} (x.1, x.2).2

Tactic:
simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
← map_inf_principal_preimage]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ Tendsto f (map (Prod.mk x.1) (𝓝 x.2 ⊓ 𝓟 (Prod.mk x.1 ⁻¹' s))) (𝓝 (f (x.1, x.2))) ↔
    Tendsto (fun x_1 => f (x.1, x_1)) (𝓝 x.2 ⊓ 𝓟 {b | (x.1, b) ∈ s}) (𝓝 (f (x.1, x.2)))
-- Mathlib/Data/NNReal/Defs.lean
theorem sSup_of_not_bddAbove {s : Set ℝ≥0} (hs : ¬BddAbove s) : SupSet.sSup s = 0

Proof state:
s : Set ℝ≥0
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
rw [← bddAbove_coe] at hs

Result:
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup s = 0

Proof state:
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup s = 0

Tactic:
rw [← coe_inj, coe_sSup, NNReal.coe_zero]

Result:
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup (toReal '' s) = 0

Proof state:
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup (toReal '' s) = 0

Tactic:
exact sSup_of_not_bddAbove hs

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Cardinality.lean
theorem lift_cardinalMk_le_max : lift.{u} #L ≤ lift.{v} #R ⊔ ℵ₀ :=
  calc
    lift.{u} #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) :=
      lift_cardinalMk_le_sigma_polynomial R L
    _ = Cardinal.sum fun p : R[X] => #{x : L | x ∈ p.aroots L}

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ p.aroots L }) = #((i : R[X]) × ↑{x | x ∈ i.aroots L})

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ p.aroots L }) = sum fun p => #↑{x | x ∈ p.aroots L}

Tactic:
rw [← mk_sigma]

Result:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ p.aroots L }) = #((i : R[X]) × ↑{x | x ∈ i.aroots L})

Proof state:
case h₁.h₁
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} #R[X] ≤ lift.{v, u} (#R ⊔ ℵ₀)

Tactic:
simp only [lift_le, Polynomial.cardinalMk_le_max]

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} #R[X] ⊔ ℵ₀ ⊔ ℵ₀ ≤ lift.{v, u} (#R ⊔ ℵ₀) ⊔ ℵ₀ ⊔ ℵ₀

Tactic:
gcongr

Result:
case h₁.h₁
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} #R[X] ≤ lift.{v, u} (#R ⊔ ℵ₀)

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} (#R ⊔ ℵ₀) ⊔ ℵ₀ ⊔ ℵ₀ = lift.{v, u} #R ⊔ ℵ₀

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ (sum fun x => ℵ₀) = lift.{v, u} #R[X] * ℵ₀

Tactic:
rw [sum_const, lift_aleph0]

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
@[simp] lemma principal_exterior (s : Set α) : 𝓟 (exterior s) = 𝓝ˢ s

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set α
⊢ 𝓟 (exterior s) = 𝓝ˢ s

Tactic:
rw [← nhdsSet_exterior, isOpen_exterior.nhdsSet_eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean
theorem UniversallyInjective.iff_diagonal :
    UniversallyInjective f ↔ Surjective (pullback.diagonal f)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ diagonal (@Surjective) f ↔ Surjective (pullback.diagonal f)

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyInjective f ↔ Surjective (pullback.diagonal f)

Tactic:
rw [universallyInjective_eq_diagonal]

Result:
X Y : Scheme
f : X ⟶ Y
⊢ diagonal (@Surjective) f ↔ Surjective (pullback.diagonal f)
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem diam_Icc {a b : ℝ} (h : a ≤ b) : Metric.diam (Icc a b) = b - a

Proof state:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Icc a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem prehaar_mono {K₀ : PositiveCompacts G} {U : Set G} (hU : (interior U).Nonempty)
    {K₁ K₂ : Compacts G} (h : (K₁ : Set G) ⊆ K₂.1) :
    prehaar (K₀ : Set G) U K₁ ≤ prehaar (K₀ : Set G) U K₂

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ 0 < ↑(index (↑K₀) U)

Tactic:
exact mod_cast index_pos K₀ hU

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) ≤ ↑(index (↑K₂) U)

Tactic:
exact mod_cast index_mono K₂.2 h hU

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ prehaar (↑K₀) U K₁ ≤ prehaar (↑K₀) U K₂

Tactic:
simp only [prehaar]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
rw [div_le_div_iff_of_pos_right]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) ≤ ↑(index (↑K₂) U)

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ 0 < ↑(index (↑K₀) U)
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem card_lt_of_card_biUnion_lt {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β} {c : Cardinal}
    (h : #(⋃ a ∈ s, t a ‹_›) < c) (a : α) (ha : a ∈ s) : # (t a ha) < c

Proof state:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c

Tactic:
have := card_lt_of_card_iUnion_lt h

Result:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
this : ∀ (i : ↑s), #↑(t ↑i ⋯) < c
⊢ #↑(t a ha) < c

Proof state:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
this : ∀ (i : ↑s), #↑(t ↑i ⋯) < c
⊢ #↑(t a ha) < c

Tactic:
simp_all only [iUnion_coe_set,
  Subtype.forall]

Result:
no goals

Proof state:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c

Tactic:
rw [biUnion_eq_iUnion] at h

Result:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem eq_one_of_map_eq_one {S : Type*} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : p.Monic)
    (map_eq : p.map f = 1) : p = 1

Proof state:
case h.e'_3
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ 1 = C (p.coeff 0)

Tactic:
rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ p.degree = 0

Tactic:
rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]

Result:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0

Proof state:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
⊢ p = 1

Tactic:
have hndeg : p.natDegree = 0 :=
  WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)

Result:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ p = 1

Proof state:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
⊢ p = 1

Tactic:
nontriviality R

Result:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ p = 1

Proof state:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0

Tactic:
rw [hp.leadingCoeff, f.map_one]

Result:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 1 ≠ 0

Proof state:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ p = 1

Tactic:
convert eq_C_of_degree_eq_zero hdeg

Result:
case h.e'_3
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ 1 = C (p.coeff 0)
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffAt.differentiableAt (h : ContDiffAt 𝕜 n f x) (hn : 1 ≤ n) :
    DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffAt 𝕜 n f x
hn : 1 ≤ n
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa [hn, differentiableWithinAt_univ] using h.differentiableWithinAt

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem disjoint_finset_sum_left {β : Type*} {i : Finset β} {f : β → Multiset α} {a : Multiset α} :
    Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a

Proof state:
case h.e'_2.a
α : Type u_3
β : Type u_6
i : Finset β
f : β → Multiset α
a : Multiset α
⊢ (∀ b ∈ i, Disjoint (f b) a) ↔ ∀ b ∈ map f i.val, Disjoint b a

Tactic:
simp [and_congr_left_iff]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_6
i : Finset β
f : β → Multiset α
a : Multiset α
⊢ Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a

Tactic:
convert @disjoint_sum_left _ a (map f i.val)

Result:
case h.e'_2.a
α : Type u_3
β : Type u_6
i : Finset β
f : β → Multiset α
a : Multiset α
⊢ (∀ b ∈ i, Disjoint (f b) a) ↔ ∀ b ∈ map f i.val, Disjoint b a
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.continuousLinearMap_comp (g : F →L[𝕜] G)
    (hf : ContDiffWithinAt 𝕜 n f s x) : ContDiffWithinAt 𝕜 n (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
x : E
n✝ : WithTop ℕ∞
g : F →L[𝕜] G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (⇑g ∘ f) p u

Tactic:
rcases hf m hm with ⟨u, hu, p, hp⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
x : E
n✝ : WithTop ℕ∞
g : F →L[𝕜] G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (⇑g ∘ f) p u

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
x : E
n✝ : WithTop ℕ∞
g : F →L[𝕜] G
n : ℕ∞
hf : ContDiffWithinAt 𝕜 (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (⇑g ∘ f) p u

Tactic:
exact ⟨u, hu, _, hp.continuousLinearMap_comp g⟩

Result:
no goals
-- Mathlib/Algebra/Lie/EngelSubalgebra.lean
lemma self_mem_engel (x : L) : x ∈ engel R x

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ((ad R L) x ^ 1) x = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, ((ad R L) x ^ n) x = 0

Tactic:
exact ⟨1, by simp⟩

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ x ∈ engel R x

Tactic:
simp only [mem_engel_iff]

Result:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ∃ n, ((ad R L) x ^ n) x = 0
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
theorem HasDerivWithinAt.clog {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ} (h₁ : HasDerivWithinAt f f' s x)
    (h₂ : f x ∈ slitPlane) : HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x

Proof state:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x

Tactic:
rw [div_eq_inv_mul]

Result:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t => log (f t)) ((f x)⁻¹ * f') s x

Proof state:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t => log (f t)) ((f x)⁻¹ * f') s x

Tactic:
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp_hasDerivWithinAt x h₁

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
theorem range_toLpHom [Fact (1 ≤ p)] :
    ((toLpHom p μ).range : AddSubgroup (Lp E p μ)) =
      MeasureTheory.Lp.boundedContinuousFunction E p μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
⊢ Lp.boundedContinuousFunction E p μ = (toLpHom p μ).range

Tactic:
exact AddMonoidHom.addSubgroupOf_range_eq_of_le
    ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E))
    (by rintro - ⟨f, rfl⟩; exact mem_Lp f : _ ≤ Lp E p μ)

Result:
no goals

Proof state:
case intro
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
f : α →ᵇ E
⊢ ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E)) f ∈ Lp E p μ

Tactic:
exact mem_Lp f

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
⊢ ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E)).range ≤ Lp E p μ

Tactic:
rintro - ⟨f, rfl⟩

Result:
case intro
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
f : α →ᵇ E
⊢ ((ContinuousMap.toAEEqFunAddHom μ).comp (toContinuousMapAddHom α E)) f ∈ Lp E p μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
⊢ (toLpHom p μ).range = Lp.boundedContinuousFunction E p μ

Tactic:
symm

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopologyEither α E
inst✝¹ : IsFiniteMeasure μ
inst✝ : Fact (1 ≤ p)
⊢ Lp.boundedContinuousFunction E p μ = (toLpHom p μ).range
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_to_volumeForm (x y : E) : ω x y = o.volumeForm ![x, y]

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y = o.volumeForm ![x, y]

Tactic:
simp [areaForm]

Result:
no goals
-- Mathlib/Data/Multiset/NatAntidiagonal.lean
theorem antidiagonal_succ {n : ℕ} :
    antidiagonal (n + 1) = (0, n + 1) ::ₘ (antidiagonal n).map (Prod.map Nat.succ id)

Proof state:
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) ::ₘ map (Prod.map Nat.succ id) (antidiagonal n)

Tactic:
simp only [antidiagonal, List.Nat.antidiagonal_succ, map_coe, cons_coe]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_natAbs_eq_min [hpos : NeZero n] (a : ZMod n) :
    a.valMinAbs.natAbs = min a.val (n - a.val)

Proof state:
n : ℕ
hpos : NeZero n
a : ZMod n
⊢ (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = a.val ⊓ (n - a.val)

Tactic:
have := a.val_lt

Result:
n : ℕ
hpos : NeZero n
a : ZMod n
this : a.val < n
⊢ (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = a.val ⊓ (n - a.val)

Proof state:
n : ℕ
hpos : NeZero n
a : ZMod n
⊢ a.valMinAbs.natAbs = a.val ⊓ (n - a.val)

Tactic:
rw [valMinAbs_def_pos]

Result:
n : ℕ
hpos : NeZero n
a : ZMod n
⊢ (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = a.val ⊓ (n - a.val)

Proof state:
n : ℕ
hpos : NeZero n
a : ZMod n
this : a.val < n
⊢ (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = a.val ⊓ (n - a.val)

Tactic:
omega

Result:
no goals