harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_intCast {n : ℤ} {x : R} : (n : R[X]).eval x = n

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
x : R
⊢ eval x ↑n = ↑n

Tactic:
simp only [← C_eq_intCast, eval_C]

Result:
no goals
-- Mathlib/GroupTheory/NoncommCoprod.lean
theorem noncommCoprod_unique (f : M × N →* P) :
    (f.comp (inl M N)).noncommCoprod (f.comp (inr M N)) (fun _ _ => (commute_inl_inr _ _).map f)
      = f :=
  ext fun x => by simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M × N →* P
x : M × N
⊢ ((f.comp (inl M N)).noncommCoprod (f.comp (inr M N)) ⋯) x = f x

Tactic:
simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

Result:
no goals
-- Mathlib/Topology/Basic.lean
@[simp]
lemma denseRange_subtype_val {p : X → Prop} : DenseRange (@Subtype.val _ p) ↔ Dense {x | p x}

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
p : X → Prop
⊢ DenseRange Subtype.val ↔ Dense {x | p x}

Tactic:
simp [DenseRange]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndepOn_iff_disjoint: LinearIndepOn R v s ↔
      Disjoint (Finsupp.supported R R s) (LinearMap.ker <| Finsupp.linearCombination R v)

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ LinearIndepOn R v s ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))

Tactic:
rw [linearIndepOn_iff, LinearMap.disjoint_ker]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_atom (a : R) (b) : a ^ b = a ^ b * (nat_lit 1).rawCast + 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
⊢ a ^ b = a ^ b * Nat.rawCast 1 + 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
lemma ofRat_div (x y : β) : ofRat (x / y) = (ofRat x / ofRat y : Cauchy abv)

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ ofRat (x / y) = ofRat x / ofRat y

Tactic:
simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sub_coe_pi_eq_add_coe_pi (θ : Angle) : θ - π = θ + π

Proof state:
θ : Angle
⊢ θ - ↑π = θ + ↑π

Tactic:
rw [sub_eq_add_neg, neg_coe_pi]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem subset_toCone : s ⊆ hs.toCone s := fun x hx =>
  hs.mem_toCone'.2 ⟨1, zero_lt_one, by rwa [one_smul]⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ 1 • x ∈ s

Tactic:
rwa [one_smul]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem moveLeft_toLeftMovesNim {o : Ordinal} (i) :
    (nim o).moveLeft (toLeftMovesNim i) = nim i

Proof state:
o : Ordinal.{u_1}
i : ↑(Set.Iio o)
⊢ (nim o).moveLeft (toLeftMovesNim i) = nim ↑i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
    (zipWith f as bs).size = min as.size bs.size

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : Array α
bs : Array β
f : α → β → γ
⊢ (zipWith f as bs).size = min as.size bs.size

Tactic:
rw [size_eq_length_toList, toList_zipWith, List.length_zipWith]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_div_le (a b : E) : ‖a / b‖ ≤ ‖a‖ + ‖b‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ ≤ ‖a‖ + ‖b‖

Tactic:
simpa [dist_eq_norm_div] using dist_triangle a 1 b

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem div_add' (a b c : K) (hc : c ≠ 0) : a / c + b = (a + b * c) / c

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ a / c + b = (a + b * c) / c

Tactic:
rwa [add_comm, add_div', add_comm]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem WithTop.coe_iInf [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (range f)) :
    ↑(⨅ i, f i) = (⨅ i, f i : WithTop α)

Proof state:
α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f) hf, ← range_comp, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem mk_univ_real : #(Set.univ : Set ℝ) = 𝔠

Proof state:
⊢ #↑Set.univ = 𝔠

Tactic:
rw [mk_univ, mk_real]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem single_eq_of_ne {i i' b} (h : i ≠ i') : (single i b : Π₀ i, β i) i' = 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
h : i ≠ i'
⊢ (single i b) i' = 0

