harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/RingedSpace/Basic.lean
@[simp]
lemma basicOpen_pow {U : Opens X} (f : X.presheaf.obj (op U)) (n : ℕ) (h : 0 < n) :
    X.basicOpen (f ^ n) = X.basicOpen f

Proof state:
case intro.zero
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : 0 < 0 + Nat.succ 0
⊢ X.basicOpen (f ^ (0 + Nat.succ 0)) = X.basicOpen f

Tactic:
simp

Result:
no goals

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
h : 0 < n
⊢ X.basicOpen (f ^ n) = X.basicOpen f

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h

Result:
case intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
k : ℕ
h : 0 < k + Nat.succ 0
⊢ X.basicOpen (f ^ (k + Nat.succ 0)) = X.basicOpen f

Proof state:
case intro.succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1 + Nat.succ 0)) = X.basicOpen f

Tactic:
rw [pow_add]

Result:
case intro.succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1) * f ^ Nat.succ 0) = X.basicOpen f

Proof state:
case intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
k : ℕ
h : 0 < k + Nat.succ 0
⊢ X.basicOpen (f ^ (k + Nat.succ 0)) = X.basicOpen f

Tactic:
induction k with
| zero => simp
| succ n hn => rw [pow_add]; simp_all

Result:
no goals

Proof state:
case intro.succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1) * f ^ Nat.succ 0) = X.basicOpen f

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_le_encard_of_injOn (hf : MapsTo f s t) (f_inj : InjOn f s) :
    s.encard ≤ t.encard

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ f '' s ⊆ t

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case h.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
x : α
hx : x ∈ s
⊢ f x ∈ t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ (f '' s).encard ≤ t.encard

Tactic:
apply encard_le_encard

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ f '' s ⊆ t

Proof state:
case h.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
x : α
hx : x ∈ s
⊢ f x ∈ t

Tactic:
exact hf hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ s.encard ≤ t.encard

Tactic:
rw [← f_inj.encard_image]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ (f '' s).encard ≤ t.encard
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem le_tan {x : ℝ} (h1 : 0 ≤ x) (h2 : x < π / 2) : x ≤ tan x

Proof state:
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
⊢ x ≤ tan x

