harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem inseparable_iff_clusterPt_uniformity {x y : α} :
    Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)

Proof state:
α : Type u
inst✝ : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ Inseparable x y

Tactic:
simp_rw [uniformity_hasBasis_closed.inseparable_iff_uniformity, isClosed_iff_clusterPt]

Result:
α : Type u
inst✝ : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ ∀ (i : Set (α × α)), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i

Proof state:
α : Type u
inst✝ : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ ∀ (i : Set (α × α)), (i ∈ 𝓤 α ∧ ∀ (a : α × α), ClusterPt a (𝓟 i) → a ∈ i) → (x, y) ∈ id i

Tactic:
exact fun U ⟨hU, hUc⟩ ↦ hUc _ <| h.mono <| le_principal_iff.2 hU

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
x y : α
⊢ Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)

Tactic:
refine ⟨fun h ↦ .of_nhds_le h.nhds_le_uniformity, fun h ↦ ?_⟩

Result:
α : Type u
inst✝ : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ Inseparable x y
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsPreconnected.Icc_subset {s : Set α} (hs : IsPreconnected s) {a b : α} (ha : a ∈ s)
    (hb : b ∈ s) : Icc a b ⊆ s

Proof state:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Tactic:
simpa only [image_id] using hs.intermediate_value ha hb continuousOn_id

Result:
no goals
-- Mathlib/Data/Multiset/Dedup.lean
theorem Disjoint.dedup_add {s t : Multiset α} (h : Disjoint s t) :
    dedup (s + t) = dedup s + dedup t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ (s + t).dedup = s.dedup + t.dedup

Tactic:
induction s, t using Quot.induction_on₂

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ (Quot.mk (⇑(isSetoid α)) a✝ + Quot.mk (⇑(isSetoid α)) b✝).dedup =
    dedup (Quot.mk (⇑(isSetoid α)) a✝) + dedup (Quot.mk (⇑(isSetoid α)) b✝)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
simpa using h

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ (Quot.mk (⇑(isSetoid α)) a✝ + Quot.mk (⇑(isSetoid α)) b✝).dedup =
    dedup (Quot.mk (⇑(isSetoid α)) a✝) + dedup (Quot.mk (⇑(isSetoid α)) b✝)

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.dedup_append (by simpa using h)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldr_cons (t : RBNode α) (l) : t.foldr (·::·) l = t.toList ++ l

Proof state:
α : Type u_1
t : RBNode α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t l = t.toList ++ l

Tactic:
unfold toList

Result:
α : Type u_1
t : RBNode α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t l = foldr (fun x1 x2 => x1 :: x2) t [] ++ l

Proof state:
α : Type u_1
t : RBNode α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t l = foldr (fun x1 x2 => x1 :: x2) t [] ++ l

Tactic:
induction t generalizing l with
| nil => rfl
| node _ a _ b iha ihb => rw [foldr, foldr, iha, iha (_::_), ihb]; simp

Result:
no goals

Proof state:
case node
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
iha : ∀ (l : List α), foldr (fun x1 x2 => x1 :: x2) a l = foldr (fun x1 x2 => x1 :: x2) a [] ++ l
ihb : ∀ (l : List α), foldr (fun x1 x2 => x1 :: x2) b l = foldr (fun x1 x2 => x1 :: x2) b [] ++ l
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) a [] ++ v✝ :: (foldr (fun x1 x2 => x1 :: x2) b [] ++ l) =
    foldr (fun x1 x2 => x1 :: x2) a [] ++ v✝ :: foldr (fun x1 x2 => x1 :: x2) b [] ++ l

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) nil l = foldr (fun x1 x2 => x1 :: x2) nil [] ++ l

Tactic:
rfl

Result:
no goals

Proof state:
case node
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
iha : ∀ (l : List α), foldr (fun x1 x2 => x1 :: x2) a l = foldr (fun x1 x2 => x1 :: x2) a [] ++ l
ihb : ∀ (l : List α), foldr (fun x1 x2 => x1 :: x2) b l = foldr (fun x1 x2 => x1 :: x2) b [] ++ l
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) (node c✝ a v✝ b) l = foldr (fun x1 x2 => x1 :: x2) (node c✝ a v✝ b) [] ++ l

Tactic:
rw [foldr, foldr, iha, iha (_::_), ihb]