Tactic:
simp only [single_apply, dif_neg h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem _root_.IsClosed.hausdorffDist_zero_iff_eq (hs : IsClosed s) (ht : IsClosed t)
    (fin : hausdorffEdist s t ≠ ⊤) : hausdorffDist s t = 0 ↔ s = t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
hs : IsClosed s
ht : IsClosed t
fin : hausdorffEdist s t ≠ ⊤
⊢ hausdorffDist s t = 0 ↔ s = t

Tactic:
simp [← hausdorffEdist_zero_iff_eq_of_closed hs ht, hausdorffDist, ENNReal.toReal_eq_zero_iff,
  fin]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_le_dens (h : s ⊆ t) : dens s ≤ dens t :=
  div_le_div_of_nonneg_right (mod_cast card_mono h) <| by positivity

Proof state:
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : s ⊆ t
⊢ 0 ≤ ↑(Fintype.card α)

Tactic:
positivity

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
lemma faithfulSMul_iff_algebraMap_injective : FaithfulSMul R A ↔ Injective (algebraMap R A)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ FaithfulSMul R A ↔ Injective ⇑(algebraMap R A)

Tactic:
rw [faithfulSMul_iff_injective_smul_one, Algebra.algebraMap_eq_smul_one']

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem dist_eq_of_L1 (x y : PiLp 1 β) : dist x y = ∑ i, dist (x i) (y i)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ dist x y = ∑ i : ι, dist (x i) (y i)

Tactic:
simp_rw [dist_eq_norm, norm_eq_of_L1, sub_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
    xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
  getElem_attachWith h

Proof state:
α : Type ?u.39174
xs : Array α
i : Nat
h : i < xs.attach.size
⊢ i < xs.size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm_ι_mul (m : M) (x : CliffordAlgebra Q) :
    changeForm h (ι (M := M) Q m * x) = ι (M := M) Q' m * changeForm h x
    - contractLeft (Q := Q') (B m) (changeForm h x) :=
-- Porting note: original statement
--    - BilinForm.toLin B m⌋changeForm h x :=
  (foldr_mul _ _ _ _ _ _).trans <| by rw [foldr_ι]; rfl

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q
⊢ ((changeFormAux Q' B) m) (((foldr Q (changeFormAux Q' B) ⋯) 1) x) =
    (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q
⊢ ((foldr Q (changeFormAux Q' B) ⋯) (((foldr Q (changeFormAux Q' B) ⋯) 1) x)) ((ι Q) m) =
    (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)

Tactic:
rw [foldr_ι]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
x : CliffordAlgebra Q
⊢ ((changeFormAux Q' B) m) (((foldr Q (changeFormAux Q' B) ⋯) 1) x) =
    (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem withBotCoe_inj {I J : WithBot (Box ι)} : (I : Set (ι → ℝ)) = J ↔ I = J

Proof state:
ι : Type u_1
I J : WithBot (Box ι)
⊢ ↑I = ↑J ↔ I = J

Tactic:
simp only [Subset.antisymm_iff, ← le_antisymm_iff, withBotCoe_subset_iff]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem separable_X_pow_sub_C' (p n : ℕ) (a : F) [CharP F p] (hn : ¬p ∣ n) (ha : a ≠ 0) :
    Separable (X ^ n - C a) :=
  separable_X_pow_sub_C a (by rwa [← CharP.cast_eq_zero_iff F p n] at hn) ha

Proof state:
F : Type u
inst✝¹ : Field F
p n : ℕ
a : F
inst✝ : CharP F p
hn : ¬p ∣ n
ha : a ≠ 0
⊢ ↑n ≠ 0

Tactic:
rwa [← CharP.cast_eq_zero_iff F p n] at hn

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Polynomial.transcendental (f : R[X]) (hf : f.natDegree ≠ 0)
    (hf' : f.leadingCoeff ∈ nonZeroDivisors R) :
    Transcendental R f

Proof state:
R : Type u
inst✝ : CommRing R
f : R[X]
hf : f.natDegree ≠ 0
hf' : f.leadingCoeff ∈ nonZeroDivisors R
⊢ Transcendental R f

Tactic:
simpa using (transcendental_X R).aeval f hf hf'

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem strictAntiOn_iff_strictAnti : StrictAntiOn f s ↔
    StrictAnti fun a : s => f a

Proof state:
α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictAntiOn f s ↔ StrictAnti fun a => f ↑a

Tactic:
simp [StrictAnti, StrictAntiOn]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The product of the prime factors of `n` that are less than `N` is an `N`-smooth number. -/
lemma prod_mem_smoothNumbers (n N : ℕ) :
    (n.primeFactorsList.filter (· < N)).prod ∈ smoothNumbers N

Proof state:
n N : ℕ
⊢ (List.filter (fun x => decide (x < N)) n.primeFactorsList).prod ∈ N.smoothNumbers

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, ← Finset.mem_range, prod_mem_factoredNumbers]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem eval₂_one_cyclotomic_prime_pow {R S : Type*} [CommRing R] [Semiring S] (f : R →+* S)
    {p : ℕ} (k : ℕ) [Fact p.Prime] : eval₂ f 1 (cyclotomic (p ^ (k + 1)) R) = p

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Semiring S
f : R →+* S
p k : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic (p ^ (k + 1)) R) = ↑p

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem dyadicMap_apply_pow' (m : ℤ) (n : ℕ) :
    m * Surreal.powHalf (Submonoid.log (Submonoid.pow (2 : ℤ) n)) = m * powHalf n