Tactic:
rcases eq_or_lt_of_le h1 with (rfl | h1')

Result:
case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0

case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x

Proof state:
case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x

Tactic:
exact le_of_lt (lt_tan h1' h2)

Result:
no goals

Proof state:
case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0

Tactic:
rw [tan_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toList_pmap {l : Vector α n} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
    (l.pmap f H).toList = l.toList.pmap f (fun a m => H a (by simpa using m))

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
⊢ (pmap f l H).toList = List.pmap f l.toList ⋯

Tactic:
simp [pmap]

Result:
no goals

Proof state:
α : Type ?u.6430
n : Nat
β : Type ?u.6482
l : Vector α n
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
a : α
m : a ∈ l.toList
⊢ a ∈ l

Tactic:
simpa using m

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_biInter_eq_biInter_closure_of_biUnion_indep {ι : Type*} {A : Set ι} (hA : A.Nonempty)
    {I : ι → Set α} (h : M.Indep (⋃ i ∈ A, I i)) :
    M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Proof state:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Tactic:
convert closure_iInter_eq_iInter_closure_of_iUnion_indep (Is := fun i : A ↦ I i) (by simpa) <;>
simp

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Tactic:
have := hA.coe_sort

Result:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Proof state:
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ Indep ?m.169874 (⋃ i, (fun i => I ↑i) i)

Tactic:
simpa

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem isCyclic_of_card_dvd_prime {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card α ∣ p) : IsCyclic α

Proof state:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α ∣ p
⊢ IsCyclic α

Tactic:
rcases (Nat.dvd_prime hp.out).mp h with h | h

Result:
case inl
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h✝ : Nat.card α ∣ p
h : Nat.card α = 1
⊢ IsCyclic α

case inr
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h✝ : Nat.card α ∣ p
h : Nat.card α = p
⊢ IsCyclic α

Proof state:
case inl
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h✝ : Nat.card α ∣ p
h : Nat.card α = 1
⊢ IsCyclic α

Tactic:
exact @isCyclic_of_subsingleton α _ (Nat.card_eq_one_iff_unique.mp h).1

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h✝ : Nat.card α ∣ p
h : Nat.card α = p
⊢ IsCyclic α

Tactic:
exact isCyclic_of_prime_card h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_sum_le (s : Finset ι) (f : ι → R[X]) :
    degree (∑ i ∈ s, f i) ≤ s.sup fun b => degree (f b) :=
  Finset.cons_induction_on s (by simp only [sum_empty, sup_empty, degree_zero, le_refl])
    fun a s has ih =>
    calc
      degree (∑ i ∈ cons a s has, f i) ≤ max (degree (f a)) (degree (∑ i ∈ s, f i))

Proof state:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
⊢ (f a).degree ⊔ (∑ i ∈ s, f i).degree ≤ (Finset.cons a s has).sup fun b => (f b).degree

Tactic:
rw [sup_cons]

Result:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
⊢ (f a).degree ⊔ (∑ i ∈ s, f i).degree ≤ (f a).degree ⊔ s.sup fun b => (f b).degree

Proof state:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s : Finset ι
f : ι → R[X]
⊢ (∑ i ∈ ∅, f i).degree ≤ ∅.sup fun b => (f b).degree

Tactic:
simp only [sum_empty, sup_empty, degree_zero, le_refl]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
⊢ (f a + ∑ x ∈ s, f x).degree ≤ (f a).degree ⊔ (∑ i ∈ s, f i).degree

Tactic:
exact degree_add_le _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
⊢ (f a).degree ⊔ (∑ i ∈ s, f i).degree ≤ (f a).degree ⊔ s.sup fun b => (f b).degree

Tactic:
exact max_le_max le_rfl ih

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
⊢ (∑ i ∈ Finset.cons a s has, f i).degree ≤ (f a).degree ⊔ (∑ i ∈ s, f i).degree

Tactic:
rw [Finset.sum_cons]

Result:
R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b => (f b).degree
⊢ (f a + ∑ x ∈ s, f x).degree ≤ (f a).degree ⊔ (∑ i ∈ s, f i).degree
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem ae_eq_trim_of_measurable {α E} {m m0 : MeasurableSpace α} {μ : Measure α}
    [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E] [MeasurableSub₂ E]
    (hm : m ≤ m0) {f g : α → E} (hf : Measurable[m] f) (hg : Measurable[m] g) (hfg : f =ᵐ[μ] g) :
    f =ᵐ[μ.trim hm] g

Proof state:
α : Type u_5
E : Type u_6
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (μ.trim hm)] g

Tactic:
rwa [Filter.EventuallyEq, ae_iff, trim_measurableSet_eq hm _]

Result:
α : Type u_5
E : Type u_6
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ MeasurableSet {a | ¬f a = g a}

Proof state:
α : Type u_5
E : Type u_6
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
hm : m ≤ m0
f g : α → E
hf : Measurable f
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ MeasurableSet {a | ¬f a = g a}

Tactic:
exact @MeasurableSet.compl α _ m (@measurableSet_eq_fun α m E _ _ _ _ _ _ hf hg)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem mul_dist_le_mul_dist_add_mul_dist (a b c d : P) :
    dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Proof state:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
rw [← div_le_div_iff_of_pos_right (mul_pos hb (mul_pos hc hd))]

Result:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) ≤
    (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))

Proof state:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
rcases eq_or_ne c a with (rfl | hc)

Result:
case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d

case inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Proof state:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H :
  dist (inversion a 1 b) (inversion a 1 d) ≤
    dist (inversion a 1 b) (inversion a 1 c) + dist (inversion a 1 c) (inversion a 1 d)
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d

Tactic:
rw [dist_inversion_inversion hb hd, dist_inversion_inversion hb hc,
  dist_inversion_inversion hc hd, one_pow] at H

Result:
case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : b ≠ a
hc : c ≠ a
hd : d ≠ a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
-- Mathlib/Analysis/Calculus/Deriv/Pow.lean
theorem derivWithin_pow' (hc : DifferentiableWithinAt 𝕜 c s x) :
    derivWithin (fun x => c x ^ n) s x = (n : 𝕜) * c x ^ (n - 1) * derivWithin c s x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
n : ℕ
hc : DifferentiableWithinAt 𝕜 c s x
⊢ derivWithin (fun x => c x ^ n) s x = ↑n * c x ^ (n - 1) * derivWithin c s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
n : ℕ
hc : DifferentiableWithinAt 𝕜 c s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => c x ^ n) s x = ↑n * c x ^ (n - 1) * derivWithin c s x

case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
n : ℕ
hc : DifferentiableWithinAt 𝕜 c s x
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ derivWithin (fun x => c x ^ n) s x = ↑n * c x ^ (n - 1) * derivWithin c s x

Proof state:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
n : ℕ
hc : DifferentiableWithinAt 𝕜 c s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => c x ^ n) s x = ↑n * c x ^ (n - 1) * derivWithin c s x

Tactic:
exact (hc.hasDerivWithinAt.pow n).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
n : ℕ
hc : DifferentiableWithinAt 𝕜 c s x
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ derivWithin (fun x => c x ^ n) s x = ↑n * c x ^ (n - 1) * derivWithin c s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem sequenceOfCofinals.monotone : Monotone (sequenceOfCofinals p 𝒟)

