harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_strictMonoOn : StrictMonoOn toNat (Iio ℵ₀)

Proof state:
⊢ ∀ (i i_1 : ℕ), i < i_1 → i < i_1

Tactic:
exact fun _ _ ↦ id

Result:
no goals

Proof state:
⊢ StrictMonoOn (⇑toNat) (Iio ℵ₀)

Tactic:
simp only [← range_natCast, StrictMonoOn, forall_mem_range, toNat_natCast, Nat.cast_lt]

Result:
⊢ ∀ (i i_1 : ℕ), i < i_1 → i < i_1
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
@[simp]
lemma dist_pi_const [Nonempty β] (a b : α) : (dist (fun _ : β => a) fun _ => b) = dist a b

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
inst✝¹ : Fintype β
inst✝ : Nonempty β
a b : α
⊢ (dist (fun x => a) fun x => b) = dist a b

Tactic:
simpa only [dist_edist] using congr_arg ENNReal.toReal (edist_pi_const a b)

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The abscissa of absolute convergence of the L-series of the Möbius function is `1`. -/
lemma abscissaOfAbsConv_moebius : abscissaOfAbsConv ↗μ = 1

Proof state:
⊢ (abscissaOfAbsConv fun n => ↑(μ n)) = 1

Tactic:
simpa [abscissaOfAbsConv, LSeriesSummable_moebius_iff, Set.Ioi_def, EReal.image_coe_Ioi]
  using csInf_Ioo <| EReal.coe_lt_top 1

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem vec2_dotProduct' {a₀ a₁ b₀ b₁ : α} : ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁

Proof state:
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁

Tactic:
rw [cons_dotProduct_cons, cons_dotProduct_cons, dotProduct_empty, add_zero]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[simp]
lemma iso_inv_base_hom_base_apply {X Y : LocallyRingedSpace.{u}} (e : X ≅ Y) (y : Y) :
    (e.hom.base (e.inv.base y)) = y

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
show (e.inv.base ≫ e.hom.base) y = 𝟙 Y.toPresheafedSpace y

