harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational (ξ : ℝ) :
    {q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2}.Infinite ↔ Irrational ξ

Proof state:
case h.e'_2.h.e'_2.h.a
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2

Tactic:
norm_cast

Result:
no goals

Proof state:
ξ : ℝ
⊢ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite ↔ Irrational ξ

Tactic:
refine
  ⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b H => Set.not_infinite.mpr ?_ h,
    Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩

Result:
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
⊢ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite

Proof state:
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
⊢ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite

Tactic:
convert Rat.finite_rat_abs_sub_lt_one_div_den_sq ((a : ℚ) / b) with q

Result:
case h.e'_2.h.e'_2.h.a
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ |ξ - ↑q| < 1 / ↑q.den ^ 2 ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2

Proof state:
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = 1 / ↑q.den ^ 2

Tactic:
rfl

Result:
no goals

Proof state:
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = ↑(1 / ↑q.den ^ 2)

Tactic:
(push_cast; rfl)

Result:
no goals

Proof state:
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = ↑(1 / ↑q.den ^ 2)

Tactic:
push_cast

Result:
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = 1 / ↑q.den ^ 2

Proof state:
case h.e'_2.h.e'_2.h.a
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ |ξ - ↑q| < 1 / ↑q.den ^ 2 ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2

Tactic:
rw [H, (by (push_cast; rfl) : (1 : ℝ) / (q.den : ℝ) ^ 2 = (1 / (q.den : ℚ) ^ 2 : ℚ))]

Result:
case h.e'_2.h.e'_2.h.a
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem hasCompactSupport_normed : HasCompactSupport (f.normed μ)

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ HasCompactSupport (f.normed μ)

Tactic:
simp only [HasCompactSupport, f.tsupport_normed_eq (μ := μ), isCompact_closedBall]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_left_injective : Function.Injective fun a ↦ a / b

Proof state:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a => a / b

Tactic:
simp only [div_eq_mul_inv]

Result:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a => a * b⁻¹

Proof state:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a => a * b⁻¹

Tactic:
exact fun a a' h ↦ mul_left_injective b⁻¹ h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_zero : logb b 0 = 0

Proof state:
b : ℝ
⊢ logb b 0 = 0

Tactic:
simp [logb]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk0_eq_mk0_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} :
    ClassGroup.mk0 I = ClassGroup.mk0 J ↔
      ∃ (x y : R) (_hx : x ≠ 0) (_hy : y ≠ 0), Ideal.span {x} * (I : Ideal R) =
      Ideal.span {y} * J

Proof state:
case refine_1.intro.intro.intro.intro.mk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

Tactic:
refine ⟨x, y, ?_, mem_nonZeroDivisors_iff_ne_zero.mp hy, ?_⟩

Result:
case refine_1.intro.intro.intro.intro.mk.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ x ≠ 0

case refine_1.intro.intro.intro.intro.mk.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

Proof state:
case refine_2.intro.intro.intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J

Tactic:
refine ⟨IsLocalization.mk' _ x ⟨y, hy'⟩, ?_, ?_⟩

Result:
case refine_2.intro.intro.intro.intro.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ mk' (FractionRing R) x ⟨y, hy'⟩ ≠ 0

case refine_2.intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy'⟩) * ↑↑I = ↑↑J
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_compl_mul_self_apply (s : Set α) (f : α → M) (a : α) :
    mulIndicator sᶜ f a * mulIndicator s f a = f a :=
  by_cases (fun ha : a ∈ s => by simp [ha]) fun ha => by simp [ha]

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ sᶜ.mulIndicator f a * s.mulIndicator f a = f a

Tactic:
simp [ha]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∉ s
⊢ sᶜ.mulIndicator f a * s.mulIndicator f a = f a

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
@[instance 100]
lemma of_isAffineHom [h : IsAffineHom f] : IsSeparated f

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated f

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff @IsSeparated (arrowIsoSpecΓOfIsAffine f)]

Result:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated (Spec.map (Scheme.Hom.appTop f))

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated (Spec.map (Scheme.Hom.appTop f))

Tactic:
infer_instance

Result:
no goals

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ IsSeparated f

Tactic:
rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := @IsSeparated) _
  (iSup_affineOpens_eq_top Y)]

Result:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), IsSeparated (f ∣_ ↑i)

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
⊢ IsSeparated f

Tactic:
have : IsAffine X := HasAffineProperty.iff_of_isAffine.mp h

Result:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
this : IsAffine X
⊢ IsSeparated f

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
H : IsAffineHom (f ∣_ ↑U)
⊢ IsSeparated (f ∣_ ↑U)

Tactic:
exact this _ U.2

Result:
no goals

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), IsSeparated (f ∣_ ↑i)

Tactic:
intro U

Result:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
⊢ IsSeparated (f ∣_ ↑U)

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
⊢ IsSeparated (f ∣_ ↑U)

Tactic:
have H : IsAffineHom (f ∣_ U) := IsLocalAtTarget.restrict h U

Result:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
U : ↑Y.affineOpens
H : IsAffineHom (f ∣_ ↑U)
⊢ IsSeparated (f ∣_ ↑U)