Proof state:
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)

Tactic:
dsimp only [sequenceOfCofinals, Nat.add]

Result:
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Proof state:
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
cases (Encodable.decode n : Option ι)

Result:
case hf.none
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match none with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

case hf.some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Proof state:
case hf.none
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤
    match none with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
rfl

Result:
no goals

Proof state:
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ Monotone (sequenceOfCofinals p 𝒟)

Tactic:
apply monotone_nat_of_le_succ

Result:
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ ∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)

Proof state:
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ ∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)

Tactic:
intro n

Result:
case hf
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)

Proof state:
case hf.some
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val✝ : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match some val✝ with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
apply Cofinal.le_above

Result:
no goals
-- Mathlib/Analysis/Analytic/Within.lean
/-- `f` has power series `p` at `x` iff some local extension of `f` has that series -/
lemma hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt [CompleteSpace F] {f : E → F}
    {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} :
    HasFPowerSeriesWithinAt f p s x ↔
      ∃ g, f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

Proof state:
case mpr.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : y ∈ EMetric.ball x (r ⊓ ENNReal.ofReal e)
⊢ dist y x < e

Tactic:
simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal] at xy

Result:
case mpr.intro.intro.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : edist y x < r ∧ dist y x < e
⊢ dist y x < e
-- Mathlib/Data/Multiset/Count.lean
lemma countP_attach (s : Multiset α) : s.attach.countP (fun a : {a // a ∈ s} ↦ p a) = s.countP p :=
  Quotient.inductionOn s fun l => by
    simp only [quot_mk_to_coe, coe_countP]
    -- Porting note: was
    -- rw [quot_mk_to_coe, coe_attach, coe_countP]
    -- exact List.countP_attach _ _
    rw [coe_attach]
    refine (coe_countP _ _).trans ?_
    convert List.countP_attach _ _
    rfl

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.countP (fun b => decide (p ↑b)) l.attach = List.countP (fun b => decide (p b)) l

Tactic:
convert List.countP_attach _ _

Result:
case h.e'_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.countP (fun b => decide (p ↑b)) l.attach = List.countP (fun a => decide (p ↑a)) l.attach

Proof state:
case h.e'_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.countP (fun b => decide (p ↑b)) l.attach = List.countP (fun a => decide (p ↑a)) l.attach

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun a => p ↑a) ↑l.attach = List.countP (fun b => decide (p b)) l

Tactic:
refine (coe_countP _ _).trans ?_

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.countP (fun b => decide (p ↑b)) l.attach = List.countP (fun b => decide (p b)) l

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun a => p ↑a) (attach ⟦l⟧) = countP p ⟦l⟧

Tactic:
simp only [quot_mk_to_coe, coe_countP]

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun a => p ↑a) (↑l).attach = List.countP (fun b => decide (p b)) l

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun a => p ↑a) (↑l).attach = List.countP (fun b => decide (p b)) l

Tactic:
rw [coe_attach]

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ countP (fun a => p ↑a) ↑l.attach = List.countP (fun b => decide (p b)) l
-- Mathlib/Logic/Nontrivial/Defs.lean
theorem Decidable.exists_ne [Nontrivial α] [DecidableEq α] (x : α) : ∃ y, y ≠ x

Proof state:
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x

Tactic:
rcases exists_pair_ne α with ⟨y, y', h⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x

Proof state:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

Tactic:
rw [← hx] at h

Result:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

Proof state:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

Tactic:
exact ⟨y', h.symm⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x

Tactic:
exact ⟨y, Ne.symm hx⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x

Tactic:
by_cases hx : x = y

Result:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
-- Mathlib/LinearAlgebra/Dimension/Localization.lean
lemma IsLocalizedModule.rank_eq {N : Type v} [AddCommGroup N]
    [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) [IsLocalizedModule p f] :
    Module.rank S N = Module.rank R M

Proof state:
R : Type u
S : Type u'
M : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Algebra R S
p : Submonoid R
inst✝⁵ : IsLocalization p S
hp : p ≤ R⁰
N : Type v
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ Module.rank S N = Module.rank R M

Tactic:
simpa using IsLocalizedModule.lift_rank_eq S p f hp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_map (f : α → β) : ∀ (l : List α) (i : Nat), (map f l)[i]? = Option.map f l[i]?
  | [], _ => rfl
  | _ :: _, 0 => by simp
  | _ :: l, i+1 => by simp [getElem?_map f l i]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
l : List α
i : Nat
⊢ (map f (head✝ :: l))[i + 1]? = Option.map f (head✝ :: l)[i + 1]?

Tactic:
simp [getElem?_map f l i]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
⊢ (map f (head✝ :: tail✝))[0]? = Option.map f (head✝ :: tail✝)[0]?

Tactic:
simp

Result:
no goals