harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero {f : E → F} {U : Set E}
    (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U)
    {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) :
    EqOn f 0 U

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
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
A : EqOn (⇑e ∘ f) 0 U
z : E
hz : z ∈ U
⊢ e (f z) = e 0

Tactic:
simpa only using A hz

Result:
no goals

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
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
A : EqOn (⇑e ∘ f) 0 U
z : E
hz : z ∈ U
⊢ f z = 0 z

Tactic:
have : e (f z) = e 0 := by simpa only using A hz

Result:
𝕜 : 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
U : Set E
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
z₀ : E
h₀ : z₀ ∈ U
hfz₀ : f =ᶠ[𝓝 z₀] 0
F' : Type u_3 := UniformSpace.Completion F
e : F →L[𝕜] F' := UniformSpace.Completion.toComplL
this✝ : AnalyticOnNhd 𝕜 (⇑e ∘ f) U
A : EqOn (⇑e ∘ f) 0 U
z : E
hz : z ∈ U
this : e (f z) = e 0
⊢ f z = 0 z
-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem range_finite [CompactSpace X] {f : X → Y} (hf : IsLocallyConstant f) :
    (Set.range f).Finite

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ (range f).Finite

Tactic:
haveI := discreteTopology_bot Y

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this✝ : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ (range f).Finite

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
⊢ (range f).Finite

Tactic:
letI : TopologicalSpace Y := ⊥

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ (range f).Finite

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this✝ : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ (range f).Finite

Tactic:
exact (isCompact_range hf.continuous).finite_of_discrete

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
lemma IsInvertedBy.iff_map_le_isomorphisms (W : MorphismProperty C) (F : C ⥤ D) :
    W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.IsInvertedBy F ↔ W.map F ≤ isomorphisms D

Tactic:
rw [iff_le_inverseImage_isomorphisms, map_le_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightShift_smul (a n' : ℤ) (hn' : n' + a = n) (x : R) :
    (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).rightShift a n' hn').v p q hpq = (x • γ.rightShift a n' hn').v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).rightShift a n' hn').v p q hpq = x • (γ.rightShift a n' hn').v p q hpq

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).rightShift a n' hn').v p q hpq = x • (γ.rightShift a n' hn').v p q hpq