Proof state:
m : ℤ
n : ℕ
⊢ ↑m * powHalf (Submonoid.log (Submonoid.pow 2 n)) = ↑m * powHalf n

Tactic:
rw [@Submonoid.log_pow_int_eq_self 2 one_lt_two]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsupp_single (i : ι) (m : M) (k : κ) (n : N) :
    finsuppTensorFinsupp R S M N ι κ (Finsupp.single i m ⊗ₜ Finsupp.single k n) =
      Finsupp.single (i, k) (m ⊗ₜ n)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
m : M
k : κ
n : N
⊢ (finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ[R] n)

Tactic:
simp [finsuppTensorFinsupp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
protected lemma IsBigO.sqrt (hfg : f =O[l] g) (hg : 0 ≤ᶠ[l] g) :
    (Real.sqrt <| f ·) =O[l] (Real.sqrt <| g ·)

Proof state:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f =O[l] g
hg : 0 ≤ᶠ[l] g
⊢ (fun x => √(f x)) =O[l] fun x => √(g x)

Tactic:
simpa [Real.sqrt_eq_rpow] using hfg.rpow one_half_pos.le hg

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_equiv_iff {a b : Ordinal} : (a.toPGame ≈ b.toPGame) ↔ a = b

Proof state:
a b : Ordinal.{u_1}
⊢ a.toPGame ≈ b.toPGame ↔ a = b

Tactic:
change _ ≤_ ∧ _ ≤ _ ↔ _

Result:
a b : Ordinal.{u_1}
⊢ a.toPGame ≤ b.toPGame ∧ b.toPGame ≤ a.toPGame ↔ a = b

Proof state:
a b : Ordinal.{u_1}
⊢ a.toPGame ≤ b.toPGame ∧ b.toPGame ≤ a.toPGame ↔ a = b

Tactic:
rw [le_antisymm_iff, toPGame_le_iff, toPGame_le_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Floor/Div.lean
lemma ceilDiv_zero (b : β) : b ⌈/⌉ (0 : α) = 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMulZeroClass α β
inst✝ : CeilDiv α β
b : β
⊢ b ⌈/⌉ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Dedup.lean
theorem Nodup.le_dedup_iff_le {s t : Multiset α} (hno : s.Nodup) : s ≤ t.dedup ↔ s ≤ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hno : s.Nodup
⊢ s ≤ t.dedup ↔ s ≤ t

Tactic:
simp [le_dedup, hno]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_neg_apply :
    mpullbackWithin I I' f (-V) s x = - mpullbackWithin I I' f V s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
V : (x : M') → TangentSpace I' x
⊢ mpullbackWithin I I' f (-V) s x = -mpullbackWithin I I' f V s x

Tactic:
simp [mpullbackWithin_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} :
    (unitOfList l).contains k = l.contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ (unitOfList l).contains k = l.contains k

Tactic:
simp_to_raw using Raw₀.Const.contains_insertManyIfNewUnit_empty_list

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iio_subset_Iic_self : Iio a ⊆ Iic a

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ Iio a ⊆ Iic a

Tactic:
simpa [← coe_subset] using Set.Iio_subset_Iic_self

Result:
no goals
-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem quasiMeasurePreserving_symm (μ : Measure α) (e : α ≃ᵐ β) :
    Measure.QuasiMeasurePreserving e.symm (μ.map e) μ :=
  ⟨e.symm.measurable, by rw [Measure.map_map, e.symm_comp_self, Measure.map_id] <;> measurability⟩

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
e : α ≃ᵐ β
⊢ Measure.map (⇑e.symm) (Measure.map (⇑e) μ) ≪ μ

Tactic:
rw [Measure.map_map, e.symm_comp_self, Measure.map_id] <;> measurability

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_apply : cfc f a = cfcHom (a := a) ha ⟨_, hf.restrict⟩

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ cfc f a = (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }

Tactic:
rw [cfc_def, dif_pos ⟨ha, hf⟩]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem algHomOfDvd_apply_root {p q : K[X]} (hpq : q ∣ p) :
    algHomOfDvd hpq (root p) = root q

Proof state:
K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : q ∣ p
⊢ (algHomOfDvd hpq) (root p) = root q

Tactic:
rw [algHomOfDvd, liftHom_root]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_sub_C (c : R) : derivative (X - C c) = 1

Proof state:
R : Type u
inst✝ : Ring R
c : R
⊢ derivative (X - C c) = 1

Tactic:
rw [derivative_sub, derivative_X, derivative_C, sub_zero]

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem prod_empty : (empty : NormalWord d).prod = 1

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
⊢ empty.prod = 1

Tactic:
simp [prod, empty]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem uniformOfFinset_apply_of_mem (ha : a ∈ s) : uniformOfFinset s hs a = (s.card : ℝ≥0∞)⁻¹

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ (uniformOfFinset s hs) a = (↑s.card)⁻¹

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_map_right (f : β → γ) (F : Filter α) (G : Filter β) :
    F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
F : Filter α
G : Filter β
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)

Tactic:
rw [← prod_map_map_eq', map_id]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem dist_le (C0 : (0 : ℝ) ≤ C) : dist f g ≤ C ↔ ∀ x : α, dist (f x) (g x) ≤ C

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 ≤ C
⊢ dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C

Tactic:
simp only [← dist_mkOfCompact, BoundedContinuousFunction.dist_le C0, mkOfCompact_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp] lemma cons_support_tail (p : G.Walk x y) (hp : ¬p.Nil) :
    x :: p.tail.support = p.support

Proof state:
V : Type u
G : SimpleGraph V
x y : V
p : G.Walk x y
hp : ¬p.Nil
⊢ x :: p.tail.support = p.support

Tactic:
rw [← support_cons, cons_tail_eq _ hp]

Result:
no goals
-- Mathlib/Algebra/Star/Module.lean
protected lemma IsSelfAdjoint.algebraMap {r : R} (hr : IsSelfAdjoint r) :
    IsSelfAdjoint (algebraMap R A r)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint ((algebraMap R A) r)

Tactic:
simpa using congr(algebraMap R A $(hr.star_eq))

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_leftUnitor {p f pf : C} (η_f : p ⊗ f ≅ pf) :
    p ◁ (λ_ f) ≪≫ η_f = normalizeIsoComp (ρ_ p) η_f :=
  Iso.ext (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ (p ◁ λ_ f ≪≫ η_f).hom = (normalizeIsoComp (ρ_ p) η_f).hom

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_add_restrict_compl (hs : MeasurableSet s) :
    μ.restrict s + μ.restrict sᶜ = μ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s + μ.restrict sᶜ = μ

Tactic:
rw [← restrict_union (@disjoint_compl_right (Set α) _ _) hs.compl, union_compl_self,
  restrict_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/MinMax.lean
theorem min_le_right (a b : Nat) : min a b ≤ b

Proof state:
a b : Nat
⊢ min a b ≤ b

Tactic:
by_cases (a <= b) <;> simp [Nat.min_def, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
    a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β k
⊢ a ∈ m.insertIfNew k v → ¬((k == a) = true ∧ ¬k ∈ m) → a ∈ m

Tactic:
simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew'

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem inr_comp_pushoutObjIso_inv (f : F ⟶ G) (g : F ⟶ H) (d : D) :
    pushout.inr (f.app d) (g.app d) ≫ (pushoutObjIso f g d).inv = (pushout.inr f g).app d

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPushouts C
f : F ⟶ G
g : F ⟶ H
d : D
⊢ pushout.inr (f.app d) (g.app d) ≫ (pushoutObjIso f g d).inv = (pushout.inr f g).app d

Tactic:
simp [pushoutObjIso]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem coe_πs (o : Ordinal) (f : LocallyConstant (π C (ord I · < o)) ℤ) :
    πs C o f = f ∘ ProjRestrict C (ord I · < o)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
f : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
⊢ ⇑((πs C o) f) = ⇑f ∘ ProjRestrict C fun x => ord I x < o

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem norm_cexp_neg_mul_sq (b : ℂ) (x : ℝ) :
    ‖Complex.exp (-b * (x : ℂ) ^ 2)‖ = exp (-b.re * x ^ 2)

Proof state:
b : ℂ
x : ℝ
⊢ ‖cexp (-b * ↑x ^ 2)‖ = rexp (-b.re * x ^ 2)

Tactic:
rw [norm_exp, ← ofReal_pow, mul_comm (-b) _, re_ofReal_mul, neg_re, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_iff_lt_mul' : a / b < c ↔ a < b * c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a / b < c ↔ a < b * c

Tactic:
rw [div_lt_iff_lt_mul, mul_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isBigO_exp_comp_exp_comp {f g : α → ℝ} :
    ((fun x => exp (f x)) =O[l] fun x => exp (g x)) ↔ IsBoundedUnder (· ≤ ·) l (f - g) :=
  Iff.trans (isBigO_iff_isBoundedUnder_le_div <| Eventually.of_forall fun _ => exp_ne_zero _) <| by
    simp only [norm_eq_abs, abs_exp, ← exp_sub, isBoundedUnder_le_exp_comp, Pi.sub_def]

Proof state:
α : Type u_1
l : Filter α
f g : α → ℝ
⊢ (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖rexp (f x)‖ / ‖rexp (g x)‖) ↔
    IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (f - g)

Tactic:
simp only [norm_eq_abs, abs_exp, ← exp_sub, isBoundedUnder_le_exp_comp, Pi.sub_def]

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem transAssocReparamAux_zero : transAssocReparamAux 0 = 0

Proof state:
⊢ transAssocReparamAux 0 = 0

Tactic:
norm_num [transAssocReparamAux]

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_map (e : Basis ι R M) (f : M ≃ₗ[R] N) :
    (e.map f).orientation = Orientation.map ι f e.orientation

Proof state:
R : Type u_1
inst✝⁶ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] N
⊢ (e.map f).orientation = (Orientation.map ι f) e.orientation

Tactic:
simp_rw [Basis.orientation, Orientation.map_apply, Basis.det_map']

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma ι_mapMap (i : I) (j : J) (hij : p i = j) :
    X.ιMapObj p i j hij ≫ mapMap φ p j = φ i ≫ Y.ιMapObj p i j hij

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝² : Category.{u_5, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
i : I
j : J
hij : p i = j
⊢ X.ιMapObj p i j hij ≫ mapMap φ p j = φ i ≫ Y.ιMapObj p i j hij

Tactic:
simp only [mapMap, ι_descMapObj]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem le_normalizer : H ≤ normalizer H := fun x xH n => by
  rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : G
xH : x ∈ H
n : G
⊢ n ∈ H ↔ x * n * x⁻¹ ∈ H

Tactic:
rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]

Result:
no goals