harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_C_mul (a0 : a ≠ 0) : (C a * p).natDegree = p.natDegree

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
a : R
inst✝ : NoZeroDivisors R
a0 : a ≠ 0
⊢ (C a * p).natDegree = p.natDegree

Tactic:
simp only [natDegree, degree_C_mul a0]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
@[simp]
lemma nsmul_eq_nsmul (n : ℕ) (x : X[S⁻¹]) :
    letI inst := OreLocalization.instModuleOfIsScalarTower (R₀ := ℕ) (R := R) (X := X) (S := S)
    HSMul.hSMul (self := @instHSMul _ _ inst.toSMul) n x = n • x

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
n : ℕ
x : OreLocalization S X
⊢ n • x = n • x

Tactic:
letI inst := OreLocalization.instModuleOfIsScalarTower (R₀ := ℕ) (R := R) (X := X) (S := S)

Result:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
n : ℕ
x : OreLocalization S X
inst : Module ℕ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
n : ℕ
x : OreLocalization S X
inst : Module ℕ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Tactic:
exact congr($(AddCommMonoid.uniqueNatModule.2 inst).smul n x)

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_sum_left {ι : Type*} [Countable ι] {μ : ι → Measure α} [∀ i, SFinite (μ i)] :
    (sum μ) ⊗ₘ κ = sum (fun i ↦ (μ i) ⊗ₘ κ)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst✝¹ : Countable ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SFinite (μ i)
⊢ (Kernel.sum fun i => Kernel.const Unit (μ i) ⊗ₖ Kernel.prodMkLeft Unit κ) () = sum fun i => μ i ⊗ₘ κ

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst✝¹ : Countable ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SFinite (μ i)
⊢ sum μ ⊗ₘ κ = sum fun i => μ i ⊗ₘ κ

Tactic:
rw [compProd, ← Kernel.sum_const, Kernel.compProd_sum_left]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
ι : Type u_3
inst✝¹ : Countable ι
μ : ι → Measure α
inst✝ : ∀ (i : ι), SFinite (μ i)
⊢ (Kernel.sum fun i => Kernel.const Unit (μ i) ⊗ₖ Kernel.prodMkLeft Unit κ) () = sum fun i => μ i ⊗ₘ κ
-- Mathlib/Order/WellFounded.lean
theorem not_rel_apply_succ [h : IsWellFounded α r] (f : ℕ → α) : ∃ n, ¬ r (f (n + 1)) (f n)

Proof state:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
⊢ ∃ n, ¬r (f (n + 1)) (f n)

Tactic:
by_contra! hf

Result:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False

Proof state:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False

Tactic:
exact (wellFounded_iff_no_descending_seq.1 h.wf).elim ⟨f, hf⟩

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem IsCompl.bihimp_eq_bot {a b : α} (h : IsCompl a b) : a ⇔ b = ⊥

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
h : IsCompl a b
⊢ a ⇔ b = ⊥

Tactic:
rw [h.eq_compl, compl_bihimp_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma leadingCoeff_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) :
    (C a * p).leadingCoeff = a * p.leadingCoeff

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).leadingCoeff = a * p.leadingCoeff

Tactic:
rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem verts_iSup {f : ι → G.Subgraph} : (⨆ i, f i).verts = ⋃ i, (f i).verts

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ (⨆ i, f i).verts = ⋃ i, (f i).verts

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_mem_openSegment_compl_self [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ)
    (hs₀ : μ s ≠ 0) (hsc₀ : μ sᶜ ≠ 0) :
    ⨍⁻ x, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ x in s, f x ∂μ) (⨍⁻ x in sᶜ, f x ∂μ)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
hs₀ : μ s ≠ 0
hsc₀ : μ sᶜ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)

