harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Basic.lean
theorem isClosed_iff_frequently : IsClosed s ↔ ∀ x, (∃ᶠ y in 𝓝 x, y ∈ s) → x ∈ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
x : X
⊢ x ∈ closure s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
rw [mem_closure_iff_frequently]

Result:
no goals

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
rw [← closure_subset_iff_isClosed]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ closure s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ closure s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
refine forall_congr' fun x => ?_

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
x : X
⊢ x ∈ closure s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
-- Mathlib/NumberTheory/FLT/MasonStothers.lean
theorem abc_subcall {a b c w : k[X]} {hw : w ≠ 0} (wab : w = wronskian a b) (ha : a ≠ 0)
    (hb : b ≠ 0) (hc : c ≠ 0) (abc_dr_dvd_w : divRadical (a * b * c) ∣ w) :
      c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Proof state:
case a
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ ?n + c.natDegree < ?n + abc_r.natDegree

case n
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ ℕ

Tactic:
calc
  a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree := by
    rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
  _ = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
    rw [mul_comm _ (radical _), radical_mul_divRadical (a * b * c)]
  _ = abc_dr.natDegree + abc_r.natDegree := by
    rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) (radical_ne_zero (a * b * c))]
  _ < a.natDegree + b.natDegree + abc_r.natDegree := by
    exact Nat.add_lt_add_right abc_dr_ndeg_lt _

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
have abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree := by
  calc
    abc_dr.natDegree ≤ w.natDegree := Polynomial.natDegree_le_of_dvd abc_dr_dvd_w hw
    _ < a.natDegree + b.natDegree := by rw [wab] at hw ⊢; exact natDegree_wronskian_lt_add hw

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem EqualizerCondition.bijective_mapToEqualizer_pullback (P : Cᵒᵖ ⥤ Type*)
    (hP : EqualizerCondition P) : ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [HasPullback π π],
    Function.Bijective
      (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) pullback.condition)

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP : EqualizerCondition P
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
⊢ Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

Tactic:
specialize hP π _ (pullbackIsPullback π π)

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
hP : Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))
⊢ Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
⊢ Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)

Tactic:
rw [Function.bijective_iff_existsUnique]

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝¹ : EffectiveEpi π
inst✝ : HasPullback π π
hP :
  ∀ (y : P.obj (op X)),
    P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y =
        P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y →
      ∃! x, P.map π.op x = y
⊢ ∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}),
    ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem norm_mul_exp_arg_mul_I (x : ℂ) : ‖x‖ * exp (arg x * I) = x

Proof state:
x : ℂ
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl

⊢ ↑‖0‖ * cexp (↑(arg 0) * I) = 0

case inr
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Proof state:
case inl

⊢ ↑‖0‖ * cexp (↑(arg 0) * I) = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
x : ℂ
hx : x ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Tactic:
have : ‖x‖ ≠ 0 := norm_ne_zero_iff.mpr hx

Result:
case inr
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Proof state:
case inr
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Tactic:
apply Complex.ext <;> field_simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd {s : AffineSubspace ℝ P} {p₁ p₂ : P}
    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (r₁ r₂ : ℝ) {v : V} (hv : v ∈ s.directionᗮ) :
    dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
      dist p₁ p₂ * dist p₁ p₂ + (r₁ - r₂) * (r₁ - r₂) * (‖v‖ * ‖v‖) :=
  calc
    dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
        ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : ℝ
v : V
hv : v ∈ s.directionᗮ
⊢ dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) * dist (r₁ • v +ᵥ p₁) (r₂ • v +ᵥ p₂) =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖

Tactic:
rw [dist_eq_norm_vsub V (r₁ • v +ᵥ p₁), vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, sub_smul,
  add_comm, add_sub_assoc]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : ℝ
