harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_const_apply (c : F) : fderivWithin 𝕜 (fun _ => c) s x = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun x => c) s x = 0

Tactic:
rw [fderivWithin, if_pos]

Result:
case hc
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
c : F
⊢ HasFDerivWithinAt (fun x => c) 0 s x

Proof state:
case hc
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
c : F
⊢ HasFDerivWithinAt (fun x => c) 0 s x

Tactic:
apply hasFDerivWithinAt_const

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem _root_.LinearMap.IsSymmetric.isSelfAdjoint {A : E →L[𝕜] E}
    (hA : (A : E →ₗ[𝕜] E).IsSymmetric) : IsSelfAdjoint A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
A : E →L[𝕜] E
hA : (↑A).IsSymmetric
⊢ IsSelfAdjoint A

Tactic:
rwa [← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] at hA

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppScalarLeft_apply_tmul_apply (p : ι →₀ R) (n : N) (i : ι) :
    finsuppScalarLeft R N ι (p ⊗ₜ[R] n) i = p i • n

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = p i • n

Tactic:
simp [finsuppScalarLeft]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem one_mul (a : R) : (nat_lit 1).rawCast * a = a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ Nat.rawCast 1 * a = a

Tactic:
simp [Nat.rawCast]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
lemma range_eq_range_of_surjective {S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y)
    [Surjective e] (hge : e ≫ g = f) : Set.range f.base = Set.range g.base

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
⊢ Set.range ⇑(ConcreteCategory.hom (e ≫ g).base) = Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
simp [Set.range_comp]

Result:
no goals

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
⊢ Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
rw [← hge]

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
e : X ⟶ Y
inst✝ : Surjective e
hge : e ≫ g = f
⊢ Set.range ⇑(ConcreteCategory.hom (e ≫ g).base) = Set.range ⇑(ConcreteCategory.hom g.base)
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_eq_univ [Fintype α] [Fintype s] : s.toFinset = Finset.univ ↔ s = univ

Proof state:
α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ s.toFinset = Finset.univ ↔ s = univ

Tactic:
rw [← coe_inj, coe_toFinset, coe_univ]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_inf_right_comm (x y z : α) : x \ z ⊓ y = (x ⊓ y) \ z

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x \ z ⊓ y = (x ⊓ y) \ z

Tactic:
rw [inf_comm x, inf_comm, inf_sdiff_assoc]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_mul_eq_mk'_of_mul (x₁ x₂) (y : S) : f.mk' x₂ y * f.toMap x₁ = f.mk' (x₁ * x₂) y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y : ↥S
⊢ f.mk' x₂ y * f.toMap x₁ = f.mk' (x₁ * x₂) y

