harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.add_smul_sub_mem (hs : StarConvex 𝕜 x s) (hy : y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
    (ht₁ : t ≤ 1) : x + t • (y - x) ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ s

Tactic:
apply hs.segment_subset hy

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ [x-[𝕜]y]

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ [x-[𝕜]y]

Tactic:
rw [segment_eq_image']

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ (fun θ => x + θ • (y - x)) '' Icc 0 1

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ (fun θ => x + θ • (y - x)) '' Icc 0 1

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

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Tendsto.lean
theorem tendsto_atTop_atTop_of_monotone' [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u)
    (H : ¬BddAbove (range u)) : Tendsto u atTop atTop

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
⊢ ∃ a, b ≤ u a

Tactic:
rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩

Result:
case intro.intro.intro
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
N : ι
hN : b < u N
⊢ ∃ a, b ≤ u a

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ ∀ (b : α), ∃ a, b ≤ u a

Tactic:
intro b

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
⊢ ∃ a, b ≤ u a

Proof state:
case intro.intro.intro
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
N : ι
hN : b < u N
⊢ ∃ a, b ≤ u a

Tactic:
exact ⟨N, le_of_lt hN⟩

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ Tendsto u atTop atTop

Tactic:
apply h.tendsto_atTop_atTop

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ ∀ (b : α), ∃ a, b ≤ u a
-- Mathlib/NumberTheory/Dioph.lean
theorem ext (d : Dioph S) (H : ∀ v, v ∈ S ↔ v ∈ S') : Dioph S'

Proof state:
α : Type u
S S' : Set (α → ℕ)
d : Dioph S
H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'
⊢ Dioph S'

Tactic:
rwa [← Set.ext H]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zero [Nontrivial M₀] : IsPrimitiveRoot (0 : M₀) 0 :=
  ⟨pow_zero 0, fun l hl ↦ by simpa [zero_pow_eq] using hl⟩

Proof state:
M₀ : Type u_7
inst✝¹ : CommMonoidWithZero M₀
inst✝ : Nontrivial M₀
l : ℕ
hl : 0 ^ l = 1
⊢ 0 ∣ l

Tactic:
simpa [zero_pow_eq] using hl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Equation.map {P : Fin 3 → R} (h : W'.Equation P) :
    (W'.map f).toProjective.Equation (f ∘ P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ f ((eval P) W'.polynomial) = f 0

Tactic:
exact congr_arg f h

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (WeierstrassCurve.map W' f).toProjective.Equation (⇑f ∘ P)

Tactic:
rw [Equation, map_polynomial, eval_map, ← eval₂_comp, ← map_zero f]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ f ((eval P) W'.polynomial) = f 0
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem isGLB_Ioc_of_isGLB_Ioi {i j k : ι} (hij_lt : i < j) (h : IsGLB (Set.Ioi i) k) :
    IsGLB (Set.Ioc i j) k

Proof state:
case inr
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y

Tactic:
exact le_trans (hx j ⟨hij_lt, le_rfl⟩) h_lt.le

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
⊢ x ≤ y

Tactic:
rcases le_or_lt y j with h_le | h_lt

Result:
case inl
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_le : y ≤ j
⊢ x ≤ y

case inr
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_lt : j < y
⊢ x ≤ y

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
⊢ (∀ x ∈ Set.Ioc i j, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioc i j, x ≤ x_1) → x ≤ k

Tactic:
refine ⟨fun x hx ↦ h.1 x hx.1, fun x hx ↦ h.2 x ?_⟩

Result:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
⊢ ∀ x_1 ∈ Set.Ioi i, x ≤ x_1

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k

Tactic:
simp_rw [IsGLB, IsGreatest, mem_upperBounds, mem_lowerBounds] at h ⊢

Result:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
⊢ (∀ x ∈ Set.Ioc i j, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioc i j, x ≤ x_1) → x ≤ k

Proof state:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
⊢ ∀ x_1 ∈ Set.Ioi i, x ≤ x_1

Tactic:
intro y hy

Result:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
⊢ x ≤ y

Proof state:
case inl
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : (∀ x ∈ Set.Ioi i, k ≤ x) ∧ ∀ (x : ι), (∀ x_1 ∈ Set.Ioi i, x ≤ x_1) → x ≤ k
x : ι
hx : ∀ x_1 ∈ Set.Ioc i j, x ≤ x_1
y : ι
hy : y ∈ Set.Ioi i
h_le : y ≤ j
⊢ x ≤ y

Tactic:
exact hx y ⟨hy, h_le⟩

Result:
no goals
-- Mathlib/NumberTheory/AbelSummation.lean
theorem summable_mul_of_bigO_atTop
    (hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t)
    (hf_int : LocallyIntegrableOn (deriv (fun t ↦ ‖f t‖)) (Set.Ici 0))
    (h_bdd : (fun n : ℕ ↦ ‖f n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun _ ↦ (1 : ℝ))
    {g : ℝ → ℝ} (hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g)
    (hg₂ : IntegrableAtFilter g atTop) :
    Summable (fun n : ℕ ↦ f n * c n)

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 0) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
⊢ LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici ↑0) volume

Tactic:
rwa [Nat.cast_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 0) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
⊢ Summable fun n => f ↑n * c n

Tactic:
refine summable_mul_of_bigO_atTop_aux c 0 h_bdd (by rwa [Nat.cast_zero]) (fun n ↦ ?_) hg₁ hg₂

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 0) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
    ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑0 ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ (fun x => ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t => ‖f t‖) (Set.Ici 0) volume
h_bdd : (fun n => ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x => 1
g : ℝ → ℝ
hg₁ : (fun t => deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
    ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑0 ↑n, deriv (fun t => ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖

Tactic:
exact_mod_cast sum_mul_eq_sub_integral_mul' _ _ (fun _ ht ↦ hf_diff _ ht.1)
  (hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc)

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem span_mFourier_closure_eq_top :
    (span ℂ (range <| mFourier (d := d))).topologicalClosure = ⊤

Proof state:
d : Type u_1
inst✝ : Fintype d
⊢ (span ℂ (range mFourier)).topologicalClosure = ⊤

Tactic:
rw [← mFourierSubalgebra_coe]

Result:
d : Type u_1
inst✝ : Fintype d
⊢ (Subalgebra.toSubmodule (mFourierSubalgebra d).toSubalgebra).topologicalClosure = ⊤
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isLittleO_deriv_smoothingFn : deriv ε =o[atTop] fun x => x⁻¹ := calc
  deriv ε =ᶠ[atTop] fun x => -x⁻¹ / (log x ^ 2)

Proof state:
⊢ deriv ε =ᶠ[atTop] fun x => -x⁻¹ / log x ^ 2

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
x : ℝ
hx : 1 < x
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Proof state:
⊢ (fun x => x) =O[atTop] fun x => x

Tactic:
aesop (add safe isBigO_refl)

Result:
no goals

Proof state:
⊢ (fun x => (x * 1)⁻¹) = fun x => x⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h
x : ℝ
hx : 1 < x
⊢ deriv ε x = -x⁻¹ / log x ^ 2

Tactic:
rw [deriv_smoothingFn hx]

Result:
no goals

Proof state:
case refine_1

⊢ (fun x => 1) =o[atTop] fun x => log x ^ 2

Tactic:
rw [isLittleO_one_left_iff]

Result:
case refine_1

⊢ Tendsto (fun x => ‖log x ^ 2‖) atTop atTop

Proof state:
case refine_2

⊢ ∀ᶠ (x : ℝ) in atTop, x * 1 = 0 → -x * log x ^ 2 = 0

Tactic:
exact Filter.Eventually.of_forall (fun x hx => by rw [mul_one] at hx; simp [hx])

Result:
no goals

Proof state:
⊢ (fun x => (-x * log x ^ 2)⁻¹) =o[atTop] fun x => (x * 1)⁻¹

Tactic:
refine IsLittleO.inv_rev ?_ ?_

Result:
case refine_1

⊢ (fun x => x * 1) =o[atTop] fun x => -x * log x ^ 2

case refine_2

⊢ ∀ᶠ (x : ℝ) in atTop, x * 1 = 0 → -x * log x ^ 2 = 0

Proof state:
⊢ (fun x => -x⁻¹ / log x ^ 2) = fun x => (-x * log x ^ 2)⁻¹

Tactic:
simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]

Result:
no goals

Proof state:
case refine_1

⊢ (fun x => x * 1) =o[atTop] fun x => -x * log x ^ 2

Tactic:
refine IsBigO.mul_isLittleO
  (by rw [isBigO_neg_right]; aesop (add safe isBigO_refl)) ?_

Result:
case refine_1

⊢ (fun x => 1) =o[atTop] fun x => log x ^ 2

Proof state:
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_1

⊢ Tendsto (fun x => ‖log x ^ 2‖) atTop atTop

Tactic:
exact Tendsto.comp tendsto_norm_atTop_atTop
  <| Tendsto.comp (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop

Result:
no goals

Proof state:
x : ℝ
hx : x = 0
⊢ -x * log x ^ 2 = 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
⊢ (fun x => x) =O[atTop] Neg.neg

Tactic:
rw [isBigO_neg_right]

Result:
⊢ (fun x => x) =O[atTop] fun x => x

Proof state:
x : ℝ
hx : x * 1 = 0
⊢ -x * log x ^ 2 = 0

Tactic:
rw [mul_one] at hx

Result:
x : ℝ
hx : x = 0
⊢ -x * log x ^ 2 = 0
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
  | 0 => by simp
  | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs

Proof state:
α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
⊢ (s ^ 0).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty

Tactic:
rw [pow_succ]

Result:
α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Proof state:
α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Tactic:
exact hs.pow.mul hs

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sq : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
  ofReal_injective <| by simp [cos_sq]

Proof state:
x : ℝ
⊢ ↑(cos x ^ 2) = ↑(1 / 2 + cos (2 * x) / 2)

Tactic:
simp [cos_sq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_append_iff {f : α → β} :
    map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
case mk.mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
l : Array α
L₁ L₂ : Array β
h : l.size = L₁.size + L₂.size
⊢ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ Array.map f l₁ = L₁ ∧ Array.map f l₂ = L₂) →
    ∃ l₁ l₂, l = l₁.toArray ++ l₂.toArray ∧ Array.map f l₁.toArray = L₁ ∧ Array.map f l₂.toArray = L₂

Tactic:
rintro ⟨l₁, l₂, rfl, rfl, rfl⟩

Result:
case mk.mk.mk.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
h : (l₁ ++ l₂).size = (Array.map f l₁).size + (Array.map f l₂).size
⊢ ∃ l₁_1 l₂_1,
    l₁ ++ l₂ = l₁_1.toArray ++ l₂_1.toArray ∧
      Array.map f l₁_1.toArray = Array.map f l₁ ∧ Array.map f l₂_1.toArray = Array.map f l₂
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem eventually_eq_zero_or_eventually_ne_zero (hf : AnalyticAt 𝕜 f z₀) :
    (∀ᶠ z in 𝓝 z₀, f z = 0) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ HasFPowerSeriesAt f 0 z₀

Tactic:
rwa [h] at hp

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
by_cases h : p = 0

Result:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : ¬p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Proof state:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : ¬p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
exact Or.inr (hp.locally_ne_zero h)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
rcases hf with ⟨p, hp⟩

Result:
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Proof state:
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp))

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem linearIndependent : LinearIndependent R b :=
  fun x y hxy => by
    rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : ι →₀ R
hxy : (linearCombination R ⇑b) x = (linearCombination R ⇑b) y
⊢ x = y

Tactic:
rw [← b.repr_linearCombination x, hxy, b.repr_linearCombination y]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ)
    (l : Array α) (init : γ) (w : stop = (l.filterMap f).size) :
    (l.filterMap f).foldlM g init 0 stop =
      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
l : Array α
init : γ
⊢ foldlM g init (filterMap f l) =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
toList✝ : List α
⊢ foldlM g init (filterMap f { toList := toList✝ }) =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init { toList := toList✝ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
toList✝ : List α
⊢ List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init toList✝ =
    List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init toList✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
stop : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
l : Array α
init : γ
w : stop = (filterMap f l).size
⊢ foldlM g init (filterMap f l) 0 stop =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
l : Array α
init : γ
⊢ foldlM g init (filterMap f l) =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init l

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
toList✝ : List α
⊢ foldlM g init (filterMap f { toList := toList✝ }) =
    foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init { toList := toList✝ }

Tactic:
simp [List.foldlM_filterMap]

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → Option β
g : γ → β → m γ
init : γ
toList✝ : List α
⊢ List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init toList✝ =
    List.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init toList✝
-- Mathlib/Algebra/Polynomial/Degree/Units.lean
lemma natDegree_eq_zero_of_isUnit (h : IsUnit p) : natDegree p = 0

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p.natDegree = 0

Tactic:
exact this.1

Result:
no goals

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p.natDegree = 0

Tactic:
rw [hq, natDegree_one, eq_comm, add_eq_zero] at this

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p.natDegree = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
⊢ p.natDegree = 0

Tactic:
nontriviality R

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
⊢ p.natDegree = 0

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
⊢ p.natDegree = 0

Tactic:
have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
this : (p * q).natDegree = p.natDegree + q.natDegree
⊢ p.natDegree = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
⊢ p.natDegree = 0

Tactic:
obtain ⟨q, hq⟩ := h.exists_right_inv

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
⊢ p.natDegree = 0
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem EMetric.diam_closure (s : Set α) : diam (closure s) = diam s

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
⊢ edist x y ≤ diam s

Tactic:
have : edist x y ∈ closure (Iic (diam s)) :=
  map_mem_closure₂ continuous_edist hx hy fun x hx y hy => edist_le_diam_of_mem hx hy

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
this : edist x y ∈ closure (Iic (diam s))
⊢ edist x y ≤ diam s

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ diam (closure s) = diam s

Tactic:
refine le_antisymm (diam_le fun x hx y hy => ?_) (diam_mono subset_closure)

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
⊢ edist x y ≤ diam s

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
y : α
hy : y ∈ closure s
this : edist x y ∈ closure (Iic (diam s))
⊢ edist x y ≤ diam s

Tactic:
rwa [closure_Iic] at this

Result:
no goals