Result:
case node
α : Type u_1
c✝ : RBColor
a : RBNode α
v✝ : α
b : RBNode α
iha : ∀ (l : List α), foldr (fun x1 x2 => x1 :: x2) a l = foldr (fun x1 x2 => x1 :: x2) a [] ++ l
ihb : ∀ (l : List α), foldr (fun x1 x2 => x1 :: x2) b l = foldr (fun x1 x2 => x1 :: x2) b [] ++ l
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) a [] ++ v✝ :: (foldr (fun x1 x2 => x1 :: x2) b [] ++ l) =
    foldr (fun x1 x2 => x1 :: x2) a [] ++ v✝ :: foldr (fun x1 x2 => x1 :: x2) b [] ++ l
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/--
Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℤ`.
-/
lemma hasSum_int_hurwitzZetaEven (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℤ ↦ 1 / (↑|n + a| : ℂ) ^ s / 2) (hurwitzZetaEven a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)

Tactic:
have := (hasSum_int_completedHurwitzZetaEven a hs).div_const (Gammaℝ s)

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun i => s.Gammaℝ / ↑|↑i + a| ^ s / 2 / s.Gammaℝ) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
⊢ HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (hurwitzZetaEven (↑a) s)

Tactic:
rw [hurwitzZetaEven, Function.update_of_ne (ne_zero_of_one_lt_re hs)]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun i => s.Gammaℝ / ↑|↑i + a| ^ s / 2 / s.Gammaℝ) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
n : ℤ
⊢ 1 / ↑|↑n + a| ^ s / 2 = s.Gammaℝ / ↑|↑n + a| ^ s / 2 / s.Gammaℝ

Tactic:
simp only [div_right_comm _ _ (Gammaℝ _),
div_self (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun i => s.Gammaℝ / ↑|↑i + a| ^ s / 2 / s.Gammaℝ) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
⊢ HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)

Tactic:
exact this.congr_fun fun n ↦ by simp only [div_right_comm _ _ (Gammaℝ _),
  div_self (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
theorem Continuous.exists_forall_le_of_hasCompactMulSupport [ClosedIicTopology α] [Nonempty β]
    [One α] {f : β → α} (hf : Continuous f) (h : HasCompactMulSupport f) :
    ∃ x : β, ∀ y : β, f x ≤ f y

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
x : β
hx : ∀ (i : β), f x ≤ f i
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
exact ⟨x, hx⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
x : β
hx : f x ∈ lowerBounds (range f)
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
rw [mem_lowerBounds, forall_mem_range] at hx

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
x : β
hx : ∀ (i : β), f x ≤ f i
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
⊢ ∃ x, ∀ (y : β), f x ≤ f y

Tactic:
obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.isCompact_range hf).exists_isLeast (range_nonempty _)

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
x : β
hx : f x ∈ lowerBounds (range f)
⊢ ∃ x, ∀ (y : β), f x ≤ f y
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem coe_range (φ : F) :
    ((NonUnitalAlgHom.range φ : NonUnitalSubalgebra R B) : Set B) = Set.range (φ : A → B)

Proof state:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ (∃ x, φ x = x✝) ↔ x✝ ∈ Set.range ⇑φ

Tactic:
rfl

Result:
no goals

Proof state:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ

Tactic:
rw [SetLike.mem_coe, mem_range]

Result:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ (∃ x, φ x = x✝) ↔ x✝ ∈ Set.range ⇑φ

Proof state:
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
⊢ ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ

Tactic:
ext

Result:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_lt_one (ha : 0 ≤ a) : ⌊a⌋₊ < 1 ↔ a < 1 :=
  (floor_lt ha).trans <| by rw [Nat.cast_one]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ a < ↑1 ↔ a < 1

Tactic:
rw [Nat.cast_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitFlipCompLimIsoLimitCompLim_inv_π_π (k) (j) :
    (limitFlipCompLimIsoLimitCompLim F).inv ≫ limit.π _ k ≫ limit.π _ j =
      (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
k : K
j : J
⊢ (limitFlipCompLimIsoLimitCompLim F).inv ≫ limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j =
    limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
dsimp [limitFlipCompLimIsoLimitCompLim]

Result:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
k : K
j : J
⊢ ((((limitUncurryIsoLimitCompLim F).inv ≫
            (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫
          (HasLimit.isoOfNatIso (uncurryObjFlip F)).inv) ≫
        (limitUncurryIsoLimitCompLim F.flip).hom) ≫
      limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j =
    limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
k : K
j : J
⊢ ((((limitUncurryIsoLimitCompLim F).inv ≫
            (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫
          (HasLimit.isoOfNatIso (uncurryObjFlip F)).inv) ≫
        (limitUncurryIsoLimitCompLim F.flip).hom) ≫
      limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j =
    limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem isEmbedding_of_pullback {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsEmbedding f)
    (H₂ : IsEmbedding g) : IsEmbedding (limit.π (cospan f g) WalkingCospan.one)

Proof state:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) =
    ⇑(ConcreteCategory.hom (pullback.snd f g ≫ g))

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]

Result:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) =
    ⇑(ConcreteCategory.hom (pullback.snd f g ≫ g))

Proof state:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsEmbedding ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one))

Tactic:
convert H₂.comp (snd_isEmbedding_of_left H₁ g)

Result:
case h.e'_5.h
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S
⊢ ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one)) =
    ⇑(ConcreteCategory.hom g) ∘ ⇑(ConcreteCategory.hom (pullback.snd f g))
-- Mathlib/Data/Finset/Image.lean
theorem _root_.Function.Injective.mem_finset_image (hf : Injective f) :
    f a ∈ s.image f ↔ a ∈ s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
⊢ f a ∈ image f s ↔ a ∈ s

Tactic:
refine ⟨fun h => ?_, Finset.mem_image_of_mem f⟩

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
h : f a ∈ image f s
⊢ a ∈ s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
h : f a ∈ image f s
⊢ a ∈ s

Tactic:
obtain ⟨y, hy, heq⟩ := mem_image.1 h

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
h : f a ∈ image f s
y : α
hy : y ∈ s
heq : f y = f a
⊢ a ∈ s

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
h : f a ∈ image f s
y : α
hy : y ∈ s
heq : f y = f a
⊢ a ∈ s

Tactic:
exact hf heq ▸ hy

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem card_roots_sub_C' {p : R[X]} {a : R} (hp0 : 0 < degree p) :
    Multiset.card (p - C a).roots ≤ natDegree p :=
  WithBot.coe_le_coe.1
    (le_trans (card_roots_sub_C hp0)
      (le_of_eq <| degree_eq_natDegree fun h => by simp_all [lt_irrefl]))

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
h : p = 0
⊢ False

Tactic:
simp_all [lt_irrefl]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
@[simp]
lemma filter_sub (p : α → Prop) [DecidablePred p] (s t : Multiset α) :
    filter p (s - t) = filter p s - filter p t

Proof state:
case pos.e_a
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
by_cases m : a ∈ s

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : a ∈ s
⊢ filter p (s.erase a) = (filter p s).erase a

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : a ∉ s
⊢ filter p (s.erase a) = (filter p s).erase a
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
lemma _root_.integrable_cexp_quadratic' (hb : b.re < 0) (c d : ℂ) :
    Integrable (fun (x : ℝ) ↦ cexp (b * x ^ 2 + c * x + d))

Proof state:
b c d : ℂ
hb : b = 0
⊢ 0 ≤ b.re

Tactic:
rw [hb, zero_re]

Result:
no goals

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume

Tactic:
have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
H : ¬Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume
⊢ False

Tactic:
simpa [hb', pi_ne_zero, Complex.exp_ne_zero, integral_undef H]
  using integral_cexp_quadratic hb c d

Result:
no goals

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
⊢ b ≠ 0

Tactic:
contrapose! hb

Result:
b c d : ℂ
hb : b = 0
⊢ 0 ≤ b.re

Proof state:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume

Tactic:
by_contra H

Result:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
H : ¬Integrable (fun x => cexp (b * ↑x ^ 2 + c * ↑x + d)) volume
⊢ False
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_bot (f : β → α) : limsup f ⊥ = ⊥

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ limsup f ⊥ = ⊥

Tactic:
simp [limsup]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem range_comp_val : (f.comp S.val).range = S.map f

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
⊢ (f.comp S.val).range = map f S

Tactic:
rw [AlgHom.range_comp, range_val]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_commute (s : Finset α) (f : α → β) (comm) (y : β)
    (h : ∀ x ∈ s, Commute y (f x)) : Commute y (s.noncommProd f comm)

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y✝ y

Tactic:
rw [Multiset.mem_map]

Result:
case h
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ (∃ a ∈ s.val, f a = y) → Commute y✝ y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
⊢ Commute y (s.noncommProd f comm)

Tactic:
apply Multiset.noncommProd_commute

Result:
case h
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
⊢ ∀ x ∈ Multiset.map f s.val, Commute y x

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ (∃ a ∈ s.val, f a = y) → Commute y✝ y

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

Result:
case h.intro.intro
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
⊢ ∀ x ∈ Multiset.map f s.val, Commute y x

Tactic:
intro y

Result:
case h
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y✝ : β
h : ∀ x ∈ s, Commute y✝ (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y✝ y

Proof state:
case h.intro.intro
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)

Tactic:
exact h x hx

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean
theorem det_sum_smul_le {ι : Type*} (s : Finset ι) {c : ι → R} {A : ι → Matrix n n R}
    {abv : AbsoluteValue R S} {x : S} (hx : ∀ k i j, abv (A k i j) ≤ x) {y : S}
    (hy : ∀ k, abv (c k) ≤ y) :
    abv (det (∑ k ∈ s, c k • A k)) ≤
      Nat.factorial (Fintype.card n) • (#s • y * x) ^ Fintype.card n

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Nontrivial R
inst✝² : LinearOrderedCommRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
c : ι → R
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x
y : S
hy : ∀ (k : ι), abv (c k) ≤ y
⊢ abv (∑ k ∈ s, c k • A k).det ≤ (Fintype.card n).factorial • (#s • y * x) ^ Fintype.card n

Tactic:
simpa only [smul_mul_assoc] using
  det_sum_le s fun k i j =>
    calc
      abv (c k * A k i j) = abv (c k) * abv (A k i j) := abv.map_mul _ _
      _ ≤ y * x := mul_le_mul (hy k) (hx k i j) (abv.nonneg _) ((abv.nonneg _).trans (hy k))

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem map_eq_of_inverse {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : φ ∘ ψ = id)
    (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) : map φ f = g

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map φ (map ψ g)

Tactic:
rw [map_map, eq, map_id]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ map φ f = g

Tactic:
refine le_antisymm hφ (le_trans ?_ (map_mono hψ))

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : φ ∘ ψ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ g ≤ map φ (map ψ g)