harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_smul_le {𝕜' : Type*} [NormedField 𝕜'] [NormedSpace 𝕜' F] [SMulCommClass 𝕜₂ 𝕜' F]
    (c : 𝕜') (f : E →SL[σ₁₂] F) : ‖c • f‖ ≤ ‖c‖ * ‖f‖ :=
  (c • f).opNorm_le_bound (mul_nonneg (norm_nonneg _) (opNorm_nonneg _)) fun _ => by
    rw [smul_apply, norm_smul, mul_assoc]
    exact mul_le_mul_of_nonneg_left (le_opNorm _ _) (norm_nonneg _)

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜₂ 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖(c • f) x✝‖ ≤ ‖c‖ * ‖f‖ * ‖x✝‖

Tactic:
rw [smul_apply, norm_smul, mul_assoc]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜₂ 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖c‖ * ‖f x✝‖ ≤ ‖c‖ * (‖f‖ * ‖x✝‖)

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
𝕜' : Type u_9
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass 𝕜₂ 𝕜' F
c : 𝕜'
f : E →SL[σ₁₂] F
x✝ : E
⊢ ‖c‖ * ‖f x✝‖ ≤ ‖c‖ * (‖f‖ * ‖x✝‖)

Tactic:
exact mul_le_mul_of_nonneg_left (le_opNorm _ _) (norm_nonneg _)

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.inv_mul_cancel_left'` for a stronger version. -/
protected lemma inv_mul_cancel_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a⁻¹ * (a * b) = b :=
  ENNReal.inv_mul_cancel_left' (by simp [ha₀]) (by simp [ha])

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = 0 → b = 0

Tactic:
simp [ha₀]

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = ⊤ → b = 0

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) :
    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
l : List α₁
init : β
⊢ foldr g init (map f l) = foldr (fun x y => g (f x) y) init l

Tactic:
induction l generalizing init <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/IntegralDomain.lean
theorem Finite.isField_of_domain (R) [CommRing R] [IsDomain R] [Finite R] : IsField R

Proof state:
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
⊢ IsField R

Tactic:
cases nonempty_fintype R

Result:
case intro
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
val✝ : Fintype R
⊢ IsField R

Proof state:
case intro
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
val✝ : Fintype R
⊢ IsField R

