harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Baire/Lemmas.lean
theorem dense_biInter_of_Gδ {S : Set α} {f : ∀ x ∈ S, Set X} (ho : ∀ s (H : s ∈ S), IsGδ (f s H))
    (hS : S.Countable) (hd : ∀ s (H : s ∈ S), Dense (f s H)) : Dense (⋂ s ∈ S, f s ‹_›)

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ x, f ↑x ⋯)

Tactic:
haveI := hS.to_subtype

Result:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
this : Countable ↑S
⊢ Dense (⋂ x, f ↑x ⋯)

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ s, ⋂ (h : s ∈ S), f s h)

Tactic:
rw [biInter_eq_iInter]

Result:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ x, f ↑x ⋯)

Proof state:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
this : Countable ↑S
⊢ Dense (⋂ x, f ↑x ⋯)

Tactic:
exact dense_iInter_of_Gδ (fun s => ho s s.2) fun s => hd s s.2

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem comapDomain_zero (f : α → β)
    (hif : Set.InjOn f (f ⁻¹' ↑(0 : β →₀ M).support) := Finset.coe_empty ▸ (Set.injOn_empty f)) :
    comapDomain f (0 : β →₀ M) hif = (0 : α →₀ M)

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hif : optParam (Set.InjOn f (f ⁻¹' ↑(support 0))) ⋯
a✝ : α
⊢ (comapDomain f 0 hif) a✝ = 0 a✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hif : optParam (Set.InjOn f (f ⁻¹' ↑(support 0))) ⋯
⊢ comapDomain f 0 hif = 0

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
hif : optParam (Set.InjOn f (f ⁻¹' ↑(support 0))) ⋯
a✝ : α
⊢ (comapDomain f 0 hif) a✝ = 0 a✝
-- Mathlib/Algebra/Order/Ring/Cast.lean
@[simp] lemma cast_lt_zero : (n : R) < 0 ↔ n < 0

Proof state:
R : Type u_1
inst✝⁴ : AddCommGroupWithOne R
inst✝³ : PartialOrder R
inst✝² : AddLeftMono R
inst✝¹ : ZeroLEOneClass R
inst✝ : NeZero 1
n : ℤ
⊢ ↑n < 0 ↔ n < 0

Tactic:
rw [← cast_zero, cast_lt]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive (attr := simp)]
lemma map_comp_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F)
    (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (g : ι → G) (n : ℤ) : f ∘ (g ^ n) = f ∘ g ^ n

Proof state:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝

Tactic:
simp [map_zpow' f hf]

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
ext

Result:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝
-- Mathlib/RepresentationTheory/Invariants.lean
theorem averageMap_invariant (v : V) : averageMap ρ v ∈ invariants ρ := fun g => by
  rw [averageMap, ← asAlgebraHom_single_one, ← LinearMap.mul_apply, ← map_mul (asAlgebraHom ρ),
    mul_average_left]

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
g : G
⊢ (ρ g) (ρ.averageMap v) = ρ.averageMap v

Tactic:
rw [averageMap, ← asAlgebraHom_single_one, ← LinearMap.mul_apply, ← map_mul (asAlgebraHom ρ),
  mul_average_left]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toReal_ofReal_eq_iff {a : ℝ} : (ENNReal.ofReal a).toReal = a ↔ 0 ≤ a :=
  ⟨fun h => by
    rw [← h]
    exact toReal_nonneg, toReal_ofReal⟩

Proof state:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ a

Tactic:
rw [← h]

Result:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ (ENNReal.ofReal a).toReal

Proof state:
a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ (ENNReal.ofReal a).toReal

Tactic:
exact toReal_nonneg

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normal_iff_forall_fieldRange_le : Normal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange ≤ K

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
⊢ Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K

Tactic:
rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aeval_root (h : IsAdjoinRoot S f) : aeval h.root f = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
⊢ (aeval h.root) f = 0

Tactic:
rw [aeval_eq, map_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem mul_congr {a b c d : Int} (h₁ : a = b) (h₂ : c = d) : a * c = b * d

Proof state:
a c d : Int
h₂ : c = d
⊢ a * c = a * d

Tactic:
subst h₂

Result:
a c : Int
⊢ a * c = a * c

Proof state:
a b c d : Int
h₁ : a = b
h₂ : c = d
⊢ a * c = b * d

Tactic:
subst h₁

Result:
a c d : Int
h₂ : c = d
⊢ a * c = a * d

Proof state:
a c : Int
⊢ a * c = a * c

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
/-- Extensionality lemma for functors `C ⥤ D` which uses as an assumption
that the induced maps `Arrow C → Arrow D` coincide. -/
lemma Arrow.functor_ext {F G : C ⥤ D} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    F.mapArrow.obj (Arrow.mk f) = G.mapArrow.obj (Arrow.mk f)) :
    F = G :=
  Functor.ext (fun X ↦ congr_arg Comma.left (h (𝟙 X))) (fun X Y f ↦ by
    have := h f
    simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this
    tauto)

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : ∃ hX hY, F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
simp only [Functor.mapArrow_obj, mk_eq_mk_iff] at this

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : ∃ hX hY, F.map (mk f).hom = eqToHom hX ≫ G.map (mk f).hom ≫ eqToHom ⋯
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
have := h f

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F G : C ⥤ D
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
X Y : C
f : X ⟶ Y
this : F.mapArrow.obj (mk f) = G.mapArrow.obj (mk f)
⊢ F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem mk_dvdNotUnit_mk_iff {a b : M} :
    DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b

Proof state:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b

Tactic:
rintro ⟨x, ⟨hx, rfl⟩⟩

Result:
case mpr.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x_1 ~ᵤ a * x

Proof state:
case mp.intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ¬IsUnit (x * ↑u)

Tactic:
simpa

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) → ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
rintro ⟨x, hx, u, rfl⟩

Result:
case mp.intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x * ↑u = a * x_1

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
refine Iff.rfl.and ?_

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ x, ¬IsUnit x ∧ b = a * x

Proof state:
case mpr.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x_1 ~ᵤ a * x

Tactic:
use x

Result:
no goals

Proof state:
case mp.intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ∃ x_1, ¬IsUnit x_1 ∧ a * x * ↑u = a * x_1

Tactic:
refine ⟨x * u, ?_, mul_assoc ..⟩

Result:
case mp.intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a x : M
hx : ¬IsUnit x
u : Mˣ
⊢ ¬IsUnit (x * ↑u)

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b

Tactic:
simp only [DvdNotUnit, mk_ne_zero, mk_surjective.exists, isUnit_mk, mk_mul_mk,
  mk_eq_mk_iff_associated, Associated.comm (x := b)]

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) → ∃ x, ¬IsUnit x ∧ b = a * x

case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b
-- Mathlib/Data/Part.lean
theorem map_bind {γ} (f : α → Part β) (x : Part α) (g : β → γ) :
    map g (x.bind f) = x.bind fun y => map g (f y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ (x.bind fun x => (f x).bind fun y => some (g y)) = x.bind fun y => map g (f y)

Tactic:
simp [bind_some_eq_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (x.bind f) = x.bind fun y => map g (f y)

Tactic:
rw [← bind_some_eq_map, bind_assoc]

Result:
α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ (x.bind fun x => (f x).bind fun y => some (g y)) = x.bind fun y => map g (f y)
-- Mathlib/Order/LiminfLimsup.lean
theorem _root_.OrderIso.isBoundedUnder_le_comp [Preorder α] [Preorder β] (e : α ≃o β) {l : Filter γ}
    {u : γ → α} : (IsBoundedUnder (· ≤ ·) l fun x => e (u x)) ↔ IsBoundedUnder (· ≤ ·) l u :=
  (Function.Surjective.exists e.surjective).trans <|
    exists_congr fun a => by simp only [eventually_map, e.le_iff_le]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
l : Filter γ
u : γ → α
a : α
⊢ (∀ᶠ (x : β) in map (fun x => e (u x)) l, (fun x1 x2 => x1 ≤ x2) x (e a)) ↔
    ∀ᶠ (x : α) in map u l, (fun x1 x2 => x1 ≤ x2) x a

Tactic:
simp only [eventually_map, e.le_iff_le]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem coe_false : ↑false = False

Proof state:
⊢ (false = true) = False

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isDetecting_unop_iff (𝒢 : Set Cᵒᵖ) : IsDetecting 𝒢.unop ↔ IsCodetecting 𝒢

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set Cᵒᵖ
⊢ IsDetecting 𝒢.unop ↔ IsCodetecting 𝒢

Tactic:
rw [← isCodetecting_op_iff, Set.unop_op]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma coeff_Ψ₃ : W.Ψ₃.coeff 4 = 3

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₃.coeff 4 = 3

Tactic:
rw [Ψ₃]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).coeff 4 = 3

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).coeff 4 = 3

Tactic:
compute_degree!

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem measurableSet_iInf {ι} {m : ι → MeasurableSpace α} {s : Set α} :
    MeasurableSet[iInf m] s ↔ ∀ i, MeasurableSet[m i] s

Proof state:
α : Type u_1
ι : Sort u_7
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ ∀ (i : ι), MeasurableSet s

Tactic:
rw [iInf, measurableSet_sInf, forall_mem_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_or (p q : Prop) [dpq : Decidable (p ∨ q)] [dp : Decidable p] [dq : Decidable q] :
    decide (p ∨ q) = (p || q)

Proof state:
case isTrue
p✝ q : Prop
dpq : Decidable (p✝ ∨ q)
dq : Decidable q
p : p✝
⊢ decide (p✝ ∨ q) = (decide p✝ || decide q)

Tactic:
simp [p]

Result:
no goals

Proof state:
p q : Prop
dpq : Decidable (p ∨ q)
dp : Decidable p
dq : Decidable q
⊢ decide (p ∨ q) = (decide p || decide q)

Tactic:
cases dp with | _ p => simp [p]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rank_lt {self : UnionFind} {i : Nat} : self.parent i ≠ i →
    self.rank i < self.rank (self.parent i)

Proof state:
self : UnionFind
i : Nat
⊢ self.parent i ≠ i → self.rank i < self.rank (self.parent i)

Tactic:
simpa only [rank] using self.rankD_lt

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem tendsto_mulExpNegMulSq {x : ℝ} :
    Tendsto (fun ε => mulExpNegMulSq ε x) (𝓝 0) (𝓝 x)

Proof state:
x : ℝ
⊢ Tendsto (fun ε => ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Tactic:
have : x = (fun ε : ℝ => mulExpNegMulSq ε x) 0 := by
  simp only [mulExpNegMulSq, zero_mul, neg_zero, exp_zero, mul_one]

Result:
x : ℝ
this : x = (fun ε => ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε => ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Proof state:
x : ℝ
this : x = (fun ε => ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε => ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Tactic:
nth_rw 2 [this]

Result:
x : ℝ
this : x = (fun ε => ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε => ε.mulExpNegMulSq x) (𝓝 0) (𝓝 ((fun ε => ε.mulExpNegMulSq x) 0))

Proof state:
x : ℝ
⊢ x = (fun ε => ε.mulExpNegMulSq x) 0

Tactic:
simp only [mulExpNegMulSq, zero_mul, neg_zero, exp_zero, mul_one]

Result:
no goals

Proof state:
x : ℝ
this : x = (fun ε => ε.mulExpNegMulSq x) 0
⊢ Continuous fun x_1 => rexp (-(x_1 * x * x))

Tactic:
fun_prop

Result:
no goals

Proof state:
x : ℝ
this : x = (fun ε => ε.mulExpNegMulSq x) 0
⊢ Tendsto (fun ε => ε.mulExpNegMulSq x) (𝓝 0) (𝓝 ((fun ε => ε.mulExpNegMulSq x) 0))

Tactic:
apply Continuous.tendsto (Continuous.mul continuous_const (by fun_prop))

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem CliqueFreeOn.of_succ (hs : G.CliqueFreeOn s (n + 1)) (ha : a ∈ s) :
    G.CliqueFreeOn (s ∩ G.neighborSet a) n

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : ↑t ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ insert a ↑t ⊆ s

Tactic:
exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n

Tactic:
refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : ↑t ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ ↑(insert a t) ⊆ s

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : ↑t ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ ↑(insert a t) ⊆ s

Tactic:
push_cast

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
t : Finset α
hts : ↑t ⊆ s ∩ G.neighborSet a
ht : G.IsNClique n t
⊢ insert a ↑t ⊆ s

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
a : α
n : ℕ
hs : G.CliqueFreeOn s (n + 1)
ha : a ∈ s
⊢ G.CliqueFreeOn (s ∩ G.neighborSet a) n

Tactic:
classical
refine fun t hts ht => hs ?_ (ht.insert fun b hb => (hts hb).2)
push_cast
exact Set.insert_subset_iff.2 ⟨ha, hts.trans Set.inter_subset_left⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem forM_eq [Monad m] (f : α → β → m PUnit) (l) :
    forM f l = l.toList.forM (fun (a, b) => f a b)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
inst✝ : Monad m
f : α → β → m PUnit
l : AssocList α β
⊢ forM f l =
    l.toList.forM fun x =>
      match x with
      | (a, b) => f a b

Tactic:
induction l <;> simp [*, forM]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma InjOn.image_diff_subset {f : α → β} {t : Set α} (h : InjOn f s) (hst : t ⊆ s) :
    f '' (s \ t) = f '' s \ f '' t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
hst : t ⊆ s
⊢ f '' (s \ t) = f '' s \ f '' t

Tactic:
rw [h.image_diff, inter_eq_self_of_subset_right hst]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_lt_of_countable_range (hτ : IsStoppingTime f τ)
    (h_countable : (Set.range τ).Countable) (i : ι) : MeasurableSet[f i] {ω | τ ω < i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
rw [this]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < i} ↔ ω ∈ {ω | τ ω ≤ i} \ {ω | τ ω = i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω < i}

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by ext1 ω; simp [lt_iff_le_and_ne]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet {ω | τ ω < i}

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | τ ω < i} ↔ ω ∈ {ω | τ ω ≤ i} \ {ω | τ ω = i}

Tactic:
simp [lt_iff_le_and_ne]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}
⊢ MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})

Tactic:
exact (hτ.measurableSet_le i).diff (hτ.measurableSet_eq_of_countable_range h_countable i)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem is3Clique_iff :
    G.IsNClique 3 s ↔ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
a b c : α
hab : G.Adj a b
hbc : G.Adj a c
hca : G.Adj b c
⊢ G.IsNClique 3 {a, b, c}

Tactic:
exact is3Clique_triple_iff.2 ⟨hab, hbc, hca⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
rwa [hs, eq_self_iff_true, and_true, is3Clique_triple_iff.symm, ← hs]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
obtain ⟨a, b, c, -, -, -, hs⟩ := card_eq_three.1 h.card_eq

Result:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Proof state:
case refine_2
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) → G.IsNClique 3 s

Tactic:
rintro ⟨a, b, c, hab, hbc, hca, rfl⟩

Result:
case refine_2.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableEq α
a b c : α
hab : G.Adj a b
hbc : G.Adj a c
hca : G.Adj b c
⊢ G.IsNClique 3 {a, b, c}

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ G.IsNClique 3 s ↔ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

case refine_2
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) → G.IsNClique 3 s

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
refine ⟨a, b, c, ?_⟩

Result:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
G : SimpleGraph α
s : Finset α
inst✝ : DecidableEq α
h : G.IsNClique 3 s
a b c : α
hs : s = {a, b, c}
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem covBy_span_singleton_sup {x : V} {s : Submodule K V} (h : x ∉ s) : CovBy s ((K ∙ x) ⊔ s) :=
  ⟨by simpa, (wcovBy_span_singleton_sup _ _).2⟩

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s : Submodule K V
h : x ∉ s
⊢ s < span K {x} ⊔ s

Tactic:
simpa

Result:
no goals