Tactic:
rw [mul_comm, mul_mk'_eq_mk'_of_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem some_eq_ite_none_left {p : Prop} [Decidable p] {b : Option β} :
    some a = (if p then none else b) ↔ ¬ p ∧ some a = b

Proof state:
β : Type u_1
a : β
p : Prop
inst✝ : Decidable p
b : Option β
⊢ (some a = if p then none else b) ↔ ¬p ∧ some a = b

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
lemma le_degrees_add_right (h : Disjoint p.degrees q.degrees) : q.degrees ≤ (p + q).degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ q.degrees ≤ (p + q).degrees

Tactic:
simpa [add_comm] using le_degrees_add_left h.symm

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_sq_add_cos_sq : sin x ^ 2 + cos x ^ 2 = 1 :=
  ofReal_injective (by simp [sin_sq_add_cos_sq])

Proof state:
x : ℝ
⊢ ↑(sin x ^ 2 + cos x ^ 2) = ↑1

Tactic:
simp [sin_sq_add_cos_sq]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_norm_right : (f =Θ[l] fun x ↦ ‖g' x‖) ↔ f =Θ[l] g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =Θ[l] fun x => ‖g' x‖) ↔ f =Θ[l] g'

Tactic:
simp [IsTheta]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem symm_trans_symm (e e' : Pretrivialization F proj) :
    (e.toPartialEquiv.symm.trans e'.toPartialEquiv).symm
      = e'.toPartialEquiv.symm.trans e.toPartialEquiv

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).symm = e'.symm.trans e.toPartialEquiv

Tactic:
rw [PartialEquiv.trans_symm_eq_symm_trans_symm, PartialEquiv.symm_symm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_iUnion_ae [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s))
    (hm : ∀ i, NullMeasurableSet (s i) μ) : μ.restrict (⋃ i, s i) = sum fun i => μ.restrict (s i) :=
  ext fun t ht => by simp only [sum_apply _ ht, restrict_iUnion_apply_ae hd hm ht]

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = (sum fun i => μ.restrict (s i)) t

Tactic:
simp only [sum_apply _ ht, restrict_iUnion_apply_ae hd hm ht]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma zero_eq_mul : 0 = m * n ↔ m = 0 ∨ n = 0

Proof state:
m n : ℕ
⊢ 0 = m * n ↔ m = 0 ∨ n = 0

Tactic:
rw [eq_comm, Nat.mul_eq_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_ceil_right_pure_floor_add_one (x : α) :
    Tendsto (ceil : α → ℤ) (𝓝[>] x) (pure (⌊x⌋ + 1)) :=
  have : ↑(⌊x⌋ + 1) - 1 ≤ x

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌊x⌋ + 1) - 1 ≤ x

Tactic:
rw [cast_add, cast_one, add_sub_cancel_right]

Result:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌊x⌋ ≤ x

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌊x⌋ ≤ x

Tactic:
exact floor_le _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem cond_eq_ite (c : Bool) (a b : α) : cond c a b = ite c a b

Proof state:
α : Type u_1
c : Bool
a b : α
⊢ (bif c then a else b) = if c = true then a else b

Tactic:
cases c <;> simp [*]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem nodup_sublists {l : List α} : Nodup (sublists l) ↔ Nodup l :=
  ⟨fun h => (h.sublist (map_pure_sublist_sublists _)).of_map _, fun h =>
    (pairwise_sublists h).imp @fun l₁ l₂ h => by simpa using h.to_ne⟩

Proof state:
α : Type u
l : List α
h✝ : l.Nodup
l₁ l₂ : List α
h : ((Lex fun x1 x2 => x1 ≠ x2) on reverse) l₁ l₂
⊢ l₁ ≠ l₂

Tactic:
simpa using h.to_ne

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma ιMapObj_iso_inv (i : I) (hi : p i = j) :
    X.ιMapObj p i j hi ≫ (c.iso hc).inv = c.inj ⟨i, hi⟩

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{u_5, u_4} C
X : GradedObject I C
p : I → J
j : J
inst✝ : X.HasMap p
c : X.CofanMapObjFun p j
hc : IsColimit c
i : I
hi : p i = j
⊢ X.ιMapObj p i j hi ≫ (iso hc).inv = Cofan.inj c ⟨i, hi⟩

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_inv

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem ofNat_iff {α β σ} [Denumerable α] [Denumerable β] [Primcodable σ] {f : α → β → σ} :
    Primrec₂ f ↔ Primrec₂ fun m n : ℕ => f (ofNat α m) (ofNat β n) :=
  (Primrec.ofNat_iff.trans <| by simp).trans unpaired

Proof state:
α : Type u_4
β : Type u_5
σ : Type u_6
inst✝² : Denumerable α
inst✝¹ : Denumerable β
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec fun n => f (ofNat (α × β) n).1 (ofNat (α × β) n).2) ↔
    Primrec (Nat.unpaired fun m n => f (ofNat α m) (ofNat β n))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_append_getElem (l : List α) (i : Nat) (h : i < l.length) :
    (l.take i) ++ [l[i]] = l.take (i+1)

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ take i l ++ [l[i]] = take (i + 1) l

Tactic:
simpa using take_concat_get l i h

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem exists_associated_prime_pow_of_unique_normalized_factor {p r : α}
    (h : ∀ {m}, m ∈ normalizedFactors r → m = p) (hr : r ≠ 0) : ∃ i : ℕ, Associated (p ^ i) r

Proof state:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ p ^ (normalizedFactors r).card ~ᵤ r

Tactic:
have := UniqueFactorizationMonoid.prod_normalizedFactors hr

Result:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (normalizedFactors r).prod ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ ∃ i, p ^ i ~ᵤ r

Tactic:
use (normalizedFactors r).card

Result:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ p ^ (normalizedFactors r).card ~ᵤ r

Proof state:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
this : (normalizedFactors r).prod ~ᵤ r
⊢ p ^ (normalizedFactors r).card ~ᵤ r

Tactic:
rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_eq_some_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} :
    m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a fallback : α
⊢ m.contains a = true → m.getKey? a = some (m.getKeyD a fallback)

Tactic:
simp_to_model using List.getKey?_eq_some_getKeyD

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
theorem not_all_isAtomic (φ : L.BoundedFormula α (n + 1)) : ¬φ.all.IsAtomic := fun con => by
  cases con

Proof state:
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀'φ).IsAtomic
⊢ False

Tactic:
cases con

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z))

Proof state:
⊢ ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z))

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_one : arccos 1 = 0

Proof state:
⊢ arccos 1 = 0

Tactic:
simp [arccos]