Tactic:
exact @Field.toIsField R (@Fintype.fieldOfDomain R _ _ (Classical.decEq R) _)

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma iInter_union_iInter {ι κ : Sort*} (f : ι → Set α) (g : κ → Set α) :
    (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j

Proof state:
α : Type u_1
ι : Sort u_12
κ : Sort u_13
f : ι → Set α
g : κ → Set α
⊢ (⋂ i, f i) ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j

Tactic:
simp_rw [iInter_union, union_iInter]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_of_ae_restrict_of_ae_restrict_compl (t : Set α) {p : α → Prop}
    (ht : ∀ᵐ x ∂μ.restrict t, p x) (htc : ∀ᵐ x ∂μ.restrict tᶜ, p x) : ∀ᵐ x ∂μ, p x :=
  nonpos_iff_eq_zero.1 <|
    calc
      μ { x | ¬p x } ≤ μ ({ x | ¬p x } ∩ t) + μ ({ x | ¬p x } ∩ tᶜ) :=
        measure_le_inter_add_diff _ _ _
      _ ≤ μ.restrict t { x | ¬p x } + μ.restrict tᶜ { x | ¬p x } :=
        add_le_add (le_restrict_apply _ _) (le_restrict_apply _ _)
      _ = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t : Set α
p : α → Prop
ht : ∀ᵐ (x : α) ∂μ.restrict t, p x
htc : ∀ᵐ (x : α) ∂μ.restrict tᶜ, p x
⊢ (μ.restrict t) {x | ¬p x} + (μ.restrict tᶜ) {x | ¬p x} = 0

Tactic:
rw [ae_iff.1 ht, ae_iff.1 htc, zero_add]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma desc' (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A) (hk : S.f ≫ k = 0) [Epi S.g] :
    ∃ (l : S.X₃ ⟶ A), S.g ≫ l = k :=
  ⟨hS.desc k hk, by simp⟩

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : Epi S.g
⊢ S.g ≫ hS.desc k hk = k

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_sub_toNat_cancel {x : BitVec w} :
    2 ^ w - (2 ^ w - x.toNat) = x.toNat

Proof state:
w : Nat
x : BitVec w
⊢ min (2 ^ w) x.toNat = x.toNat

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ 2 ^ w - (2 ^ w - x.toNat) = x.toNat

Tactic:
simp [Nat.sub_sub_eq_min, Nat.min_eq_right]

Result:
w : Nat
x : BitVec w
⊢ min (2 ^ w) x.toNat = x.toNat
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem support_eq_inter_preimage :
    support f = (chartAt H c).source ∩ extChartAt I c ⁻¹' ball (extChartAt I c c) f.rOut

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ support ↑f = (chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut

Tactic:
rw [coe_def, support_indicator, support_comp_eq_preimage, ← extChartAt_source I,
  ← (extChartAt I c).symm_image_target_inter_eq', ← (extChartAt I c).symm_image_target_inter_eq',
  f.support_eq]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_eq_intCast [DecidableEq n] [Ring α] [StarRing α]
    {M : Matrix n n α} {d : ℤ} :
    Mᴴ = d ↔ M = d :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [conjTranspose_intCast]

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Ring α
inst✝ : StarRing α
M : Matrix n n α
d : ℤ
⊢ M = (↑d)ᴴ ↔ M = ↑d

Tactic:
rw [conjTranspose_intCast]

Result:
no goals
-- Mathlib/Topology/Homotopy/Basic.lean
theorem equivalence : Equivalence (@Homotopic X Y _ _) :=
  ⟨refl, by apply symm, by apply trans⟩

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ∀ {x y : C(X, Y)}, x.Homotopic y → y.Homotopic x

Tactic:
apply symm

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ∀ {x y z : C(X, Y)}, x.Homotopic y → y.Homotopic z → x.Homotopic z

Tactic:
apply trans

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem dense_iff (hf : IsInducing f) {s : Set X} :
    Dense s ↔ ∀ x, f x ∈ closure (f '' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ Dense s ↔ ∀ (x : X), f x ∈ closure (f '' s)

Tactic:
simp only [Dense, hf.closure_eq_preimage_closure_image, mem_preimage]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem cos_oangle_eq_cos_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.Angle.cos (o.oangle x y) = Real.cos (InnerProductGeometry.angle x y)

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = Real.cos (InnerProductGeometry.angle x y)

Tactic:
rw [o.cos_oangle_eq_inner_div_norm_mul_norm hx hy, InnerProductGeometry.cos_angle]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_tensor {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
    F.map (f ⊗ g) = δ F X X' ≫ (F.map f ⊗ F.map g) ≫ μ F Y Y'

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ F.map (f ⊗ g) = δ F X X' ≫ (F.map f ⊗ F.map g) ≫ μ F Y Y'

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zip_toArray (as : List α) (bs : List β) :
    Array.zip as.toArray bs.toArray = (List.zip as bs).toArray

Proof state:
α : Type u_1
β : Type u_2
as : List α
bs : List β
⊢ as.toArray.zip bs.toArray = (as.zip bs).toArray

Tactic:
simp [Array.zip, zipWith_toArray, zip]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem mulLeftMap_eq_mulRightMap_of_commute [SMulCommClass R S S]
    {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M)
    (hc : ∀ (i : ι) (n : N), Commute (m i).1 n.1) : mulLeftMap N m = mulRightMap N m

Proof state:
case h.h
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
i : ι
n : ↥N
⊢ (mulLeftMap N m ∘ₗ lsingle i) n = (N.mulRightMap m ∘ₗ lsingle i) n

Tactic:
simp [(hc i n).eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
⊢ mulLeftMap N m = N.mulRightMap m

Tactic:
ext i n

Result:
case h.h
R : Type u_1
inst✝⁵ : Semiring R
S : Type u_4
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : SMulCommClass R R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n
i : ι
n : ↥N
⊢ (mulLeftMap N m ∘ₗ lsingle i) n = (N.mulRightMap m ∘ₗ lsingle i) n
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_multiset_count [DecidableEq α] [CommMonoid α] (s : Multiset α) :
    s.prod = ∏ m ∈ s.toFinset, m ^ s.count m

Proof state:
case h.e'_2.h.e'_3
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s : Multiset α
⊢ s = Multiset.map id s

Tactic:
rw [Multiset.map_id]

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s : Multiset α
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s

Tactic:
convert prod_multiset_map_count s id

Result:
case h.e'_2.h.e'_3
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s : Multiset α
⊢ s = Multiset.map id s
-- Mathlib/CategoryTheory/EqToHom.lean
theorem congr_obj {F G : C ⥤ D} (h : F = G) (X) : F.obj X = G.obj X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X : C
⊢ F.obj X = G.obj X

Tactic:
rw [h]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem properDivisors.not_self_mem : ¬n ∈ properDivisors n

Proof state:
n : ℕ
⊢ n ∉ n.properDivisors

Tactic:
simp [properDivisors]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Tendsto.lean
theorem tendsto_atTop [Preorder β] {m : α → β} {f : Filter α} :
    Tendsto m f atTop ↔ ∀ b, ∀ᶠ a in f, b ≤ m a

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
m : α → β
f : Filter α
⊢ Tendsto m f atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a

Tactic:
simp only [atTop, tendsto_iInf, tendsto_principal, mem_Ici]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Sub.lean
theorem sub_apply_eq_zero_of_restrict_le_restrict (h_le : μ.restrict s ≤ ν.restrict s)
    (h_meas_s : MeasurableSet s) : (μ - ν) s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_le : μ.restrict s ≤ ν.restrict s
h_meas_s : MeasurableSet s
⊢ (μ - ν) s = 0

Tactic:
rw [← restrict_apply_self, restrict_sub_eq_restrict_sub_restrict, sub_eq_zero_of_le] <;> simp [*]

Result:
no goals
-- Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
theorem single_strictAnti : StrictAnti (fun (a : α) ↦ toDegLex (single a 1))

Proof state:
α : Type u_1
inst✝ : LinearOrder α
⊢ StrictAnti fun a => toDegLex (single a 1)

Tactic:
intro _ _ h

Result:
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ : α
h : a✝ < b✝
⊢ (fun a => toDegLex (single a 1)) b✝ < (fun a => toDegLex (single a 1)) a✝

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a✝ b✝ : α
h : a✝ < b✝
⊢ (fun a => toDegLex (single a 1)) b✝ < (fun a => toDegLex (single a 1)) a✝

Tactic:
simp only [lt_iff, ofDegLex_toDegLex, degree_single, lt_self_iff_false, Lex.single_lt_iff, h,
  and_self, or_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem countP_attachWith {p : α → Prop} (l : List α) (H : ∀ a ∈ l, p a) (q : α → Bool) :
    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q

Proof state:
α : Type u_1
p : α → Prop
l : List α
H : ∀ (a : α), a ∈ l → p a
q : α → Bool
⊢ countP (fun a => q a.val) (l.attachWith p H) = countP q l

Tactic:
simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem uniformContinuous_of_continuousAt_zero [UniformSpace E] [UniformAddGroup E]
    {p : Seminorm 𝕝 E} (hp : ContinuousAt p 0) : UniformContinuous p

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (⇑p) 0
hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)
⊢ Tendsto ((fun p => dist p.1 p.2) ∘ fun x => (p x.1, p x.2)) (comap (fun x => x.1 - x.2) (𝓝 0)) (𝓝 0)

Tactic:
exact
  tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hp.comp Filter.tendsto_comap)
    (fun xy => dist_nonneg) fun xy => p.norm_sub_map_le_sub _ _

Result:
no goals

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (⇑p) 0
hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)
⊢ UniformContinuous ⇑p

Tactic:
rw [UniformContinuous, uniformity_eq_comap_nhds_zero_swapped,
  Metric.uniformity_eq_comap_nhds_zero, Filter.tendsto_comap_iff]

Result:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (⇑p) 0
hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)
⊢ Tendsto ((fun p => dist p.1 p.2) ∘ fun x => (p x.1, p x.2)) (comap (fun x => x.1 - x.2) (𝓝 0)) (𝓝 0)

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (⇑p) 0
⊢ UniformContinuous ⇑p

Tactic:
have hp : Filter.Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp

Result:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : UniformSpace E
inst✝ : UniformAddGroup E
p : Seminorm 𝕝 E
hp✝ : ContinuousAt (⇑p) 0
hp : Tendsto (⇑p) (𝓝 0) (𝓝 0)
⊢ UniformContinuous ⇑p
-- Mathlib/Order/Interval/Set/Pi.lean
theorem Icc_diff_pi_univ_Ioc_subset (x y z : ∀ i, α i) :
    (Icc x z \ pi univ fun i ↦ Ioc (y i) (z i)) ⊆ ⋃ i : ι, Icc x (update z i (y i))

Proof state:
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z a : (i : ι) → α i
hay : a ∉ univ.pi fun i => Ioc (y i) (z i)
hax : x ≤ a
haz : a ≤ z
⊢ a ∈ ⋃ i, Icc x (update z i (y i))

Tactic:
simpa [not_and_or, hax, le_update_iff, haz _] using hay

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z : (i : ι) → α i
⊢ (Icc x z \ univ.pi fun i => Ioc (y i) (z i)) ⊆ ⋃ i, Icc x (update z i (y i))

Tactic:
rintro a ⟨⟨hax, haz⟩, hay⟩

Result:
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z a : (i : ι) → α i
hay : a ∉ univ.pi fun i => Ioc (y i) (z i)
hax : x ≤ a
haz : a ≤ z
⊢ a ∈ ⋃ i, Icc x (update z i (y i))
-- Mathlib/Topology/Instances/ENat.lean
theorem nhds_natCast (n : ℕ) : 𝓝 (n : ℕ∞) = pure (n : ℕ∞)

Proof state:
n : ℕ
⊢ 𝓝 ↑n = pure ↑n

Tactic:
simp [← isOpenEmbedding_natCast.map_nhds_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basisDivisor_ne_zero_iff : basisDivisor x y ≠ 0 ↔ x ≠ y

Proof state:
F : Type u_1
inst✝ : Field F
x y : F
⊢ basisDivisor x y ≠ 0 ↔ x ≠ y

Tactic:
rw [Ne, basisDivisor_eq_zero_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem Balanced.starConvex (hs : Balanced ℝ s) : StarConvex ℝ 0 s :=
  starConvex_zero_iff.2 fun _ hx a ha₀ ha₁ =>
    hs _ (by rwa [Real.norm_of_nonneg ha₀]) (smul_mem_smul_set hx)

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Balanced ℝ s
x✝ : E
hx : x✝ ∈ s
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ ‖a‖ ≤ 1

Tactic:
rwa [Real.norm_of_nonneg ha₀]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
lemma ext_of_iso {F G : C ⥤ D} (e : F ≅ G) (hobj : ∀ X, F.obj X = G.obj X)
    (happ : ∀ X, e.hom.app X = eqToHom (hobj X)) : F = G :=
  Functor.ext hobj (fun X Y f => by
    rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
    Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id])

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
rw [← cancel_mono (e.hom.app Y), e.hom.naturality f, happ, happ, Category.assoc,
Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
lemma apply_eq_toArithmeticFunction_apply {N : ℕ} {R : Type*} [CommMonoidWithZero R]
    (χ : DirichletCharacter R N) {n : ℕ} (hn : n ≠ 0) :
    χ n = toArithmeticFunction (χ ·) n

Proof state:
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
n : ℕ
hn : n ≠ 0
⊢ χ ↑n = (toArithmeticFunction fun x => χ ↑x) n

Tactic:
simp [toArithmeticFunction, hn]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem zpowers_eq_bot {g : G} : zpowers g = ⊥ ↔ g = 1

Proof state:
G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g = ⊥ ↔ g = 1

Tactic:
rw [eq_bot_iff, zpowers_le, mem_bot]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
@[to_additive]
lemma isUltrametricDist_of_forall_norm_mul_le_max_norm
    (h : ∀ x y : S', ‖x * y‖ ≤ max ‖x‖ ‖y‖) : IsUltrametricDist S' where
  dist_triangle_max x y z

Proof state:
S' : Type u_2
inst✝ : SeminormedGroup S'
h : ∀ (x y : S'), ‖x * y‖ ≤ ‖x‖ ⊔ ‖y‖
x y z : S'
⊢ dist x z ≤ dist x y ⊔ dist y z

Tactic:
simpa only [dist_eq_norm_div, le_max_iff, div_mul_div_cancel] using h (x / y) (y / z)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_add {a b} : (⟨a + b⟩ : R[X]) = ⟨a⟩ + ⟨b⟩ :=
  show _ = add _ _ by rw [add_def]

Proof state:
R : Type u
inst✝ : Semiring R
a b : R[ℕ]
⊢ { toFinsupp := a + b } = Polynomial.add { toFinsupp := a } { toFinsupp := b }

Tactic:
rw [add_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.mul_right_eq_zero_iff (h : Monic p) {q : R[X]} : p * q = 0 ↔ q = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ p * q = 0 ↔ q = 0

Tactic:
by_cases hq : q = 0 <;> simp [h.mul_right_ne_zero, hq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_mul_sub (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (c * x - d)) = c⁻¹ • ∫ x in c * a - d..c * b - d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (c * x - d) = c⁻¹ • ∫ (x : ℝ) in c * a - d..c * b - d, f x

Tactic:
simpa only [sub_eq_add_neg] using integral_comp_mul_add f hc (-d)

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem ext' {g h : M ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h :=
  LinearMap.ext fun z =>
    TensorProduct.induction_on z (by simp_rw [LinearMap.map_zero]) H fun x y ihx ihy => by
      rw [g.map_add, h.map_add, ihx, ihy]

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
g h : M ⊗[R] N →ₗ[R] P
H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)
z : M ⊗[R] N
⊢ g 0 = h 0

Tactic:
simp_rw [LinearMap.map_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
g h : M ⊗[R] N →ₗ[R] P
H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)
z x y : M ⊗[R] N
ihx : g x = h x
ihy : g y = h y
⊢ g (x + y) = h (x + y)

Tactic:
rw [g.map_add, h.map_add, ihx, ihy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
  ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩

Proof state:
α : Type u_1
l : List α
x✝ : ∃ a, l = [a]
w✝ : α
h : l = [w✝]
⊢ l.length = 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} :
    (ofList l).size ≤ l.length

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
⊢ (ofList l).size ≤ l.length

Tactic:
simp_to_raw using Raw₀.size_insertMany_empty_list_le

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem deriv_norm_ofReal_cpow (c : ℂ) {t : ℝ} (ht : 0 < t) :
    (deriv fun x : ℝ ↦ ‖(x : ℂ) ^ c‖) t = c.re * t ^ (c.re - 1)

Proof state:
c : ℂ
t : ℝ
ht : 0 < t
⊢ (fun x => ‖↑x ^ c‖) =ᶠ[𝓝 t] fun x => x ^ c.re

Tactic:
filter_upwards [eventually_gt_nhds ht] with x hx

Result:
case h
c : ℂ
t : ℝ
ht : 0 < t
x : ℝ
hx : 0 < x
⊢ ‖↑x ^ c‖ = x ^ c.re

Proof state:
c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x => x ^ c.re) t = c.re * t ^ (c.re - 1)

Tactic:
rw [Real.deriv_rpow_const (Or.inl ht.ne')]

Result:
no goals

Proof state:
c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x => ‖↑x ^ c‖) t = c.re * t ^ (c.re - 1)

Tactic:
rw [EventuallyEq.deriv_eq (f := fun x ↦ x ^ c.re)]

Result:
c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun x => x ^ c.re) t = c.re * t ^ (c.re - 1)

c : ℂ
t : ℝ
ht : 0 < t
⊢ (fun x => ‖↑x ^ c‖) =ᶠ[𝓝 t] fun x => x ^ c.re

Proof state:
case h
c : ℂ
t : ℝ
ht : 0 < t
x : ℝ
hx : 0 < x
⊢ ‖↑x ^ c‖ = x ^ c.re

Tactic:
rw [Complex.norm_cpow_eq_rpow_re_of_pos hx]

Result:
no goals