harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem IsSepClosed.separableClosure_eq_bot_iff [IsSepClosed E] :
    separableClosure F E = ⊥ ↔ IsSepClosed F

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
⊢ ∃ x, eval x p = 0

Tactic:
obtain ⟨x, hx⟩ := IsSepClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne' hsep

Result:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : E
hx : (aeval x) p = 0
⊢ ∃ x, eval x p = 0

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
⊢ separableClosure F E = ⊥ ↔ IsSepClosed F

Tactic:
refine ⟨fun h ↦ IsSepClosed.of_exists_root _ fun p _ hirr hsep ↦ ?_,
  fun _ ↦ IntermediateField.eq_bot_of_isSepClosed_of_isSeparable _⟩

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
⊢ ∃ x, eval x p = 0

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ eval x p = 0

Tactic:
simpa [Algebra.ofId_apply] using hx

Result:
no goals

Proof state:
case intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : E
hx : (aeval x) p = 0
⊢ ∃ x, eval x p = 0

Tactic:
obtain ⟨x, rfl⟩ := h ▸ mem_separableClosure_iff.2 (hsep.of_dvd <| minpoly.dvd _ x hx)

Result:
case intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ ∃ x, eval x p = 0

Proof state:
case intro.intro
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsSepClosed E
h : separableClosure F E = ⊥
p : F[X]
x✝ : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : F
hx : (aeval ((Algebra.ofId F E).toRingHom x)) p = 0
⊢ ∃ x, eval x p = 0

Tactic:
exact ⟨x, by simpa [Algebra.ofId_apply] using hx⟩

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
lemma prod_map_add {s : Multiset ι} {f g : ι → α} :
    prod (s.map fun i ↦ f i + g i) =
      sum ((antidiagonal s).map fun p ↦ (p.1.map f).prod * (p.2.map g).prod)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : CommSemiring α
s : Multiset ι
f g : ι → α
⊢ (map (fun i => f i + g i) s).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum

Tactic:
refine s.induction_on ?_ fun a s ih ↦ ?_

Result:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommSemiring α
s : Multiset ι
f g : ι → α
⊢ (map (fun i => f i + g i) 0).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)).sum

case refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommSemiring α
s✝ : Multiset ι
f g : ι → α
a : ι
s : Multiset ι
ih : (map (fun i => f i + g i) s).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i => f i + g i) (a ::ₘ s)).prod =
    (map (fun p => (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal).sum

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommSemiring α
s✝ : Multiset ι
f g : ι → α
a : ι
s : Multiset ι
ih : (map (fun i => f i + g i) s).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i => f i + g i) (a ::ₘ s)).prod =
    (map (fun p => (map f p.1).prod * (map g p.2).prod) (a ::ₘ s).antidiagonal).sum

Tactic:
simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a),
  mul_left_comm (g a), sum_map_add, antidiagonal_cons, Prod.map_fst, Prod.map_snd,
  id_eq, map_add, map_map, Function.comp_apply, mul_assoc, sum_add]