Result:
no goals
-- Mathlib/Algebra/Group/Graph.lean
/-- **Goursat's lemma** for monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that the natural maps from `G` to
both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃* I`. -/
@[to_additive "**Goursat's lemma** for additive monoid isomorphisms.

Let `G ≤ H × I` be a submonoid of a product of additive monoids. Assume that the natural maps from
`G` to both factors are bijective. Then `G` is the graph of some isomorphism `f : H ≃+ I`."]
lemma Submonoid.exists_mulEquiv_eq_mgraph {G : Submonoid (H × I)}
    (hG₁ : Bijective (Prod.fst ∘ G.subtype)) (hG₂ : Bijective (Prod.snd ∘ G.subtype)) :
    ∃ e : H ≃* I, G = e.toMonoidHom.mgraph

Proof state:
H : Type u_2
I : Type u_3
inst✝¹ : Monoid H
inst✝ : Monoid I
G : Submonoid (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
hG₂ : Bijective (Prod.snd ∘ ⇑G.subtype)
⊢ ∃ e, G = e.toMonoidHom.mgraph

Tactic:
simpa using MonoidHom.exists_mulEquiv_mrange_eq_mgraph hG₁.surjective hG₂.surjective
  fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Result:
no goals
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_D₂ [HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] :
    ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
      d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{u_13, u_1} C₁
inst✝¹⁹ : Category.{u_14, u_2} C₂
inst✝¹⁸ : Category.{u_15, u_5} C₃
inst✝¹⁷ : Category.{u_16, u_6} C₄
inst✝¹⁶ : Category.{u_17, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
⊢ ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
simp [D₂]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem term_atom {α} [AddCommMonoid α] (x : α) : x = term 1 x 0

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
x : α
⊢ x = term 1 x 0

Tactic:
simp [term]

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem T_def : T = ‖F.eval a‖ / ‖F.derivative.eval a‖ ^ 2

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
⊢ T_gen p F a = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2

Tactic:
simp [T_gen, ← PadicInt.norm_def]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
lemma dvd_iff {p : A[X]} : minpoly A x ∣ p ↔ Polynomial.aeval x p = 0 :=
  ⟨fun ⟨q, hq⟩ ↦ by rw [hq, map_mul, aeval, zero_mul], minpoly.dvd A x⟩

Proof state:
A : Type u_1
B : Type u_2
inst✝² : Field A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
x✝ : minpoly A x ∣ p
q : A[X]
hq : p = minpoly A x * q
⊢ (Polynomial.aeval x) p = 0

Tactic:
rw [hq, map_mul, aeval, zero_mul]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem map_sub (n m k : ℕ) (h₁ : k ≤ n) :
    ((Ico n m).map fun x => x - k) = Ico (n - k) (m - k)

Proof state:
n m k : ℕ
h₁ : k ≤ n
⊢ map (fun x => x - k) (Ico n m) = Ico (n - k) (m - k)

Tactic:
rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' _ _ _ h₁]

Result:
no goals
-- Mathlib/RingTheory/MatrixAlgebra.lean
theorem invFun_smul (a : A) (M : Matrix n n A) :
    invFun n R A (a • M) = a ⊗ₜ 1 * invFun n R A M

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
M : Matrix n n A
⊢ invFun n R A (a • M) = a ⊗ₜ[R] 1 * invFun n R A M

Tactic:
simp [invFun, Finset.mul_sum]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem insert_iInter (x : β) (t : ι → Set β) : insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Proof state:
β : Type u_2
ι : Sort u_5
x : β
t : ι → Set β
⊢ insert x (⋂ i, t i) = ⋂ i, insert x (t i)

Tactic:
simp_rw [← union_singleton, iInter_union]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
lemma map₂_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : Π i, s i) (y : Π i, t i) :
    map₂ f (tprod R x) (tprod R y) = tprod R fun i ↦ f i (x i) (y i)

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i
x : (i : ι) → s i
y : (i : ι) → t i
⊢ ((map₂ f) ((tprod R) x)) ((tprod R) y) = ⨂ₜ[R] (i : ι), ((f i) (x i)) (y i)

Tactic:
simp [map₂]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem lowerClosure_sUnion (S : Set (Set α)) : lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s

Proof state:
α : Type u_1
inst✝ : Preorder α
S : Set (Set α)
⊢ lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s

Tactic:
simp_rw [sUnion_eq_biUnion, lowerClosure_iUnion]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem supDegree_neg {f : R'[A]} :
    (-f).supDegree D = f.supDegree D

Proof state:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f : R'[A]
⊢ supDegree D (-f) = supDegree D f

Tactic:
rw [supDegree, supDegree, Finsupp.support_neg]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem bsup_lt_ord_lift_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} o.card < c) :
    (∀ i hi, f i hi < c.ord) → Ordinal.bsup.{u, v} o f < c.ord :=
  bsup_lt_ord_lift (by rwa [hc.cof_eq])

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem orderEmbOfFin_boundaries :
    c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length = c.boundary

Proof state:
n : ℕ
c : Composition n
⊢ c.boundaries.orderEmbOfFin ⋯ = c.boundary

Tactic:
refine (Finset.orderEmbOfFin_unique' _ ?_).symm

Result:
n : ℕ
c : Composition n
⊢ ∀ (x : Fin (c.length + 1)), c.boundary x ∈ c.boundaries

Proof state:
n : ℕ
c : Composition n
⊢ ∀ (x : Fin (c.length + 1)), c.boundary x ∈ c.boundaries

Tactic:
exact fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean
@[simp]
lemma desc_mk {M : ModuleCat.{v} R} {n : ℕ} {N : ModuleCat.{max u v} R}
    (φ : M.AlternatingMap N n) (x : Fin n → M) :
    desc φ (mk x) = φ x

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
n : ℕ
N : ModuleCat R
φ : M.AlternatingMap N n
x : Fin n → ↑M
⊢ (ConcreteCategory.hom (desc φ)) (mk x) = φ x

Tactic:
apply exteriorPower.alternatingMapLinearEquiv_apply_ιMulti

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap_comap_eq_relrank_of_surjective
    {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E) (h : Function.Surjective f) :
    relrank (A.comap f) (B.comap f) = relrank A B

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
L : Type v
inst✝¹ : Field L
inst✝ : Algebra F L
f : L →ₐ[F] E
h : Function.Surjective ⇑f
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa using lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem mapShortComplexH1_id :
    mapShortComplexH1 (MonoidHom.id _) (𝟙 A) = 𝟙 _

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ mapShortComplexH1 (MonoidHom.id H) (𝟙 A) = 𝟙 (shortComplexH1 A)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma monotoneOn_or_antitoneOn_iff_uIcc :
    MonotoneOn f s ∨ AntitoneOn f s ↔
      ∀ᵉ (a ∈ s) (b ∈ s) (c ∈ s), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
⊢ MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, monotone_or_antitone_iff_uIcc,
  mem_uIcc]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem modEq_comm : a ≡ b [PMOD p] ↔ b ≡ a [PMOD p] :=
  (Equiv.neg _).exists_congr_left.trans <| by simp [ModEq, ← neg_eq_iff_eq_neg]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ (∃ b_1, b - a = (Equiv.symm (Equiv.neg ℤ)) b_1 • p) ↔ b ≡ a [PMOD p]

Tactic:
simp [ModEq, ← neg_eq_iff_eq_neg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_X : sumIDeriv X = X + C 1

Proof state:
⊢ sumIDeriv X = X + C 1

Tactic:
rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
  Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean
theorem mulMap_comm : mulMap B A = (mulMap A B).comp (Algebra.TensorProduct.comm R B A)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ B.mulMap A = (A.mulMap B).comp ↑(Algebra.TensorProduct.comm R ↥B ↥A)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem coe_moebius_mul_coe_zeta [Ring R] : (μ * ζ : ArithmeticFunction R) = 1

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ ↑μ * ↑ζ = 1

Tactic:
rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma RepresentableBy.comp_homEquiv_symm {F : Cᵒᵖ ⥤ Type v} {Y : C}
    (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (op X')) (f : X ⟶ X') :
    f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x) :=
  e.homEquiv.injective (by simp [homEquiv_comp])

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
X X' : C
x : F.obj (op X')
f : X ⟶ X'
⊢ e.homEquiv (f ≫ e.homEquiv.symm x) = e.homEquiv (e.homEquiv.symm (F.map f.op x))

Tactic:
simp [homEquiv_comp]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Field.lean
lemma Multiset.sum_map_div (s : Multiset ι) (f : ι → K) (a : K) :
    (s.map (fun x ↦ f x / a)).sum = (s.map f).sum / a

Proof state:
ι : Type u_1
K : Type u_2
inst✝ : DivisionSemiring K
s : Multiset ι
f : ι → K
a : K
⊢ (map (fun x => f x / a) s).sum = (map f s).sum / a

Tactic:
simp only [div_eq_mul_inv, Multiset.sum_map_mul_right]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma map_symm (G : SimpleGraph W) (e : V ≃ W) :
    G.map e.symm.toEmbedding = G.comap e.toEmbedding

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph W
e : V ≃ W
⊢ SimpleGraph.map e.symm.toEmbedding G = SimpleGraph.comap (⇑e.toEmbedding) G

Tactic:
rw [← comap_symm, e.symm_symm]

Result:
no goals