Tactic:
simpa only [union_compl_self, restrict_univ] using
  laverage_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _)
    (measure_ne_top _ _)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.mul_const (hc : HasStrictDerivAt c c' x) (d : 𝔸) :
    HasStrictDerivAt (fun y => c y * d) (c' * d) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
⊢ HasStrictDerivAt (fun y => c y * d) (c' * d) x

Tactic:
convert hc.mul (hasStrictDerivAt_const x d) using 1

Result:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
⊢ c' * d = c' * d + c x * 0

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
⊢ c' * d = c' * d + c x * 0

Tactic:
rw [mul_zero, add_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_rw₁ {f f' : α → β} (h : f =ᵐ[μ] f') (g : β → ℝ≥0∞) :
    ∫⁻ a, g (f a) ∂μ = ∫⁻ a, g (f' a) ∂μ :=
  lintegral_congr_ae <| h.mono fun a h => by dsimp only; rw [h]

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h✝ : f =ᶠ[ae μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
⊢ (fun a => g (f a)) a = (fun a => g (f' a)) a

Tactic:
dsimp only

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h✝ : f =ᶠ[ae μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
⊢ g (f a) = g (f' a)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h✝ : f =ᶠ[ae μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
⊢ g (f a) = g (f' a)

Tactic:
rw [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_singleton_smul_eq {r : R} (hr : IsUnit r) (x : M) : (R ∙ r • x) = R ∙ x

Proof state:
case intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : Rˣ
⊢ span R {r • x} = span R {x}

Tactic:
exact span_singleton_group_smul_eq R r x

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : IsUnit r
x : M
⊢ span R {r • x} = span R {x}

Tactic:
lift r to Rˣ using hr

Result:
case intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : Rˣ
⊢ span R {↑r • x} = span R {x}

Proof state:
case intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : Rˣ
⊢ span R {↑r • x} = span R {x}

Tactic:
rw [← Units.smul_def]

Result:
case intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : Rˣ
⊢ span R {r • x} = span R {x}
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousWithinAt_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'}
    {S : Set X} {x₀ : X} : EquicontinuousWithinAt (uα :=  ⨅ k, u k) F S x₀ ↔
      ∀ k, EquicontinuousWithinAt (uα :=  u k) F S x₀

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀)) ↔
    ∀ (k : κ), Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf]

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀ ↔ ∀ (k : κ), ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀

Tactic:
unfold ContinuousWithinAt

Result:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀)) ↔
    ∀ (k : κ), Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), EquicontinuousWithinAt F S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt (uα := _), topologicalSpace]

Result:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀ ↔ ∀ (k : κ), ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_inv (f : R → R) (a : Aˣ)
    (hf : ContinuousOn f ((· ⁻¹) '' (spectrum R (a : A)))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Semifield 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
inst✝² : ContinuousFunctionalCalculus R p
inst✝¹ : HasContinuousInv₀ R
inst✝ : UniqueHom R A
f : R → R
a : Aˣ
hf : autoParam (ContinuousOn f ((fun x => x⁻¹) '' spectrum R ↑a)) _auto✝
ha : autoParam (p ↑a) _auto✝
⊢ cfc (fun x => f x⁻¹) ↑a = cfc f ↑a⁻¹

Tactic:
rw [cfc_comp' .., cfc_inv_id _]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma IsQuasiregular.map {F R S : Type*} [NonUnitalSemiring R] [NonUnitalSemiring S]
    [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x : R} (hx : IsQuasiregular x) :
    IsQuasiregular (f x)

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x : R
hx : ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0
⊢ ∃ y, y + f x + f x * y = 0 ∧ f x + y + y * f x = 0

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := hx

Result:
case intro.intro
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ ∃ y, y + f x + f x * y = 0 ∧ f x + y + y * f x = 0

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x : R
hx : IsQuasiregular x
⊢ IsQuasiregular (f x)

Tactic:
rw [isQuasiregular_iff] at hx ⊢

Result:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x : R
hx : ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0
⊢ ∃ y, y + f x + f x * y = 0 ∧ f x + y + y * f x = 0

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ f y + f x + f x * f y = 0 ∧ f x + f y + f y * f x = 0

Tactic:
simpa using And.intro congr(f $(hy₁)) congr(f $(hy₂))

Result:
no goals

Proof state:
case intro.intro
F : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonUnitalSemiring R
inst✝² : NonUnitalSemiring S
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ ∃ y, y + f x + f x * y = 0 ∧ f x + y + y * f x = 0

Tactic:
exact ⟨f y, by simpa using And.intro congr(f $(hy₁)) congr(f $(hy₂))⟩

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem exists_isOpen_superset_and_isCompact_closure {K : Set X} (hK : IsCompact K) :
    ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

Tactic:
rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩

Result:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

Proof state:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : R1Space X
inst✝ : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
K' : Set X
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

Tactic:
exact ⟨interior K', isOpen_interior, hKK', hK'.closure_of_subset interior_subset⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem fderiv_norm_smul_neg (ht : t < 0) :
    fderiv ℝ (‖·‖) (t • x) = -fderiv ℝ (‖·‖) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
t : ℝ
ht : t < 0
⊢ fderiv ℝ (fun x => ‖x‖) (t • x) = -fderiv ℝ (fun x => ‖x‖) x

Tactic:
simp [fderiv_norm_smul, ht]

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
theorem algebraMap_matrix_apply {r : R} {i j : n} :
    algebraMap R (Matrix n n α) r i j = if i = j then algebraMap R α r else 0

Proof state:
n : Type u_3
R : Type u_7
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring R
inst✝¹ : Semiring α
inst✝ : Algebra R α
r : R
i j : n
⊢ (algebraMap R (Matrix n n α)) r i j = if i = j then (algebraMap R α) r else 0

Tactic:
dsimp [algebraMap, Algebra.algebraMap, Matrix.scalar]

Result:
n : Type u_3
R : Type u_7
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring R
inst✝¹ : Semiring α
inst✝ : Algebra R α
r : R
i j : n
⊢ diagonal ((Pi.constRingHom n α) (Algebra.algebraMap r)) i j = if i = j then Algebra.algebraMap r else 0

Proof state:
n : Type u_3
R : Type u_7
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring R
inst✝¹ : Semiring α
inst✝ : Algebra R α
r : R
i j : n
⊢ diagonal ((Pi.constRingHom n α) (Algebra.algebraMap r)) i j = if i = j then Algebra.algebraMap r else 0

Tactic:
split_ifs with h <;> simp [h, Matrix.one_apply_ne]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_const_add (c : F) :
    fderivWithin 𝕜 (fun y => c + f y) s x = fderivWithin 𝕜 f s x

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
f : E → F
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y => c + f y) s x = fderivWithin 𝕜 f s x

Tactic:
simpa only [add_comm] using fderivWithin_add_const c

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ball_disjoint_closedBall (h : δ + ε ≤ dist x y) : Disjoint (ball x δ) (closedBall y ε) :=
  (closedBall_disjoint_ball <| by rwa [add_comm, dist_comm]).symm

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε ≤ dist x y
⊢ ε + δ ≤ dist y x

Tactic:
rwa [add_comm, dist_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_sub_right_of_add_le {a b c : Int} (h : a + b ≤ c) : a ≤ c - b

Proof state:
a b c : Int
h : a + b ≤ c
⊢ a ≤ c - b

Tactic:
have h := Int.add_le_add_right h (-b)

Result:
a b c : Int
h✝ : a + b ≤ c
h : a + b + -b ≤ c + -b
⊢ a ≤ c - b

Proof state:
a b c : Int
h✝ : a + b ≤ c
h : a + b + -b ≤ c + -b
⊢ a ≤ c - b

Tactic:
rwa [Int.add_neg_cancel_right] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    (hl : DistinctKeys l) (hka : k == a) : getEntry? a (eraseKey k l) = none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
hka : (k == a) = true
⊢ getEntry? a (eraseKey k l) = none

Tactic:
rw [← getEntry?_congr hka, getEntry?_eraseKey_self hl]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem mem_closed_iff_bsup (hs : IsClosed s) :
    a ∈ s ↔
      ∃ (o : Ordinal) (_ho : o ≠ 0) (f : ∀ a < o, Ordinal),
        (∀ i hi, f i hi ∈ s) ∧ bsup.{u, u} o f = a

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Tactic:
rw [← mem_closure_iff_bsup, hs.closure_eq]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_pow₀ (ha : 1 < a) : ∀ {n : ℕ}, n ≠ 0 → 1 < a ^ n
  | 0, h => (h rfl).elim
  | n + 1, _ => by rw [pow_succ']; exact one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a ^ (n + 1)

Tactic:
rw [pow_succ']

Result:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n

Tactic:
exact one_lt_mul_of_lt_of_le ha (one_le_pow₀ ha.le)

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem normalClosure_eq_iInf :
    normalClosure s = ⨅ (N : Subgroup G) (_ : Normal N) (_ : s ⊆ N), N :=
  le_antisymm (le_iInf fun _ => le_iInf fun _ => le_iInf normalClosure_le_normal)
    (iInf_le_of_le (normalClosure s)
      (iInf_le_of_le (by infer_instance) (iInf_le_of_le subset_normalClosure le_rfl)))

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ (normalClosure s).Normal

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_eq_zero (d0 : d ≠ 0) : mkRat n d = 0 ↔ n = 0

Proof state:
d : Nat
n : Int
d0 : d ≠ 0
⊢ mkRat n d = 0 ↔ n = 0

Tactic:
simp [mkRat_def, d0]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem map_lift_eq {m : β → γ} (hg : Monotone g) : map m (f.lift g) = f.lift (map m ∘ g) :=
  have : Monotone (map m ∘ g) := map_mono.comp hg
  Filter.ext fun s => by
    simp only [mem_lift_sets hg, mem_lift_sets this, exists_prop, mem_map, Function.comp_apply]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : β → γ
hg : Monotone g
this : Monotone (map m ∘ g)
s : Set γ
⊢ s ∈ map m (f.lift g) ↔ s ∈ f.lift (map m ∘ g)

Tactic:
simp only [mem_lift_sets hg, mem_lift_sets this, exists_prop, mem_map, Function.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_self {x : BitVec w} : x &&& x = x

Proof state:
w : Nat
x : BitVec w
⊢ x &&& x = x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& x).getLsbD i = x.getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& x).getLsbD i = x.getLsbD i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.1.size = l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (insertMany empty l).val.val.size = l.length

Tactic:
rw [size_insertMany_list _ Raw.WF.empty₀ distinct]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ empty.val.size + l.length = l.length

α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ ∀ (a : α), empty.contains a = true → (List.map Prod.fst l).contains a = false

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ empty.val.size + l.length = l.length

Tactic:
simp only [size_empty, Nat.zero_add]

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ ∀ (a : α), empty.contains a = true → (List.map Prod.fst l).contains a = false

Tactic:
simp only [contains_empty, Bool.false_eq_true, false_implies, implies_true]

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem mem_ndinter {s t : Multiset α} {a : α} : a ∈ ndinter s t ↔ a ∈ s ∧ a ∈ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t

Tactic:
simp [ndinter, mem_filter]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_top_eq_top_of_infinite (V : Type*) [Infinite V] :
    (⊤ : SimpleGraph V).chromaticNumber = ⊤

Proof state:
V : Type u_3
inst✝ : Infinite V
hc : ∃ n, ⊤.Colorable n
⊢ False

Tactic:
obtain ⟨n, ⟨hn⟩⟩ := hc

Result:
case intro.intro
V : Type u_3
inst✝ : Infinite V
n : ℕ
hn : ⊤.Coloring (Fin n)
⊢ False

Proof state:
V : Type u_3
inst✝ : Infinite V
⊢ ⊤.chromaticNumber = ⊤

Tactic:
by_contra hc

Result:
V : Type u_3
inst✝ : Infinite V
hc : ¬⊤.chromaticNumber = ⊤
⊢ False

Proof state:
V : Type u_3
inst✝ : Infinite V
hc : ¬⊤.chromaticNumber = ⊤
⊢ False

Tactic:
rw [← Ne, chromaticNumber_ne_top_iff_exists] at hc

Result:
V : Type u_3
inst✝ : Infinite V
hc : ∃ n, ⊤.Colorable n
⊢ False

Proof state:
case intro.intro
V : Type u_3
inst✝ : Infinite V
n : ℕ
hn : ⊤.Coloring (Fin n)
⊢ False

Tactic:
exact not_injective_infinite_finite _ hn.injective_of_top_hom

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem isCaratheodory_inter (h₁ : IsCaratheodory m s₁) (h₂ : IsCaratheodory m s₂) :
    IsCaratheodory m (s₁ ∩ s₂)

Proof state:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)

Tactic:
exact isCaratheodory_union _ (isCaratheodory_compl _ h₁) (isCaratheodory_compl _ h₂)

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ ∩ s₂)

Tactic:
rw [← isCaratheodory_compl_iff, Set.compl_inter]

Result:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
⊢ m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDerivWithin_comp_sub (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s x =
      iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z => f (z - a)) s x = iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

Tactic:
simp [iteratedFDerivWithin_comp_sub']

Result:
no goals