Result:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommSemiring α
s✝ : Multiset ι
f g : ι → α
a : ι
s : Multiset ι
ih : (map (fun i => f i + g i) s).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i => (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum +
      (map (fun i => (map f i.1).prod * (g a * (map g i.2).prod)) s.antidiagonal).sum =
    (map (fun x => (map f x.1).prod * (g a * (map g x.2).prod)) s.antidiagonal).sum +
      (map (fun i => (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
inst✝ : CommSemiring α
s : Multiset ι
f g : ι → α
⊢ (map (fun i => f i + g i) 0).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) (antidiagonal 0)).sum

Tactic:
simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : CommSemiring α
s✝ : Multiset ι
f g : ι → α
a : ι
s : Multiset ι
ih : (map (fun i => f i + g i) s).prod = (map (fun p => (map f p.1).prod * (map g p.2).prod) s.antidiagonal).sum
⊢ (map (fun i => (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum +
      (map (fun i => (map f i.1).prod * (g a * (map g i.2).prod)) s.antidiagonal).sum =
    (map (fun x => (map f x.1).prod * (g a * (map g x.2).prod)) s.antidiagonal).sum +
      (map (fun i => (map f i.1).prod * (f a * (map g i.2).prod)) s.antidiagonal).sum

Tactic:
exact add_comm _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_id (n) (l : List α) : l.modify id n = l

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ modify id n l = l

Tactic:
simp [modify]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
/-- The semilatice generated by a finite set is finite. -/
protected lemma Set.Finite.supClosure (hs : s.Finite) : (supClosure s).Finite

Proof state:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ t.sup' ht id ∈ ↑(Finset.image (fun t => (↑t).sup' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)

Tactic:
simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
  Finset.mem_powerset, Finset.not_nonempty_iff_eq_empty, mem_filter]

Result:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ ∃ a, ∃ (h : a ⊆ s ∧ a.Nonempty), (a.sup' ⋯ fun x => x) = t.sup' ⋯ fun x => x

Proof state:
case intro
α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ (supClosure ↑s).Finite

Tactic:
classical
refine ({t ∈ s.powerset | t.Nonempty}.attach.image
  fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
rintro _ ⟨t, ht, hts, rfl⟩
simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
  Finset.mem_powerset, Finset.not_nonempty_iff_eq_empty, mem_filter]
exact ⟨t, ⟨hts, ht⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
hs : s.Finite
⊢ (supClosure s).Finite

Tactic:
lift s to Finset α using hs

Result:
case intro
α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ (supClosure ↑s).Finite

Proof state:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ ∃ a, ∃ (h : a ⊆ s ∧ a.Nonempty), (a.sup' ⋯ fun x => x) = t.sup' ⋯ fun x => x

Tactic:
exact ⟨t, ⟨hts, ht⟩, rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ (supClosure ↑s).Finite

Tactic:
refine ({t ∈ s.powerset | t.Nonempty}.attach.image
  fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_

Result:
case intro
α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ supClosure ↑s ⊆ ↑(Finset.image (fun t => (↑t).sup' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)

Proof state:
case intro
α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ supClosure ↑s ⊆ ↑(Finset.image (fun t => (↑t).sup' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)

Tactic:
rintro _ ⟨t, ht, hts, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeSup α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ t.sup' ht id ∈ ↑(Finset.image (fun t => (↑t).sup' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)
-- Mathlib/Topology/LocalAtTarget.lean
theorem isOpen_iff_inter :
    IsOpen s ↔ ∀ i, IsOpen (s ∩ U i)

Proof state:
case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ IsOpen s

Tactic:
simpa [← inter_iUnion, hU.iSup_set_eq_univ] using isOpen_iUnion H

Result:
no goals

Proof state:
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (s ∩ ↑(U i))

Tactic:
constructor

Result:
case mp
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen s → ∀ (i : ι), IsOpen (s ∩ ↑(U i))

case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) → IsOpen s

Proof state:
case mp
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen s → ∀ (i : ι), IsOpen (s ∩ ↑(U i))

Tactic:
exact fun H i ↦ H.inter (U i).isOpen

Result:
no goals

Proof state:
case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ (∀ (i : ι), IsOpen (s ∩ ↑(U i))) → IsOpen s

Tactic:
intro H

Result:
case mpr
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
H : ∀ (i : ι), IsOpen (s ∩ ↑(U i))
⊢ IsOpen s
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) card_mul_addConst]
lemma card_mul_mulConst (A B : Finset G) : #A * σₘ[A, B] = #(A * B)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ ↑(#A) * σₘ[A, B] = ↑(#(A * B))

Tactic:
rw [mul_comm, mulConst_mul_card]

Result:
no goals
-- Mathlib/Algebra/Lie/DirectSum.lean
theorem lie_of_of_ne [DecidableEq ι] {i j : ι} (hij : i ≠ j) (x : L i) (y : L j) :
    ⁅of L i x, of L j y⁆ = 0

Proof state:
case w
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k

Tactic:
obtain rfl | hik := Decidable.eq_or_ne i k

Result:
case w.inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
⊢ ⁅((of L i) x) i, ((of L j) y) i⁆ = 0 i

case w.inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : i ≠ k
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k

Proof state:
case w.inl
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
⊢ ⁅((of L i) x) i, ((of L j) y) i⁆ = 0 i

Tactic:
rw [of_eq_of_ne _ _ _ hij.symm, lie_zero, zero_apply]

Result:
no goals

Proof state:
case w.inr
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
hik : i ≠ k
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k

Tactic:
rw [of_eq_of_ne _ _ _ hik, zero_lie, zero_apply]

Result:
no goals

Proof state:
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
⊢ ⁅(of L i) x, (of L j) y⁆ = 0

Tactic:
ext k

Result:
case w
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅(of L i) x, (of L j) y⁆ k = 0 k

Proof state:
case w
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅(of L i) x, (of L j) y⁆ k = 0 k

Tactic:
rw [bracket_apply]

Result:
case w
ι : Type v
L : ι → Type w
inst✝¹ : (i : ι) → LieRing (L i)
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
x : L i
y : L j
k : ι
⊢ ⁅((of L i) x) k, ((of L j) y) k⁆ = 0 k
-- Mathlib/Order/Filter/Ring.lean
theorem EventuallyLE.mul_nonneg [OrderedSemiring β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f)
    (hg : 0 ≤ᶠ[l] g) : 0 ≤ᶠ[l] f * g

Proof state:
α : Type u
β : Type v
inst✝ : OrderedSemiring β
l : Filter α
f g : α → β
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
⊢ 0 ≤ᶠ[l] f * g

Tactic:
filter_upwards [hf, hg] with x using _root_.mul_nonneg

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
private lemma F_differentiableAt_of_ne (B : BadChar N) {s : ℂ} (hs : s ≠ 1) :
    DifferentiableAt ℂ B.F s

Proof state:
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
apply DifferentiableAt.congr_of_eventuallyEq

Result:
case h
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ ?f s

case hL
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ B.F =ᶠ[𝓝 s] ?f

case f
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ ℂ → ℂ

Proof state:
case h
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ ?f s

Tactic:
exact (differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)

Result:
no goals

Proof state:
case hL
N : ℕ
inst✝ : NeZero N
B : DirichletCharacter.BadChar N
s : ℂ
hs : s ≠ 1
⊢ B.F =ᶠ[𝓝 s] fun y => riemannZeta y * LFunction B.χ y

Tactic:
filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_of_ne ht ..

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma isIso_iff_yoneda_map_bijective {X Y : C} (f : X ⟶ Y) :
    IsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f))

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (yoneda.map f)
T : C
⊢ Function.Bijective fun x => x ≫ f

Tactic:
rw [← isIso_iff_bijective]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (yoneda.map f)
T : C
⊢ IsIso fun x => x ≫ f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (yoneda.map f)
⊢ ∀ (T : C), Function.Bijective fun x => x ≫ f

Tactic:
intro T

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (yoneda.map f)
T : C
⊢ Function.Bijective fun x => x ≫ f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x => x ≫ f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_yoneda_map_bijective f hf⟩

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ ∀ (T : C), Function.Bijective fun x => x ≫ f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (yoneda.map f)
T : C
⊢ IsIso fun x => x ≫ f

Tactic:
exact inferInstanceAs (IsIso ((yoneda.map f).app _))

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ ∀ (T : C), Function.Bijective fun x => x ≫ f

Tactic:
have : IsIso (yoneda.map f) := inferInstance

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (yoneda.map f)
⊢ ∀ (T : C), Function.Bijective fun x => x ≫ f
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem y_eq_zero_of_not_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (hx : x ∉ ball (0 : E) (1 + D)) :
    y D x = 0

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0

Tactic:
have B' : ∀ y, y ∈ ball x D → φ y = φ x := by rw [Bx]; exact B

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
B : ∀ y ∈ ball x D, φ y = 0
Bx : φ x = 0
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 0

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ ball y D ⊆ ball 0 (1 + D)

Tactic:
apply ball_subset_ball'

Result:
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ D + dist y 0 ≤ 1 + D
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem interior_reProdIm (s t : Set ℝ) : interior (s ×ℂ t) = interior s ×ℂ interior t

Proof state:
s t : Set ℝ
⊢ interior (s ×ℂ t) = interior s ×ℂ interior t

Tactic:
rw [reProdIm, reProdIm, interior_inter, interior_preimage_re, interior_preimage_im]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_nat_mod (s : Multiset ℕ) (n : ℕ) : s.prod % n = (s.map (· % n)).prod % n

Proof state:
s : Multiset ℕ
n : ℕ
⊢ s.prod % n = (map (fun x => x % n) s).prod % n

Tactic:
induction s using Multiset.induction <;> simp [Nat.mul_mod, *]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_maximal_coprime {w : HeightOneSpectrum R} (hw : w ≠ v) :
    count K v (w.asIdeal : FractionalIdeal R⁰ K) = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
⊢ count K v ↑w.asIdeal = 0

Tactic:
have hw_ne_zero : (w.asIdeal : FractionalIdeal R⁰ K) ≠ 0 :=
  coeIdeal_ne_zero.mpr w.ne_bot

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
⊢ count K v ↑w.asIdeal = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
⊢ count K v ↑w.asIdeal = 0

Tactic:
have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v ↑w.asIdeal = 0
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.tower_top_of_subalgebra_le
    {A B : Subalgebra R S} (hle : A ≤ B) {x : S}
    (h : IsAlgebraic A x) : IsAlgebraic B x

Proof state:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
⊢ IsAlgebraic (↥B) x

Tactic:
haveI : IsScalarTower A B S := .of_algebraMap_eq fun _ ↦ rfl

Result:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this✝ : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
this : IsScalarTower (↥A) (↥B) S
⊢ IsAlgebraic (↥B) x

Proof state:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this✝ : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
this : IsScalarTower (↥A) (↥B) S
⊢ IsAlgebraic (↥B) x

Tactic:
exact h.extendScalars (Subalgebra.inclusion_injective hle)

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
⊢ IsAlgebraic (↥B) x

Tactic:
letI : Algebra A B := (Subalgebra.inclusion hle).toAlgebra

Result:
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
A B : Subalgebra R S
hle : A ≤ B
x : S
h : IsAlgebraic (↥A) x
this : Algebra ↥A ↥B := (Subalgebra.inclusion hle).toAlgebra
⊢ IsAlgebraic (↥B) x
-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem congr_hom {X Y : PresheafedSpace.{_, _, v} C} (α β : X ⟶ Y) (h : α = β) (x : X) :
    α.stalkMap x =
      eqToHom (show Y.presheaf.stalk (α.base x) =
        Y.presheaf.stalk (β.base x) by rw [h]) ≫ β.stalkMap x

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Hom.stalkMap α x = eqToHom ⋯ ≫ Hom.stalkMap β x

Tactic:
rw [← stalkMap.congr α β h x x rfl, eqToHom_refl, Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Y.presheaf.stalk ((ConcreteCategory.hom α.base) x) = Y.presheaf.stalk ((ConcreteCategory.hom β.base) x)

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Order/Filter/CardinalInter.lean
theorem eventually_cardinal_ball {S : Set ι} (hS : #S < c)
    {p : α → ∀ i ∈ S, Prop} :
    (∀ᶠ x in l, ∀ i hi, p x i hi) ↔ ∀ i hi, ∀ᶠ x in l, p x i hi

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
p : α → (i : ι) → i ∈ S → Prop
⊢ ⋂ i, ⋂ (i_1 : i ∈ S), {x | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x | p x i hi} ∈ l

Tactic:
exact cardinal_bInter_mem hS

Result:
no goals

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
p : α → (i : ι) → i ∈ S → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi

Tactic:
simp only [Filter.Eventually, setOf_forall]

Result:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
p : α → (i : ι) → i ∈ S → Prop
⊢ ⋂ i, ⋂ (i_1 : i ∈ S), {x | p x i i_1} ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), {x | p x i hi} ∈ l