Proof state:
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
⊢ IsSeparated f

Tactic:
wlog hY : IsAffine Y

Result:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ IsSeparated f

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
hY : IsAffine Y
⊢ IsSeparated f
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one (n : ℕ) : adicAbv v n ≤ 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
n : ℕ
⊢ (adicAbv v) ↑n ≤ 1

Tactic:
simp only [← FinitePlace.norm_def, map_natCast, IsUltrametricDist.norm_natCast_le_one]

Result:
no goals
-- Mathlib/Order/SuccPred/Tree.lean
lemma isAtom_findAtom {r : α} (hr : r ≠ ⊥) :
    IsAtom (findAtom r)

Proof state:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ ∀ b < findAtom r, b = ⊥

Tactic:
intro b hb

Result:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b < findAtom r
⊢ b = ⊥

Proof state:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b < findAtom r
⊢ b = ⊥

Tactic:
apply Order.le_pred_of_lt at hb

Result:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b ≤ Order.pred (findAtom r)
⊢ b = ⊥

Proof state:
case left
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ findAtom r ≠ ⊥

Tactic:
simp [hr]

Result:
no goals

Proof state:
case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b ≤ Order.pred (findAtom r)
⊢ b = ⊥

Tactic:
simpa using hb

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ IsAtom (findAtom r)

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ findAtom r ≠ ⊥

case right
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ ∀ b < findAtom r, b = ⊥
-- Mathlib/Algebra/DualNumber.lean
theorem algHom_ext ⦃f g : R[ε] →ₐ[R] A⦄ (hε : f ε = g ε) : f = g

Proof state:
case hinr.h
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : R[ε] →ₐ[R] A
hε : f ε = g ε
⊢ f (1 • ε) = g (1 • ε)

Tactic:
simp only [one_smul, hε]

Result:
no goals

Proof state:
case hinr.h
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : R[ε] →ₐ[R] A
hε : f ε = g ε
⊢ (f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton R R[ε] ε)) 1 =
    (g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton R R[ε] ε)) 1

Tactic:
dsimp

Result:
case hinr.h
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : R[ε] →ₐ[R] A
hε : f ε = g ε
⊢ f (1 • ε) = g (1 • ε)

Proof state:
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : R[ε] →ₐ[R] A
hε : f ε = g ε
⊢ f = g

Tactic:
ext

Result:
case hinr.h
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : R[ε] →ₐ[R] A
hε : f ε = g ε
⊢ (f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton R R[ε] ε)) 1 =
    (g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton R R[ε] ε)) 1
-- Mathlib/AlgebraicGeometry/ResidueField.lean
lemma range_fromSpecResidueField (x : X.carrier) :
    Set.range (X.fromSpecResidueField x).base = {x}

Proof state:
case h
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecResidueField x).base) ↔ s ∈ {x}

Tactic:
simp only [Set.mem_range, fromSpecResidueField_apply, Set.mem_singleton_iff, eq_comm (a := s)]

Result:
case h
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ (∃ y, x = s) ↔ x = s

Proof state:
case h.mpr
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ x = s → ∃ y, x = s

Tactic:
rintro rfl

Result:
case h.mpr
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ ∃ y, x = x

Proof state:
case h
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ (∃ y, x = s) ↔ x = s

Tactic:
constructor

Result:
case h.mp
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ (∃ y, x = s) → x = s

case h.mpr
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ x = s → ∃ y, x = s

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ Set.range ⇑(ConcreteCategory.hom (X.fromSpecResidueField x).base) = {x}

Tactic:
ext s

Result:
case h
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (X.fromSpecResidueField x).base) ↔ s ∈ {x}

Proof state:
case h.mp.intro
X : Scheme
x s : ↑↑X.toPresheafedSpace
h : x = s
⊢ x = s

Tactic:
exact h

Result:
no goals

Proof state:
case h.mpr
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ ∃ y, x = x

Tactic:
exact ⟨closedPoint (X.residueField x), rfl⟩

Result:
no goals

Proof state:
case h.mp
X : Scheme
x s : ↑↑X.toPresheafedSpace
⊢ (∃ y, x = s) → x = s

Tactic:
rintro ⟨-, h⟩