Tactic:
simp only [rightShift_v _ a n' hn' p q hpq _ rfl, smul_v, Linear.smul_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
⊢ (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
p q : ℤ
hpq : p + n' = q
⊢ ((x • γ).rightShift a n' hn').v p q hpq = (x • γ.rightShift a n' hn').v p q hpq
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[deprecated not_odd_iff_even (since := "2024-08-21")]
lemma even_iff_not_odd : Even n ↔ ¬Odd n

Proof state:
n : ℤ
⊢ Even n ↔ ¬Odd n

Tactic:
rw [not_odd_iff, even_iff]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsStrictRestriction.ssubset (h : N <r M) : N.E ⊂ M.E

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
⊢ M = M ↾ R ↾ R

Tactic:
rw [show R = M.E from h', restrict_idem, restrict_ground_eq_self]

Result:
no goals

Proof state:
α : Type u_1
M N : Matroid α
h : N <r M
⊢ N.E ⊂ M.E

Tactic:
obtain ⟨R, -, rfl⟩ := h.1

Result:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
⊢ (M ↾ R).E ⊂ M.E

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
⊢ (M ↾ R).E ⊂ M.E

Tactic:
refine h.isRestriction.subset.ssubset_of_ne (fun h' ↦ h.2 ⟨R, Subset.rfl, ?_⟩)

Result:
case intro.intro
α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
⊢ M = M ↾ R ↾ R
-- Mathlib/Algebra/Lie/InvariantForm.lean
lemma atomistic : ∀ I : LieIdeal K L, sSup {J : LieIdeal K L | IsAtom J ∧ J ≤ I} = I

Proof state:
case hst
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
a✝ :
  ∀ (y : LieIdeal K L),
    (invImage (fun x => finrank K ↥x) instWellFoundedRelationOfSizeOf).1 y I → sSup {J | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h✝ : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ J = ⊥

Tactic:
rw [eq_bot_iff]

Result:
case hst
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
Φ : LinearMap.BilinForm K L
hΦ_nondeg : Φ.Nondegenerate
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
hΦ_refl : Φ.IsRefl
hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I
I : LieIdeal K L
a✝ :
  ∀ (y : LieIdeal K L),
    (invImage (fun x => finrank K ↥x) instWellFoundedRelationOfSizeOf).1 y I → sSup {J | IsAtom J ∧ J ≤ y} = y
hI : ¬I = ⊥
J : LieIdeal K L
h✝ : IsAtom J ∧ J ≤ I
hJ : IsAtom J
hJI : J ≤ I
J' : LieSubmodule K L L := orthogonal Φ hΦ_inv J
this : I ≤ J ⊔ J' ⊓ I
hIJ' : I ≤ J'
⊢ J ≤ ⊥
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma isStableUnderCobaseChange_iff_pushouts_le :
    P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P

Proof state:
case mpr.of_isPushout
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
⊢ ∀ {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'}, IsPushout g f f' g' → P f → P f'

Tactic:
intro _ _ _ _ _ _ _ _ h₁ h₂

Result:
case mpr.of_isPushout
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
f'✝ : B✝ ⟶ B'✝
g'✝ : A'✝ ⟶ B'✝
h₁ : IsPushout g✝ f✝ f'✝ g'✝
h₂ : P f✝
⊢ P f'✝

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderCobaseChange → P.pushouts ≤ P

Tactic:
intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : w✝⁴ ⟶ X✝
w✝ : w✝³ ⟶ Y✝
h₁ : P w✝²
h₂ : IsPushout w✝¹ w✝² f✝ w✝
⊢ P f✝

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pushouts ≤ P → P.IsStableUnderCobaseChange

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
⊢ P.IsStableUnderCobaseChange

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : w✝⁴ ⟶ X✝
w✝ : w✝³ ⟶ Y✝
h₁ : P w✝²
h₂ : IsPushout w✝¹ w✝² f✝ w✝
⊢ P f✝

Tactic:
exact of_isPushout h₂ h₁

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
⊢ P.IsStableUnderCobaseChange

Tactic:
constructor

Result:
case mpr.of_isPushout
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
⊢ ∀ {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'}, IsPushout g f f' g' → P f → P f'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderCobaseChange ↔ P.pushouts ≤ P

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderCobaseChange → P.pushouts ≤ P

case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pushouts ≤ P → P.IsStableUnderCobaseChange

Proof state:
case mpr.of_isPushout
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ A'✝ B✝ B'✝ : C
f✝ : A✝ ⟶ A'✝
g✝ : A✝ ⟶ B✝
f'✝ : B✝ ⟶ B'✝
g'✝ : A'✝ ⟶ B'✝
h₁ : IsPushout g✝ f✝ f'✝ g'✝
h₂ : P f✝
⊢ P f'✝

Tactic:
exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.add_smul_sub_mem (h : StrictConvex 𝕜 s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
    {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : x + t • (y - x) ∈ interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ interior s

Tactic:
apply h.openSegment_subset hx hy hxy

Result:
case a
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ openSegment 𝕜 x y

Proof state:
case a
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ (fun θ => x + θ • (y - x)) '' Ioo 0 1

Tactic:
exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

Result:
no goals

Proof state:
case a
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ openSegment 𝕜 x y

Tactic:
rw [openSegment_eq_image']

Result:
case a
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ (fun θ => x + θ • (y - x)) '' Ioo 0 1
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
lemma prod_int_mod (l : List ℤ) (n : ℤ) : l.prod % n = (l.map (· % n)).prod % n

Proof state:
l : List ℤ
n : ℤ
⊢ l.prod % n = (map (fun x => x % n) l).prod % n

Tactic:
induction l <;> simp [Int.mul_emod, *]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem disjoint_ball_ball_iff (hδ : 0 < δ) (hε : 0 < ε) :
    Disjoint (ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
⊢ Disjoint (ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Tactic:
refine ⟨fun h => le_of_not_lt fun hxy => ?_, ball_disjoint_ball⟩

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < δ + ε
⊢ False

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < δ + ε
⊢ False

Tactic:
rw [add_comm] at hxy

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
⊢ False

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y < ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_lt hδ hε hxy

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y < ε
⊢ False

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y < ε
⊢ False

Tactic:
rw [dist_comm] at hxz

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y < ε
⊢ False
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem coe_sumCoords_of_fintype [Fintype ι] : (b.sumCoords : M → R) = ∑ i, b.coord i

Proof state:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
m : M
⊢ b.sumCoords m = (∑ i : ι, b.coord i) m

Tactic:
simp only [sumCoords, Finsupp.sum_fintype, LinearMap.id_coe, LinearEquiv.coe_coe, coord_apply,
  id, Fintype.sum_apply, imp_true_iff, Finsupp.coe_lsum, LinearMap.coe_comp, comp_apply,
  LinearMap.coeFn_sum]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
⊢ ⇑b.sumCoords = ⇑(∑ i : ι, b.coord i)

Tactic:
ext m

Result:
case h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
m : M
⊢ b.sumCoords m = (∑ i : ι, b.coord i) m
-- Mathlib/NumberTheory/Bertrand.lean
theorem exists_prime_lt_and_le_two_mul (n : ℕ) (hn0 : n ≠ 0) :
    ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

Proof state:
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ 511 < 521

Tactic:
norm_num1

Result:
no goals

Proof state:
case inr
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
revert h

Result:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Proof state:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exact exists_prime_lt_and_le_two_mul_eventually n h

Result:
no goals

Proof state:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
run_tac do
  for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
    let i : Term := quote i
    evalTactic <| ←
      `(tactic| refine exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) ?_)

Result:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 2 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Proof state:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 2 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩

Result:
no goals

Proof state:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
open Lean Elab Tactic in
run_tac do
  for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
    let i : Term := quote i
    evalTactic <| ←
      `(tactic| refine exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) ?_)
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩

Result:
no goals

Proof state:
case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
replace h : n < 521 := h.trans_lt (by norm_num1)

Result:
case inr
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Proof state:
n : ℕ
hn0 : n ≠ 0
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
rcases lt_or_le 511 n with h | h

Result:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem card_cliqueFinset_le : #(G.cliqueFinset n) ≤ (card α).choose n

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ (Fintype.card α).choose n

Tactic:
rw [← card_univ, ← card_powersetCard]

Result:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ #(powersetCard n univ)

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
s : Finset α
⊢ s ∈ G.cliqueFinset n → s ∈ powersetCard n univ

Tactic:
simpa [mem_powersetCard_univ] using IsNClique.card_eq

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
⊢ #(G.cliqueFinset n) ≤ #(powersetCard n univ)

Tactic:
refine card_mono fun s => ?_

Result:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
s : Finset α
⊢ s ∈ G.cliqueFinset n → s ∈ powersetCard n univ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_eq_cons_iff {l} {b} {bs} :
    filterMap f l = b :: bs ↔
      ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ x, x ∈ l₁ → f x = none) ∧ f a = some b ∧
        filterMap f l₂ = bs

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
l : List α✝¹
b : α✝
bs : List α✝
⊢ filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  cases h : f a with
  | none =>
    simp only [filterMap_cons_none h]
    intro w
    specialize ih w
    obtain ⟨l₁, a', l₂, rfl, w₁, w₂, w₃⟩ := ih
    exact ⟨a :: l₁, a', l₂, by simp_all⟩
  | some b =>
    simp only [filterMap_cons_some h, cons.injEq, and_imp]
    rintro rfl rfl
    refine ⟨[], a, l, by simp [h]⟩

Result:
no goals

Proof state:
case mp.cons.none
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
h : f a = none
w : filterMap f l = b :: bs
⊢ ∃ l₁ a_1 l₂, a :: l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂ = bs

Tactic:
specialize ih w

Result:
case mp.cons.none
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
h : f a = none
w : filterMap f l = b :: bs
ih : ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
⊢ ∃ l₁ a_1 l₂, a :: l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂ = bs

Proof state:
case mp.cons.none
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
h : f a = none
⊢ filterMap f l = b :: bs →
    ∃ l₁ a_2 l₂, a :: l = l₁ ++ a_2 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_2 = some b ∧ filterMap f l₂ = bs

Tactic:
intro w

Result:
case mp.cons.none
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
b : α✝
bs : List α✝
a : α✝¹
l : List α✝¹
ih :
  filterMap f l = b :: bs →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs
h : f a = none
w : filterMap f l = b :: bs
⊢ ∃ l₁ a_1 l₂, a :: l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂ = bs

Proof state:
case mp.cons.some
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
l : List α✝¹
b : α✝
h : f a = some b
ih :
  filterMap f l = b :: filterMap f l →
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = filterMap f l
⊢ ∃ l₁ a_1 l₂,
    a :: l = l₁ ++ a_1 :: l₂ ∧ (∀ (x : α✝¹), x ∈ l₁ → f x = none) ∧ f a_1 = some b ∧ filterMap f l₂ = filterMap f l

Tactic:
refine ⟨[], a, l, by simp [h]⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma zeroLocus_inter_subset_support (I : IdealSheafData X) (U : X.affineOpens) :
    X.zeroLocus (U := U.1) (I.ideal U) ∩ U ⊆ I.support

Proof state:
case intro.intro.intro.intro.intro.intro.mk.mk.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'

Tactic:
cases n <;>
  simpa [RingHom.algebraMap_toAlgebra, ← hfg, hxf, hxs, Scheme.basicOpen_pow] using hs'

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊓ ↑↑V ≤ X.zeroLocus ↑(I.ideal V)

Tactic:
rintro x ⟨⟨hx, hxU⟩, hxV⟩

Result:
case intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hx : x ∈ X.zeroLocus ↑(I.ideal U)
hxU : x ∈ ↑↑U
⊢ x ∈ X.zeroLocus ↑(I.ideal V)

Proof state:
case intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
⊢ False

Tactic:
obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, hxV⟩

Result:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
⊢ False