Result:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom (e.inv.base ≫ e.hom.base)) y = (ConcreteCategory.hom (𝟙 Y.toPresheafedSpace).base) y

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom (e.inv.base ≫ e.hom.base)) y = (ConcreteCategory.hom (𝟙 Y.toPresheafedSpace).base) y

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem isOpenMap_mk : IsOpenMap (mk : X → SeparationQuotient X) := fun s hs =>
  isQuotientMap_mk.isOpen_preimage.1 <| by rwa [preimage_image_mk_open hs]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ IsOpen (mk ⁻¹' (mk '' s))

Tactic:
rwa [preimage_image_mk_open hs]

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_reindex (e : Basis ι R M) (eι : ι ≃ ι') :
    (e.reindex eι).orientation = Orientation.reindex R M eι e.orientation

Proof state:
R : Type u_1
inst✝⁶ : StrictOrderedCommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_4
ι' : Type u_5
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
e : Basis ι R M
eι : ι ≃ ι'
⊢ (e.reindex eι).orientation = (Orientation.reindex R M eι) e.orientation

Tactic:
simp_rw [Basis.orientation, Orientation.reindex_apply, Basis.det_reindex']

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
lemma isPullback_Spec_map_pushout {A B C : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) :
    IsPullback (Spec.map (pushout.inl f g))
      (Spec.map (pushout.inr f g)) (Spec.map f) (Spec.map g)

Proof state:
case h
A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPushout f g (pushout.inl f g) (pushout.inr f g)

Tactic:
exact IsPushout.of_hasPushout f g

Result:
no goals

Proof state:
A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPullback (Spec.map (pushout.inl f g)) (Spec.map (pushout.inr f g)) (Spec.map f) (Spec.map g)

Tactic:
apply isPullback_Spec_map_isPushout

Result:
case h
A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPushout f g (pushout.inl f g) (pushout.inr f g)
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem hasCompactSupport [FiniteDimensional ℝ E] : HasCompactSupport f

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : HasContDiffBump E
c : E
f : ContDiffBump c
inst✝ : FiniteDimensional ℝ E
⊢ HasCompactSupport ↑f

Tactic:
simp_rw [HasCompactSupport, f.tsupport_eq, isCompact_closedBall]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIcc_eq_union : [[a, b]] = Icc a b ∪ Icc b a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc a b ∪ Icc b a

Tactic:
rw [Icc_union_Icc', max_comm] <;> rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem lift_le_continuum {c : Cardinal.{u}} : lift.{v} c ≤ 𝔠 ↔ c ≤ 𝔠

Proof state:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ 𝔠 ↔ c ≤ 𝔠

Tactic:
rw [← lift_continuum.{v, u}, lift_le]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) :
    (p.concat h).edges = p.edges.concat s(v, w)

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).edges = p.edges.concat s(v, w)

Tactic:
simp [edges]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_eq_sub (a b : α) : toIocMod hp a b = toIocMod hp 0 (b - a) + a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = toIocMod hp 0 (b - a) + a

Tactic:
rw [toIocMod_sub_eq_sub, zero_add, sub_add_cancel]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
@[simp] lemma log_zero : log (0 : A) = 0

Proof state:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
⊢ log 0 = 0

Tactic:
simp [log]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
  if_pos <| by simp

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
⊢ ∅ ⊆ {⊤} ∨ ¬BddBelow ∅

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem nextn_stop : ∀ {s}, ValidFor l m r s → ∀ n, s.nextn n ⟨utf8Len m⟩ = ⟨utf8Len m⟩
  | _, _, 0 => rfl
  | _, h, n+1 => by simp [Substring.nextn, h.next_stop, h.nextn_stop n]

Proof state:
l m r : List Char
x✝ : Substring
h : ValidFor l m r x✝
n : Nat
⊢ x✝.nextn (n + 1) { byteIdx := utf8Len m } = { byteIdx := utf8Len m }

Tactic:
simp [Substring.nextn, h.next_stop, h.nextn_stop n]

Result:
no goals
-- Mathlib/Algebra/Vertex/VertexOperator.lean
theorem of_coeff_apply_coeff (f : ℤ → Module.End R V)
    (hf : ∀ (x : V), ∃ n, ∀ m < n, (f m) x = 0) (x : V) (n : ℤ) :
    ((HahnModule.of R).symm ((of_coeff f hf) x)).coeff n = (f n) x

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), ∃ n, ∀ m < n, (f m) x = 0
x : V
n : ℤ
⊢ ((HahnModule.of R).symm ((of_coeff f hf) x)).coeff n = (f n) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem gen_mem_uniformity (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
    UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ UniformOnFun.gen 𝔖 s V ∈ ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)

Tactic:
apply_rules [mem_iInf_of_mem, mem_principal_self]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β)

Tactic:
rw [UniformOnFun.uniformity_eq]

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ UniformOnFun.gen 𝔖 s V ∈ ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)
-- Mathlib/Topology/UnitInterval.lean
theorem symm_one : σ 1 = 0 :=
  Subtype.ext <| by simp [symm]

Proof state:
⊢ ↑(σ 1) = ↑0

Tactic:
simp [symm]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_sum {α β} : IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Proof state:
α : Type u_4
β : Type u_5
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_sum, not_or]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem not_coprime_of_dvd_of_dvd (dgt1 : 1 < d) (Hm : d ∣ m) (Hn : d ∣ n) : ¬ Coprime m n :=
  fun co => Nat.not_le_of_gt dgt1 <| Nat.le_of_dvd Nat.zero_lt_one <| by
    rw [← co.gcd_eq_one]; exact dvd_gcd Hm Hn

Proof state:
d m n : Nat
dgt1 : 1 < d
Hm : d ∣ m
Hn : d ∣ n
co : m.Coprime n
⊢ d ∣ 1

Tactic:
rw [← co.gcd_eq_one]