Result:
case h.mp.intro
X : Scheme
x s : ↑↑X.toPresheafedSpace
h : x = s
⊢ x = s
-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma parallelComp_comp_prod {η : Kernel β γ} [IsSFiniteKernel η]
    {κ' : Kernel α β'} [IsSFiniteKernel κ'] {η' : Kernel β' γ'} [IsSFiniteKernel η'] :
    (η ∥ₖ η') ∘ₖ (κ ×ₖ κ') = (η ∘ₖ κ) ×ₖ (η' ∘ₖ κ')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
β' : Type u_6
γ' : Type u_7
mβ' : MeasurableSpace β'
mγ' : MeasurableSpace γ'
inst✝³ : IsSFiniteKernel κ
η : Kernel β γ
inst✝² : IsSFiniteKernel η
κ' : Kernel α β'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel β' γ'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ×ₖ κ') = η ∘ₖ κ ×ₖ (η' ∘ₖ κ')

Tactic:
rw [← parallelComp_comp_copy, ← comp_assoc, parallelComp_comp_parallelComp,
  ← parallelComp_comp_copy]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Prod.lean
lemma prod_fac₂ :
    W₂.Q ⋙ (curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip

Proof state:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₂.Q ⋙ (curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip

Tactic:
simp only [prodLift, Functor.curry_obj_uncurry_obj, Functor.flip_flip]

Result:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₂.Q ⋙ Construction.lift (prodLift₁ F hF).flip ⋯ = (prodLift₁ F hF).flip

Proof state:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₂.Q ⋙ Construction.lift (prodLift₁ F hF).flip ⋯ = (prodLift₁ F hF).flip

Tactic:
apply Construction.fac

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_empty : (#v[] : Vector α 0).toArray = #[]

Proof state:
α : Type u_1
⊢ { toArray := #[], size_toArray := ⋯ }.toArray = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatchingFree.mono {G G' : SimpleGraph V} (h : G ≤ G') (hmf : G'.IsMatchingFree) :
    G.IsMatchingFree

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
⊢ G.IsMatchingFree

Tactic:
intro x

Result:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
⊢ ¬x.IsPerfectMatching

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ False

Tactic:
apply hmf (x.map (SimpleGraph.Hom.ofLE h))

Result:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ (Subgraph.map (Hom.ofLE h) x).IsPerfectMatching

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ (Subgraph.map (Hom.ofLE h) x).verts

Tactic:
simp only [Subgraph.map_verts, Hom.coe_ofLE, id_eq, Set.image_id']

Result:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ x.verts

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ (Subgraph.map (Hom.ofLE h) x).IsPerfectMatching

Tactic:
refine ⟨hc.1.map_ofLE h, ?_⟩

Result:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ (Subgraph.map (Hom.ofLE h) x).IsSpanning

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ x.verts

Tactic:
exact hc.2 v

Result:
no goals

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
⊢ ¬x.IsPerfectMatching

Tactic:
by_contra! hc

Result:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ False

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ (Subgraph.map (Hom.ofLE h) x).IsSpanning

Tactic:
intro v

Result:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ (Subgraph.map (Hom.ofLE h) x).verts
-- Mathlib/Probability/Martingale/Convergence.lean
theorem Submartingale.exists_ae_trim_tendsto_of_bdd [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (hbdd : ∀ n, eLpNorm (f n) 1 μ ≤ R) :
    ∀ᵐ ω ∂μ.trim (sSup_le fun _ ⟨_, hn⟩ => hn ▸ ℱ.le _ : ⨆ n, ℱ n ≤ m0),
      ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Tactic:
rw [ae_iff, trim_measurableSet_eq]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ μ {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)} = 0

case hs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ MeasurableSet {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)}

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ μ {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)} = 0

Tactic:
exact hf.exists_ae_tendsto_of_bdd hbdd

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Tactic:
letI := (⨆ n, ℱ n)

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ ∀ᵐ (ω : Ω) ∂μ.trim ⋯, ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)

Proof state:
case hs
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
this : MeasurableSpace Ω := ⨆ n, ↑ℱ n
⊢ MeasurableSet {a | ¬∃ c, Tendsto (fun n => f n a) atTop (𝓝 c)}

Tactic:
exact MeasurableSet.compl <| measurableSet_exists_tendsto
  fun n => (hf.stronglyMeasurable n).measurable.mono (le_sSup ⟨n, rfl⟩) le_rfl

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem convexHull_union_neg_eq_absConvexHull {s : Set E} :
    convexHull ℝ (s ∪ -s) = absConvexHull ℝ s

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (balancedHull ℝ s) ≤ (convexHull ℝ) (s ∪ -s)

Tactic:
rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (balancedHull ℝ s) ≤ (convexHull ℝ) ((convexHull ℝ) (s ∪ -s))

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ‖-1‖ ≤ 1 ∧ x✝¹ ∈ -1 • s

Tactic:
aesop

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x✝¹ ∈ r • s

Tactic:
use -1

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ‖-1‖ ≤ 1 ∧ x✝¹ ∈ -1 • s

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (balancedHull ℝ s) ≤ (convexHull ℝ) ((convexHull ℝ) (s ∪ -s))

Tactic:
exact convexHull_mono balancedHull_subset_convexHull_union_neg

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (s ∪ -s) = (convexHull ℝ) (balancedHull ℝ s)

Tactic:
exact le_antisymm (convexHull_mono (union_subset (subset_balancedHull ℝ)
  (fun _ _ => by rw [mem_balancedHull_iff]; use -1; aesop)))
  (by
    rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]
    exact convexHull_mono balancedHull_subset_convexHull_union_neg)

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (s ∪ -s) = (absConvexHull ℝ) s

Tactic:
rw [absConvexHull_eq_convexHull_balancedHull]

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ (convexHull ℝ) (s ∪ -s) = (convexHull ℝ) (balancedHull ℝ s)

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ x✝¹ ∈ balancedHull ℝ s

Tactic:
rw [mem_balancedHull_iff]

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ -s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x✝¹ ∈ r • s