v : V
hv : v ∈ s.directionᗮ
⊢ ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + |r₁ - r₂| * |r₁ - r₂| * ‖v‖ * ‖v‖ =
    dist p₁ p₂ * dist p₁ p₂ + (r₁ - r₂) * (r₁ - r₂) * (‖v‖ * ‖v‖)

Tactic:
rw [dist_eq_norm_vsub V p₁, abs_mul_abs_self, mul_assoc]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : ℝ
v : V
hv : v ∈ s.directionᗮ
⊢ ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + ‖(r₁ - r₂) • v‖ * ‖(r₁ - r₂) • v‖ =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + |r₁ - r₂| * |r₁ - r₂| * ‖v‖ * ‖v‖

Tactic:
rw [norm_smul, Real.norm_eq_abs]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : ℝ
v : V
hv : v ∈ s.directionᗮ
⊢ ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + |r₁ - r₂| * ‖v‖ * (|r₁ - r₂| * ‖v‖) =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + |r₁ - r₂| * |r₁ - r₂| * ‖v‖ * ‖v‖

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : ℝ
v : V
hv : v ∈ s.directionᗮ
⊢ ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + |r₁ - r₂| * ‖v‖ * (|r₁ - r₂| * ‖v‖) =
    ‖p₁ -ᵥ p₂‖ * ‖p₁ -ᵥ p₂‖ + |r₁ - r₂| * |r₁ - r₂| * ‖v‖ * ‖v‖

Tactic:
ring

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_sup : (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
tauto

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
simp only [realize, max, realize_not, eq_iff_iff]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_eq_zero_iff_not_mem : indicator s 1 i = (0 : M₀) ↔ i ∉ s

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s : Set ι
i : ι
inst✝ : Nontrivial M₀
⊢ s.indicator 1 i = 0 ↔ i ∉ s

Tactic:
simp [indicator_apply, imp_false]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroOneClass M₀
s : Set ι
i : ι
inst✝ : Nontrivial M₀
⊢ s.indicator 1 i = 0 ↔ i ∉ s

Tactic:
classical simp [indicator_apply, imp_false]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem norm_integral_le_norm (f : α →₁ₛ[μ] E) : ‖integral f‖ ≤ ‖f‖

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
⊢ ‖integral f‖ ≤ ‖f‖

Tactic:
rw [integral, norm_eq_integral]

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
⊢ ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
⊢ ‖MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f)‖ ≤
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))

Tactic:
exact (toSimpleFunc f).norm_integral_le_integral_norm (SimpleFunc.integrable f)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f

Proof state:
α✝¹ : Type u_1
o : Option α✝¹
α✝ : Sort u_2
b : α✝
f : α✝¹ → α✝
⊢ (o.pelim b fun a x => f a) = o.elim b f

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem smul_cancel_of_non_zero_divisor {M R : Type*} [Monoid M] [NonUnitalNonAssocRing R]
    [DistribMulAction M R] (k : M) (h : ∀ x : R, k • x = 0 → x = 0) {a b : R} (h' : k • a = k • b) :
    a = b

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ k • (a - b) = 0

Tactic:
rw [smul_sub, h', sub_self]

Result:
no goals

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ a - b = 0

Tactic:
refine h _ ?_

Result:
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ k • (a - b) = 0

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ a = b

Tactic:
rw [← sub_eq_zero]

Result:
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : DistribMulAction M R
k : M
h : ∀ (x : R), k • x = 0 → x = 0
a b : R
h' : k • a = k • b
⊢ a - b = 0
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem map_exp_comap_re_atTop : map exp (comap re atTop) = cobounded ℂ

Proof state:
⊢ map cexp (comap re atTop) = cobounded ℂ

Tactic:
rw [← comap_exp_cobounded, map_comap, range_exp, inf_eq_left, le_principal_iff]

Result:
⊢ {0}ᶜ ∈ cobounded ℂ

Proof state:
⊢ {0}ᶜ ∈ cobounded ℂ

Tactic:
exact eventually_ne_cobounded _

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Ioc_mul_Ico_subset' (a b c d : α) : Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

Tactic:
rintro x ⟨y, ⟨hya, hyb⟩, z, ⟨hzc, hzd⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a < y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioo (a * c) (b * d)

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

Tactic:
have := mulRightMono_of_mulRightStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this✝ : MulLeftMono α
this : MulRightMono α
y : α
hya : a < y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun x1 x2 => x1 * x2) y z ∈ Ioo (a * c) (b * d)

Tactic:
exact ⟨mul_lt_mul_of_lt_of_le hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Result:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.image_isVonNBounded_iff_seminorm_bounded (f : G → E) {s : Set G}
    (hp : WithSeminorms p) :
    Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i (f x) < r

Proof state:
𝕜 : Type u_1
E : Type u_5
G : Type u_7
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
f : G → E
s : Set G
hp : WithSeminorms p
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) (f x) < r