Result:
d m n : Nat
dgt1 : 1 < d
Hm : d ∣ m
Hn : d ∣ n
co : m.Coprime n
⊢ d ∣ m.gcd n

Proof state:
d m n : Nat
dgt1 : 1 < d
Hm : d ∣ m
Hn : d ∣ n
co : m.Coprime n
⊢ d ∣ m.gcd n

Tactic:
exact dvd_gcd Hm Hn

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem not_nonempty_empty : ¬ZFSet.Nonempty ∅

Proof state:
⊢ ¬∅.Nonempty

Tactic:
simp [ZFSet.Nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_range (i : Nat) (hi : i < n) : (Vector.range n)[i] = i

Proof state:
n i : Nat
hi : i < n
⊢ (range n)[i] = i

Tactic:
simp [Vector.range]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem gc_set :
    @GaloisConnection (Set R) (Set (PrimeSpectrum R))ᵒᵈ _ _ (fun s => zeroLocus s) fun t =>
      vanishingIdeal t

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ GaloisConnection (fun s => zeroLocus s) fun t => ↑(vanishingIdeal t)

Tactic:
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi R R).gc

Result:
R : Type u
inst✝ : CommSemiring R
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s => zeroLocus s) fun t => ↑(vanishingIdeal t)

Proof state:
R : Type u
inst✝ : CommSemiring R
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s => zeroLocus s) fun t => ↑(vanishingIdeal t)

Tactic:
simpa [zeroLocus_span, Function.comp_def] using ideal_gc.compose (gc R)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem extendScalars_self : extendScalars (le_refl F) = ⊥ :=
  restrictScalars_injective K (by simp)

Proof state:
K : Type u_1
inst✝² : Field K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
⊢ restrictScalars K (extendScalars ⋯) = restrictScalars K ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Init.lean
@[simp]
lemma lt_toNat {m : ℕ} : m < toNat n ↔ (m : ℤ) < n

Proof state:
n : ℤ
m : ℕ
⊢ m < n.toNat ↔ ↑m < n

Tactic:
rw [← Int.not_le, ← Nat.not_le, toNat_le]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma lambda_not_dvd_X : ¬ λ ∣ S.X :=
  fun h ↦ lambda_not_dvd_x S <| X_u₁_spec S ▸ dvd_mul_of_dvd_left (dvd_pow h (by decide)) _

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ FermatLastTheoremForThreeGen.Solution.X S
⊢ 3 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_sub_self_right {m n : ℕ} (h : m ≤ n) : Coprime m (n - m) ↔ Coprime m n

Proof state:
m n : ℕ
h : m ≤ n
⊢ m.Coprime (n - m) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_sub_self_right h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_mapₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : Raw.WFImp (m.mapₘ f).1 where
  buckets_hash_self := isHashSelf_mapₘ h
  size_eq

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
⊢ (m.mapₘ f).val.size = (toListModel (m.mapₘ f).val.buckets).length

Tactic:
rw [toListModel_mapₘ.length_eq, List.length_map, ← h.size_eq, mapₘ]

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem single_mul_single_right [Fintype n] [Fintype k] [DecidableEq n] [DecidableEq k]
    [DecidableEq m] [Semiring α] (a : m) (b : n) (c : k) (M : Matrix k l α) :
    (single a b).toMatrix * ((single b c).toMatrix * M) = (single a c).toMatrix * M

Proof state:
k : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype k
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
a : m
b : n
c : k
M : Matrix k l α
⊢ (single a b).toMatrix * ((single b c).toMatrix * M) = (single a c).toMatrix * M

Tactic:
rw [← Matrix.mul_assoc, single_mul_single]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
@[simp] lemma mul_div_cancel_left₀ (b : M₀) {a : M₀} (ha : a ≠ 0) : a * b / a = b

Proof state:
M₀ : Type u_1
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Div M₀
inst✝ : MulDivCancelClass M₀
b a : M₀
ha : a ≠ 0
⊢ a * b / a = b

