harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Bochner.lean
/-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x ∂μ`. -/
lemma tendsto_integral_of_L1' {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G} {l : Filter ι}
    (hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)) :
    Tendsto (fun i ↦ ∫ x, F i x ∂μ) l (𝓝 (∫ x, f x ∂μ))

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
refine tendsto_integral_of_L1 f hfi hFi ?_

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
exact hF

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => eLpNorm (F i - f) 1 μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : Integrable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_natCast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0

Proof state:
R : Type u
m n : ℕ
inst✝ : Semiring R
⊢ (↑m).coeff n = ↑(if n = 0 then m else 0)

Tactic:
simp only [← C_eq_natCast, coeff_C, Nat.cast_ite, Nat.cast_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem unit_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
    (x : C) : adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) =
      adj2.unit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x

Tactic:
rw [← adj2.unit_naturality_assoc, ← G'.map_comp]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x) ≫ adj1.counit.app (F.obj x)) = adj2.unit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ (adj1.rightAdjointUniq adj2).hom.app (F.obj x) = adj2.unit.app x

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, conjugateIsoEquiv_apply_hom,
  Iso.refl_hom, conjugateEquiv_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ adj2.unit.app (G.obj (F.obj x)) ≫ G'.map (adj1.counit.app (F.obj x)) = adj2.unit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj2.unit.app x ≫ G'.map (F.map (adj1.unit.app x) ≫ adj1.counit.app (F.obj x)) = adj2.unit.app x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasStrictFDerivAt_const_add_iff (c : F) :
    HasStrictFDerivAt (c + f ·) f' x ↔ HasStrictFDerivAt f f' 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
f' : E →L[𝕜] F
x : E
c : F
⊢ HasStrictFDerivAt (fun x => c + f x) f' x ↔ HasStrictFDerivAt f f' x

Tactic:
simpa only [add_comm] using hasStrictFDerivAt_add_const_iff c

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem rotateRight_replicate (n) (a : α) : rotateRight (replicate m a) n = replicate m a

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
⊢ 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m

Tactic:
intro h

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m

Proof state:
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
this : (n + 1) % m < m
⊢ m - (n + 1) % m ≤ m

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m > 0

Tactic:
omega

Result:
no goals

Proof state:
case zero
α : Type u_1
m : Nat
a : α
⊢ (replicate m a).rotateRight 0 = replicate m a

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
⊢ m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m

Tactic:
have : (n + 1) % m < m := Nat.mod_lt _ (by omega)

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
this : (n + 1) % m < m
⊢ m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
⊢ (replicate m a).rotateRight (n + 1) = replicate m a

Tactic:
suffices 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m by
  simpa [rotateRight]

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
⊢ 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m

Proof state:
α : Type u_1
m n : Nat
a : α
⊢ (replicate m a).rotateRight n = replicate m a

Tactic:
cases n with
| zero => simp
| succ n =>
  suffices 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m by
    simpa [rotateRight]
  intro h
  have : (n + 1) % m < m := Nat.mod_lt _ (by omega)
  rw [Nat.min_eq_left (by omega)]
  omega

Result:
no goals

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
this : (n + 1) % m < m
⊢ m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m

Tactic:
rw [Nat.min_eq_left (by omega)]

Result:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
this : (n + 1) % m < m
⊢ m - (m - (n + 1) % m) + (m - (n + 1) % m) = m

Proof state:
α : Type u_1
m : Nat
a : α
n : Nat
this : 1 < m → m - (m - (n + 1) % m) + min (m - (n + 1) % m) m = m
⊢ (replicate m a).rotateRight (n + 1) = replicate m a

Tactic:
simpa [rotateRight]

Result:
no goals

Proof state:
case succ
α : Type u_1
m : Nat
a : α
n : Nat
h : 1 < m
this : (n + 1) % m < m
⊢ m - (m - (n + 1) % m) + (m - (n + 1) % m) = m

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem preimage_nhds_within_coinduced {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t)
    (ht : IsOpen t)
    (hs : s ∈ @nhds β (.coinduced (fun x : t => π x) inferInstance) (π a)) :
    π ⁻¹' s ∈ 𝓝 a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝[t] a

Tactic:
exact preimage_nhdsWithin_coinduced' h hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
rw [← ht.nhdsWithin_eq h]

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝[t] a
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_eq_inv_mul_cond_mul (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : Measure Ω)
    [IsFiniteMeasure μ] : μ[t|s] = (μ s)⁻¹ * μ[s|t] * μ t

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
s t : Set Ω
hms : MeasurableSet s
hmt : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ μ[t | s] = (μ s)⁻¹ * μ[s | t] * μ t

Tactic:
rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem C_eq_intCast (n : ℤ) : C (n : R) = n

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

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
lemma nondegenerate_iff (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm) :
    B.Nondegenerate ↔ ∀ x, B x x = 0 ↔ x = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ Nondegenerate B ↔ ∀ (x : M), (B x) x = 0 ↔ x = 0

Tactic:
simp_rw [hB.isRefl.nondegenerate_iff_separatingLeft, separatingLeft_iff_ker_eq_bot,
  Submodule.eq_bot_iff, B.apply_apply_same_eq_zero_iff hs hB, mem_ker]

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ (∀ (x : M), B x = 0 → x = 0) ↔ ∀ (x : M), B x = 0 ↔ x = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
⊢ B x = 0 → x = 0 ↔ (B x = 0 ↔ x = 0)

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ (∀ (x : M), B x = 0 → x = 0) ↔ ∀ (x : M), B x = 0 ↔ x = 0

Tactic:
exact forall_congr' fun x ↦ by aesop

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem bind_zero_right (m : Measure α) : bind m (0 : α → Measure β) = 0

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (0 a) s ∂m = 0

Tactic:
simp only [Pi.zero_apply, coe_zero, lintegral_const, zero_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
⊢ m.bind 0 = 0

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ (m.bind 0) s = 0 s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ (m.bind 0) s = 0 s

Tactic:
simp only [bind, hs, join_apply, coe_zero, Pi.zero_apply]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), μ s ∂map 0 m = 0

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), μ s ∂map 0 m = 0

Tactic:
rw [lintegral_map (measurable_coe hs) measurable_zero]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (0 a) s ∂m = 0
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
theorem biInter_gt_closedBall (x : α) (r : ℝ) : ⋂ r' > r, closedBall x r' = closedBall x r

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ r', ⋂ (_ : r' > r), closedBall x r' = closedBall x r

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋂ r', ⋂ (_ : r' > r), closedBall x r' ↔ x✝ ∈ closedBall x r

Proof state:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋂ r', ⋂ (_ : r' > r), closedBall x r' ↔ x✝ ∈ closedBall x r

Tactic:
simp [forall_gt_imp_ge_iff_le_of_dense]

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingNorm_smul [Zero α] [∀ i, SMulWithZero α (β i)] {k : α}
    (hk : ∀ i, IsSMulRegular (β i) k) (x : ∀ i, β i) : hammingNorm (k • x) = hammingNorm x :=
  hammingNorm_comp (fun i (c : β i) => k • c) hk fun i => by simp_rw [smul_zero]

Proof state:
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : Zero α
inst✝ : (i : ι) → SMulWithZero α (β i)
k : α
hk : ∀ (i : ι), IsSMulRegular (β i) k
x : (i : ι) → β i
i : ι
⊢ (fun i c => k • c) i 0 = 0

Tactic:
simp_rw [smul_zero]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem singleton_smul (a : A) (M : Submodule R A) :
    Set.up ({a} : Set A) • M = M.map (LinearMap.mulLeft R a)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ span R ((fun x => a * x) '' ↑M) = map (LinearMap.mulLeft R a) M

Tactic:
exact (map (LinearMap.mulLeft R a) M).span_eq

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ Set.up {a} • M = map (LinearMap.mulLeft R a) M

Tactic:
conv_lhs => rw [← span_eq M]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ Set.up {a} • span R ↑M = map (LinearMap.mulLeft R a) M

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ Set.up {a} • span R ↑M = map (LinearMap.mulLeft R a) M

Tactic:
rw [setSemiring_smul_def, SetSemiring.down_up, span_mul_span, singleton_mul]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ span R ((fun x => a * x) '' ↑M) = map (LinearMap.mulLeft R a) M
-- Mathlib/FieldTheory/SplittingField/Construction.lean
theorem factor_dvd_of_not_isUnit {f : K[X]} (hf1 : ¬IsUnit f) : factor f ∣ f

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
⊢ f.factor ∣ f

Tactic:
by_cases hf2 : f = 0

Result:
case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ f.factor ∣ f

case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ f.factor ∣ f

Proof state:
case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ f.factor ∣ f

Tactic:
rw [factor, dif_pos (WfDvdMonoid.exists_irreducible_factor hf1 hf2)]

Result:
case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose ⋯ ∣ f

Proof state:
case neg
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : ¬f = 0
⊢ Classical.choose ⋯ ∣ f

Tactic:
exact (Classical.choose_spec <| WfDvdMonoid.exists_irreducible_factor hf1 hf2).2

Result:
no goals

Proof state:
case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ f.factor ∣ f

Tactic:
rw [hf2]

Result:
case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor 0 ∣ 0

Proof state:
case pos
K : Type v
inst✝ : Field K
f : K[X]
hf1 : ¬IsUnit f
hf2 : f = 0
⊢ factor 0 ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem polynomialFunctions_separatesPoints (X : Set R) : (polynomialFunctions X).SeparatesPoints :=
  fun x y h => by
  -- We use `Polynomial.X`, then clean up.
  refine ⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, ?_⟩⟩
  dsimp; simp only [Polynomial.eval_X]
  exact fun h' => h (Subtype.ext h')

Proof state:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X

Tactic:
simp only [Polynomial.eval_X]

Result:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬↑x = ↑y

Proof state:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ (fun f => ⇑f) (↑(toContinuousMapOnAlgHom X) Polynomial.X) x ≠
    (fun f => ⇑f) (↑(toContinuousMapOnAlgHom X) Polynomial.X) y

Tactic:
dsimp

Result:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬eval (↑x) Polynomial.X = eval (↑y) Polynomial.X

Proof state:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(polynomialFunctions X), f x ≠ f y

Tactic:
refine ⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, ?_⟩⟩

Result:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ (fun f => ⇑f) (↑(toContinuousMapOnAlgHom X) Polynomial.X) x ≠
    (fun f => ⇑f) (↑(toContinuousMapOnAlgHom X) Polynomial.X) y

Proof state:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x y : ↑X
h : x ≠ y
⊢ ¬↑x = ↑y

Tactic:
exact fun h' => h (Subtype.ext h')

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_radical : comap f (radical K) = radical (comap f K)

Proof state:
case h
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
x✝ : R
⊢ x✝ ∈ comap f K.radical ↔ x✝ ∈ (comap f K).radical

Tactic:
simp [radical]

Result:
no goals

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K.radical = (comap f K).radical

Tactic:
ext

Result:
case h
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
x✝ : R
⊢ x✝ ∈ comap f K.radical ↔ x✝ ∈ (comap f K).radical
-- Mathlib/Order/RelSeries.lean
@[simp] lemma head_smash {p q : RelSeries r} (h : p.last = q.head) :
    (smash p q h).head = p.head

Proof state:
case h.e'_3.e_a
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
H : p.length = 0
⊢ 0 = Fin.last p.length

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ p.length = 0 → q.toFun 0 = p.toFun 0

Tactic:
intro H

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
H : p.length = 0
⊢ q.toFun 0 = p.toFun 0

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ (p.smash q h).head = p.head

Tactic:
delta head smash

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ { length := p.length + q.length,
          toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩, step := ⋯ }.toFun
      0 =
    p.toFun 0

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ { length := p.length + q.length,
          toFun := fun i => if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩, step := ⋯ }.toFun
      0 =
    p.toFun 0

Tactic:
simp only [Fin.val_zero, Fin.zero_eta, zero_le, Nat.sub_eq_zero_of_le, dite_eq_ite,
  ite_eq_left_iff, not_lt, nonpos_iff_eq_zero]

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
⊢ p.length = 0 → q.toFun 0 = p.toFun 0

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
H : p.length = 0
⊢ q.toFun 0 = p.toFun 0

Tactic:
convert h.symm

Result:
case h.e'_3
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
H : p.length = 0
⊢ p.toFun 0 = p.last

Proof state:
case h.e'_3
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
H : p.length = 0
⊢ p.toFun 0 = p.last

Tactic:
congr

Result:
case h.e'_3.e_a
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
H : p.length = 0
⊢ 0 = Fin.last p.length
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem mapRange_id : v.mapRange (AddMonoidHom.id M) continuous_id = v

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
⊢ v.mapRange (AddMonoidHom.id M) ⋯ = v

Tactic:
ext

Result:
case h
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(v.mapRange (AddMonoidHom.id M) ⋯) i✝ = ↑v i✝

Proof state:
case h
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(v.mapRange (AddMonoidHom.id M) ⋯) i✝ = ↑v i✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem comp_neg_X_comp_neg_X {R : Type*} [CommRing R] (p : R[X]) :
    (p.comp (-X)).comp (-X) = p

Proof state:
R : Type u_3
inst✝ : CommRing R
p : R[X]
⊢ p.comp ((-X).comp (-X)) = p

Tactic:
simp only [neg_comp, X_comp, neg_neg, comp_X]

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommRing R
p : R[X]
⊢ (p.comp (-X)).comp (-X) = p

Tactic:
rw [comp_assoc]

Result:
R : Type u_3
inst✝ : CommRing R
p : R[X]
⊢ p.comp ((-X).comp (-X)) = p
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a fallback : α} {v : β k} :
    (m.insert k v).getKeyD a fallback =
      if k == a then k else m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a fallback : α
v : β k
⊢ (m.insert k v).getKeyD a fallback = if (k == a) = true then k else m.getKeyD a fallback

Tactic:
simp_to_model [insert] using List.getKeyD_insertEntry

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioi_subset_Ioi (h : a ≤ b) : Ioi b ⊆ Ioi a

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a ≤ b
⊢ Ioi b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioi_subset_Ioi h

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
lemma IsFinite.iff_isProper_and_isAffineHom :
    IsFinite f ↔ IsProper f ∧ IsAffineHom f

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsProper f ∧ IsAffineHom f

Tactic:
rw [eq_isProper_inf_isAffineHom]

Result:
X Y : Scheme
f : X ⟶ Y
⊢ (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_map {g : β → γ} {f : α → β} (hg : Measurable g) (hf : Measurable f) :
    (μ.map f).map g = μ.map (g ∘ f) :=
  ext fun s hs => by simp [hf, hg, hs, hg hs, hg.comp hf, ← preimage_comp]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : Measurable g
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ (map g (map f μ)) s = (map (g ∘ f) μ) s

Tactic:
simp [hf, hg, hs, hg hs, hg.comp hf, ← preimage_comp]

Result:
no goals