Tactic:
simp_rw [hp.isVonNBounded_iff_seminorm_bounded, Set.forall_mem_image]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousWithinAt.diff_iff
    (ht : ContinuousWithinAt f t x) : ContinuousWithinAt f (s \ t) x ↔ ContinuousWithinAt f s x :=
  ⟨fun h => (h.union ht).mono <| by simp only [diff_union_self, subset_union_left], fun h =>
    h.mono diff_subset⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
ht : ContinuousWithinAt f t x
h : ContinuousWithinAt f (s \ t) x
⊢ s ⊆ s \ t ∪ t

Tactic:
simp only [diff_union_self, subset_union_left]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain'_reverse : ∀ {l}, Chain' R (reverse l) ↔ Chain' (flip R) l
  | [] => Iff.rfl
  | [a] => by simp only [chain'_singleton, reverse_singleton]
  | a :: b :: l => by
    rw [chain'_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
      chain'_split, ← reverse_cons, @chain'_reverse (b :: l), and_comm, chain'_pair, flip]

Proof state:
α : Type u
R : α → α → Prop
a : α
⊢ Chain' R [a].reverse ↔ Chain' (flip R) [a]

Tactic:
simp only [chain'_singleton, reverse_singleton]

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a b : α
l : List α
⊢ Chain' R (a :: b :: l).reverse ↔ Chain' (flip R) (a :: b :: l)

Tactic:
rw [chain'_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
  chain'_split, ← reverse_cons, @chain'_reverse (b :: l), and_comm, chain'_pair, flip]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_replace [LawfulBEq α] {l : List α} {i : Nat} :
    (l.replace a b)[i]? = if l[i]? == some a then if a ∈ l.take i then some a else some b else l[i]?

Proof state:
case cons.succ
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
x : α
xs : List α
ih :
  ∀ {i : Nat},
    (xs.replace a b)[i]? = if (xs[i]? == some a) = true then if a ∈ take i xs then some a else some b else xs[i]?
n✝ : Nat
⊢ ((x :: xs).replace a b)[n✝ + 1]? =
    if ((x :: xs)[n✝ + 1]? == some a) = true then if a ∈ take (n✝ + 1) (x :: xs) then some a else some b
    else (x :: xs)[n✝ + 1]?

Tactic:
simp only [replace_cons]

Result:
case cons.succ
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
x : α
xs : List α
ih :
  ∀ {i : Nat},
    (xs.replace a b)[i]? = if (xs[i]? == some a) = true then if a ∈ take i xs then some a else some b else xs[i]?
n✝ : Nat
⊢ (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b)[n✝ + 1]? =
    if ((x :: xs)[n✝ + 1]? == some a) = true then if a ∈ take (n✝ + 1) (x :: xs) then some a else some b
    else (x :: xs)[n✝ + 1]?

Proof state:
case cons.succ
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
x : α
xs : List α
ih :
  ∀ {i : Nat},
    (xs.replace a b)[i]? = if (xs[i]? == some a) = true then if a ∈ take i xs then some a else some b else xs[i]?
n✝ : Nat
⊢ (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b)[n✝ + 1]? =
    if ((x :: xs)[n✝ + 1]? == some a) = true then if a ∈ take (n✝ + 1) (x :: xs) then some a else some b
    else (x :: xs)[n✝ + 1]?

Tactic:
split <;> split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
i : Nat
⊢ ([].replace a b)[i]? = if ([][i]? == some a) = true then if a ∈ take i [] then some a else some b else [][i]?

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma adj_edge {v w : V} : (edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w

Proof state:
V : Type u_1
s t v w : V
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)

Tactic:
tauto

Result:
no goals

Proof state:
V : Type u_1
s t v w : V
⊢ (edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w

Tactic:
simp only [edge_adj, ne_eq, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk,
  and_congr_left_iff]

Result:
V : Type u_1
s t v w : V
⊢ ¬v = w → (v = s ∧ w = t ∨ v = t ∧ w = s ↔ s = v ∧ t = w ∨ s = w ∧ t = v)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α}
    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
    getKeyD (insertManyIfNewUnit m l) k fallback = fallback

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k fallback : α
contains_eq_false : l.contains k = false
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKeyD k fallback = fallback

Tactic:
exact Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
  ⟨m.1, _⟩ m.2 not_mem contains_eq_false

Result:
no goals

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k fallback : α
not_mem : ¬k ∈ m
contains_eq_false : l.contains k = false
⊢ (insertManyIfNewUnit m l).getKeyD k fallback = fallback

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k fallback : α
contains_eq_false : l.contains k = false
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKeyD k fallback = fallback
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem symm_apply_mem_of_equiv_iff {I : Ideal R} {f : R ≃+* S} {y : S} :
    f.symm y ∈ I ↔ y ∈ I.map f

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
y : S
⊢ f.symm y ∈ I ↔ y ∈ map f I

Tactic:
rw [← comap_symm, mem_comap]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_add_C_pow (r : R) (n k : ℕ) :
    ((X + C r) ^ n).coeff k = r ^ (n - k) * (n.choose k : R)

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]

Result:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ n + 1 ≤ k → r ^ (n - k) * ↑(n.choose k) = 0

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

Tactic:
intro _ _ h

Result:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
h : b✝ ≠ k
⊢ (X ^ b✝).coeff k * r ^ (n - b✝) * ↑(n.choose b✝) = 0

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
h : b✝ ≠ k
⊢ (X ^ b✝).coeff k * r ^ (n - b✝) * ↑(n.choose b✝) = 0

Tactic:
simp [coeff_X_pow, h.symm]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∑ x ∈ range (n + 1), (X ^ x).coeff k * r ^ (n - x) * ↑(n.choose x) = r ^ (n - k) * ↑(n.choose k)

Tactic:
rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]

Result:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ n + 1 ≤ k → r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
intro h

Result:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * ↑(n.choose k) = 0

Proof state:
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ((X + C r) ^ n).coeff k = r ^ (n - k) * ↑(n.choose k)

Tactic:
rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, map_sum]

Result:
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∑ x ∈ range (n + 1), (lcoeff R k) (X ^ x * C r ^ (n - x) * ↑(n.choose x)) = r ^ (n - k) * ↑(n.choose k)

Proof state:
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∑ x ∈ range (n + 1), (lcoeff R k) (X ^ x * C r ^ (n - x) * ↑(n.choose x)) = r ^ (n - k) * ↑(n.choose k)

Tactic:
simp only [one_pow, mul_one, lcoeff_apply, ← C_eq_natCast, ← C_pow, coeff_mul_C, Nat.cast_id]

Result:
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∑ x ∈ range (n + 1), (X ^ x).coeff k * r ^ (n - x) * ↑(n.choose x) = r ^ (n - k) * ↑(n.choose k)

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]

Result:
no goals