Tactic:
rw [mul_comm, mul_div_cancel_right₀ _ ha]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem isCaratheodory_compl_iff : IsCaratheodory m sᶜ ↔ IsCaratheodory m s :=
  ⟨fun h => by simpa using isCaratheodory_compl m h, isCaratheodory_compl m⟩

Proof state:
α : Type u
m : OuterMeasure α
s : Set α
h : m.IsCaratheodory sᶜ
⊢ m.IsCaratheodory s

Tactic:
simpa using isCaratheodory_compl m h

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_pos : 0 < sqrt x ↔ 0 < x

Proof state:
x : ℝ≥0
⊢ 0 < sqrt x ↔ 0 < x

Tactic:
simp [pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Module/End.lean
theorem map_intCast_smul [AddCommGroup M] [AddCommGroup M₂] {F : Type*} [FunLike F M M₂]
    [AddMonoidHomClass F M M₂] (f : F) (R S : Type*) [Ring R] [Ring S] [Module R M] [Module S M₂]
    (x : ℤ) (a : M) :
    f ((x : R) • a) = (x : S) • f a

Proof state:
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module S M₂
x : ℤ
a : M
⊢ f (↑x • a) = ↑x • f a

Tactic:
simp only [Int.cast_smul_eq_zsmul, map_zsmul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_coeff_of_ne (i : ℕ) (hi : i ≠ f.natDegree) : f.eraseLead.coeff i = f.coeff i

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
hi : i ≠ f.natDegree
⊢ f.eraseLead.coeff i = f.coeff i

Tactic:
simp [eraseLead_coeff, hi]

Result:
no goals
-- Mathlib/Topology/Algebra/Field.lean
theorem affineHomeomorph_image_Icc {𝕜 : Type*} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)

Proof state:
𝕜 : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIoc : Fintype.card (Set.Ioc a b) = b - a

Proof state:
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a

Tactic:
rw [← card_Ioc, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem le_compl_comm : a ≤ bᶜ ↔ b ≤ aᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ b ≤ aᶜ

Tactic:
rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem HasGradientAtFilter.congr_of_eventuallyEq (h : HasGradientAtFilter f f' x L)
    (hL : f₁ =ᶠ[L] f) (hx : f₁ x = f x) : HasGradientAtFilter f₁ f' x L

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
f' x : F
L : Filter F
f₁ : F → 𝕜
h : HasGradientAtFilter f f' x L
hL : f₁ =ᶠ[L] f
hx : f₁ x = f x
⊢ HasGradientAtFilter f₁ f' x L

Tactic:
rwa [hL.hasGradientAtFilter_iff hx rfl]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem norm_approxOn_y₀_le [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E}
    {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s] (x : β) (n : ℕ) :
    ‖approxOn f hf s y₀ h₀ n x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
⊢ ‖(approxOn f hf s y₀ h₀ n) x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖

Tactic:
simpa [enorm, edist_eq_enorm_sub, ← ENNReal.coe_add, norm_sub_rev]
  using edist_approxOn_y0_le hf h₀ x n

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem le_pre : μ ≤ pre m r ↔ ∀ s : Set X, diam s ≤ r → μ s ≤ m s

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
r : ℝ≥0∞
μ : OuterMeasure X
⊢ μ ≤ pre m r ↔ ∀ (s : Set X), diam s ≤ r → μ s ≤ m s

Tactic:
simp only [pre, le_boundedBy, extend, le_iInf_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem comap_map_mkQ : comap p.mkQ (map p.mkQ p') = p ⊔ p'

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap p.mkQ (map p.mkQ p') = p ⊔ p'

Tactic:
simp [comap_map_eq, sup_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctorAssociatorX_hom (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄)
    (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
    mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫
    (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom =
      ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
        mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝³³ : Category.{u_17, u_1} C₁
inst✝³² : Category.{u_16, u_2} C₂
inst✝³¹ : Category.{u_14, u_5} C₃
inst✝³⁰ : Category.{u_13, u_6} C₄
inst✝²⁹ : Category.{u_15, u_3} C₁₂
inst✝²⁸ : Category.{u_18, u_4} C₂₃
inst✝²⁷ : HasZeroMorphisms C₁
inst✝²⁶ : HasZeroMorphisms C₂
inst✝²⁵ : HasZeroMorphisms C₃
inst✝²⁴ : Preadditive C₁₂
inst✝²³ : Preadditive C₂₃
inst✝²² : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ 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
inst✝¹⁷ : G₂₃.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁵ : F.PreservesZeroMorphisms
inst✝¹⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst✝¹² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹¹ : TotalComplexShape c₁₂ c₃ c₄
inst✝¹⁰ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁹ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁸ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝⁷ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝⁶ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝⁵ : DecidableEq ι₁₂
inst✝⁴ : DecidableEq ι₂₃
inst✝³ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝² : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝¹ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom =
    ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
      mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h

Tactic:
apply GradedObject.ι_mapBifunctorAssociator_hom

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformlyOn_iff_forall_tendsto :
    TendstoLocallyUniformlyOn F f p s ↔
      ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) :=
  forall₂_swap.trans <| forall₄_congr fun _ _ _ _ => by
    rw [mem_map, mem_prod_iff_right]; rfl

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔
    x✝¹ ∈ map (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x✝³)

Tactic:
rw [mem_map, mem_prod_iff_right]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔
    ∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (x : ι) in p, ∀ y ∈ t, (x, y) ∈ (fun y => (f y.2, F y.1 y.2)) ⁻¹' x✝¹

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
inst✝ : TopologicalSpace α
x✝³ : α
x✝² : x✝³ ∈ s
x✝¹ : Set (β × β)
x✝ : x✝¹ ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x✝¹) ↔
    ∃ t ∈ 𝓝[s] x✝³, ∀ᶠ (x : ι) in p, ∀ y ∈ t, (x, y) ∈ (fun y => (f y.2, F y.1 y.2)) ⁻¹' x✝¹

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValRat_of_nat (n : ℕ) : ↑(padicValNat p n) = padicValRat p n

Proof state:
p n : ℕ
⊢ ↑(padicValNat p n) = padicValRat p ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem restr_eq_of_source_subset {e : PartialEquiv α β} {s : Set α} (h : e.source ⊆ s) :
    e.restr s = e :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) (by simp [inter_eq_self_of_subset_left h])

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : e.source ⊆ s
⊢ (e.restr s).source = e.source

Tactic:
simp [inter_eq_self_of_subset_left h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_castSucc [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
    ∏ i, f i = (∏ i : Fin n, f (Fin.castSucc i)) * f (last n)

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
f : Fin (n + 1) → β
⊢ ∏ i : Fin (n + 1), f i = (∏ i : Fin n, f i.castSucc) * f (last n)

Tactic:
simpa [mul_comm] using prod_univ_succAbove f (last n)

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem abs_zero : (0 : EReal).abs = 0

Proof state:
⊢ EReal.abs 0 = 0

Tactic:
rw [abs_eq_zero_iff]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma two_pow_succ (n : ℕ) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n

Proof state:
n : ℕ
⊢ 2 ^ (n + 1) = 2 ^ n + 2 ^ n

Tactic:
simp [Nat.pow_succ, Nat.mul_two]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_dblXYZ (P : Fin 3 → A) : (W'.baseChange B).toProjective.dblXYZ (f ∘ P) =
    f ∘ (W'.baseChange A).toProjective.dblXYZ P

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.dblXYZ (⇑f ∘ P) = ⇑f ∘ (baseChange W' A).toProjective.dblXYZ P

Tactic:
rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem hasDerivAt_fourier_neg (n : ℤ) (x : ℝ) :
    HasDerivAt (fun y : ℝ => fourier (-n) (y : AddCircle T))
      (-2 * π * I * n / T * fourier (-n) (x : AddCircle T)) x

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y => (fourier (-n)) ↑y) (-2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x) x

Tactic:
simpa using hasDerivAt_fourier T (-n) x

Result:
no goals