harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/AlgebraicClosure.lean
theorem map_eq_of_algebraicClosure_eq_bot [Algebra E K] [IsScalarTower F E K]
    (h : algebraicClosure E K = ⊥) :
    (algebraicClosure F E).map (IsScalarTower.toAlgHom F E K) = algebraicClosure F K

Proof state:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E) = algebraicClosure F K

Tactic:
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

Result:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
x : K
hx : x ∈ algebraicClosure F K
⊢ x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
y : E
hx : (algebraMap E K) y ∈ algebraicClosure F K
⊢ (algebraMap E K) y ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)

Tactic:
exact ⟨y, (map_mem_algebraicClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
x : K
hx : x ∈ algebraicClosure F K
⊢ x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)

Tactic:
obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2
  (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)

Result:
case intro
F : Type u_1
E : Type u_2
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : algebraicClosure E K = ⊥
y : E
hx : (algebraMap E K) y ∈ algebraicClosure F K
⊢ (algebraMap E K) y ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegrable_const (a : E) (c : ℂⁿ) (R : ℝⁿ) : TorusIntegrable (fun _ => a) c R

Proof state:
n : ℕ
E : Type u_1
inst✝ : NormedAddCommGroup E
a : E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ TorusIntegrable (fun x => a) c R

Tactic:
simp [TorusIntegrable, measure_Icc_lt_top]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_iSup [Finite β] {f : β → L.BoundedFormula α n}
    {v : α → M} {v' : Fin n → M} :
    (iSup f).Realize v v' ↔ ∃ b, (f b).Realize v v'

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
n : ℕ
inst✝ : Finite β
f : β → L.BoundedFormula α n
v : α → M
v' : Fin n → M
⊢ (iSup f).Realize v v' ↔ ∃ b, (f b).Realize v v'

Tactic:
simp only [iSup, realize_foldr_sup, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and,
  exists_exists_eq_and]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_neg (f : ℕ → ℂ) (s : ℂ) : term (-f) s = -term f s

Proof state:
f : ℕ → ℂ
s : ℂ
⊢ term (-f) s = -term f s

Tactic:
ext ⟨- | n⟩ <;>
simp [neg_div]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous_iff_map_ωSup_of_orderHom {f : α →o β} :
    ωScottContinuous f ↔ ∀ c : Chain α, f (ωSup c) = ωSup (c.map f)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ (∃ (hf : Monotone ⇑f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := ⇑f, monotone' := hf })) ↔
    ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

Tactic:
exact exists_prop_of_true f.monotone'

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ ωScottContinuous ⇑f ↔ ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

Tactic:
rw [ωScottContinuous_iff_monotone_map_ωSup]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ (∃ (hf : Monotone ⇑f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := ⇑f, monotone' := hf })) ↔
    ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)
-- Mathlib/Data/Set/Countable.lean
theorem countable_insert {s : Set α} {a : α} : (insert a s).Countable ↔ s.Countable

Proof state:
α : Type u
s : Set α
a : α
⊢ (insert a s).Countable ↔ s.Countable

Tactic:
simp only [insert_eq, countable_union, countable_singleton, true_and]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ZModModule.sub_eq_add (x y : G) : x - y = x + y

Proof state:
G : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : Module (ZMod 2) G
x y : G
⊢ x - y = x + y

Tactic:
simp [neg_eq_self, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem closure_subset_thickening {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) :
    closure E ⊆ thickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ cthickening 0 E ⊆ thickening δ E

Tactic:
exact cthickening_subset_thickening' δ_pos δ_pos E

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ closure E ⊆ thickening δ E

Tactic:
rw [← cthickening_zero]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ cthickening 0 E ⊆ thickening δ E
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem dist_le_of_le_geometric_two_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ C / 2 ^ n

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n

Tactic:
symm

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n = C / 2 ^ n

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C / 2 ^ n

Tactic:
convert dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ (n + m)

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n = C / 2 ^ n

Tactic:
exact ((hasSum_geometric_two' C).div_const _).tsum_eq

Result:
no goals

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ (n + m)

Tactic:
simp only [add_comm n, pow_add, ← div_div]

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoMetricSpace α
C : ℝ
f : ℕ → α
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem iSupLift_comp_inclusion {i : ι} (h : K i ≤ T) :
    (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Proof state:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem coe_eq_zero : (q : ℚ) = 0 ↔ q = 0

Proof state:
q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem _root_.Polynomial.toLaurent_X : (toLaurent Polynomial.X : R[T;T⁻¹]) = T 1

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ toLaurent X = T 1

Tactic:
have : (Polynomial.X : R[X]) = monomial 1 1 := by simp [← C_mul_X_pow_eq_monomial]

Result:
R : Type u_1
inst✝ : Semiring R
this : X = (monomial 1) 1
⊢ toLaurent X = T 1

Proof state:
R : Type u_1
inst✝ : Semiring R
this : X = (monomial 1) 1
⊢ toLaurent X = T 1

Tactic:
simp [this, Polynomial.toLaurent_C_mul_T]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ X = (monomial 1) 1

Tactic:
simp [← C_mul_X_pow_eq_monomial]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem stmts_trans {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h₁ : q₁ ∈ stmts₁ q₂) :
    some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ some q₂ ∈ stmts M S → some q₁ ∈ stmts M S

Tactic:
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
  forall_eq', exists_imp, and_imp]

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h₁ : q₁ ∈ stmts₁ q₂
⊢ ∀ x ∈ S, q₂ ∈ stmts₁ (M x) → ∃ a ∈ S, q₁ ∈ stmts₁ (M a)

Tactic:
exact fun l ls h₂ ↦ ⟨_, ls, stmts₁_trans h₂ h₁⟩

Result:
no goals
-- Mathlib/Order/Bounds/OrderIso.lean
theorem isLUB_image {s : Set α} {x : β} : IsLUB (f '' s) x ↔ IsLUB s (f.symm x) :=
  ⟨fun h => IsLUB.of_image (by simp) ((f.apply_symm_apply x).symm ▸ h), fun h =>
    (IsLUB.of_image (by simp)) <| (f.symm_image_image s).symm ▸ h⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB (⇑f '' s) x
⊢ ∀ {x y : α}, f x ≤ f y ↔ x ≤ y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB s (f.symm x)
⊢ ∀ {x y : β}, f.symm x ≤ f.symm y ↔ x ≤ y

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_trans (θ₁ θ₂ : Real.Angle) :
    (o.rotation θ₁).trans (o.rotation θ₂) = o.rotation (θ₂ + θ₁) :=
  LinearIsometryEquiv.ext fun _ => by rw [← rotation_rotation, LinearIsometryEquiv.trans_apply]

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ₁ θ₂ : Real.Angle
x✝ : V
⊢ ((o.rotation θ₁).trans (o.rotation θ₂)) x✝ = (o.rotation (θ₂ + θ₁)) x✝

Tactic:
rw [← rotation_rotation, LinearIsometryEquiv.trans_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem cuspFunction_zero_eq_limUnder_nhds_ne :
    cuspFunction h f 0 = limUnder (𝓝[≠] 0) (cuspFunction h f)

Proof state:
h : ℝ
f : ℂ → ℂ
⊢ cuspFunction h f 0 = limUnder (𝓝[≠] 0) (cuspFunction h f)

Tactic:
conv_lhs => simp only [cuspFunction, update_self]

Result:
h : ℝ
f : ℂ → ℂ
⊢ limUnder (𝓝[≠] 0) (f ∘ invQParam h) = limUnder (𝓝[≠] 0) (cuspFunction h f)

Proof state:
h : ℝ
f : ℂ → ℂ
r : ℂ
hr : r ∈ {0}ᶜ
⊢ (f ∘ invQParam h) r = cuspFunction h f r

Tactic:
rw [cuspFunction, update_of_ne hr]

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
⊢ limUnder (𝓝[≠] 0) (f ∘ invQParam h) = limUnder (𝓝[≠] 0) (cuspFunction h f)

Tactic:
refine congr_arg lim (Filter.map_congr <| eventuallyEq_nhdsWithin_of_eqOn fun r hr ↦ ?_)

Result:
h : ℝ
f : ℂ → ℂ
r : ℂ
hr : r ∈ {0}ᶜ
⊢ (f ∘ invQParam h) r = cuspFunction h f r
-- Mathlib/CategoryTheory/IsConnected.lean
theorem any_functor_const_on_obj [IsPreconnected J] {α : Type u₂} (F : J ⥤ Discrete α) (j j' : J) :
    F.obj j = F.obj j'

Proof state:
case as
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ (F.obj j).as = (F.obj j').as

Tactic:
exact ((isoConstant F j').hom.app j).down.1

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ F.obj j = F.obj j'

Tactic:
ext

Result:
case as
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ (F.obj j).as = (F.obj j').as
-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem closure_range_zpow_eq_pow (x : G) :
    closure (range (x ^ · : ℤ → G)) = closure (range (x ^ · : ℕ → G))

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ closure (range fun x_1 => x ^ x_1) = closure (range fun x_1 => x ^ x_1)

Tactic:
ext y

Result:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
⊢ y ∈ closure (range fun x_1 => x ^ x_1) ↔ y ∈ closure (range fun x_1 => x ^ x_1)

Proof state:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
⊢ y ∈ closure (range fun x_1 => x ^ x_1) ↔ y ∈ closure (range fun x_1 => x ^ x_1)

Tactic:
exact (mapClusterPt_atTop_pow_tfae y x).out 3 2

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem fiber_nonempty_iff_mem_image {y : β} : (s.filter (f · = y)).Nonempty ↔ y ∈ s.image f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
y : β
⊢ (filter (fun x => f x = y) s).Nonempty ↔ y ∈ image f s

Tactic:
simp [Finset.Nonempty]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem linearProjOfIsCompl_apply_eq_zero_iff (h : IsCompl p q) {x : E} :
    linearProjOfIsCompl p q h x = 0 ↔ x ∈ q

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ (p.linearProjOfIsCompl q h) x = 0 ↔ x ∈ q

Tactic:
simp [linearProjOfIsCompl]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem trans_assoc {Z' : C} (α : X ≅ Y) (β : Y ≅ Z) (γ : Z ≅ Z') :
    (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

Tactic:
ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom

Tactic:
simp only [trans_hom, Category.assoc]

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem isLeft_right (h : LiftRel r s (inl a) y) : y.isLeft

Proof state:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a : α
c✝ : γ
a✝ : r a c✝
⊢ (inl c✝).isLeft = true

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
a : α
h : LiftRel r s (inl a) y
⊢ y.isLeft = true

Tactic:
cases h

Result:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a : α
c✝ : γ
a✝ : r a c✝
⊢ (inl c✝).isLeft = true
-- Mathlib/Algebra/Polynomial/Div.lean
theorem finiteMultiplicity_X_sub_C (a : R) (h0 : p ≠ 0) : FiniteMultiplicity (X - C a) p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
⊢ FiniteMultiplicity (X - C a) p

Tactic:
haveI := Nontrivial.of_polynomial_ne h0

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ FiniteMultiplicity (X - C a) p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ FiniteMultiplicity (X - C a) p

Tactic:
refine finiteMultiplicity_of_degree_pos_of_monic ?_ (monic_X_sub_C _) h0

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < (X - C a).degree

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1

Tactic:
decide

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < (X - C a).degree

Tactic:
rw [degree_X_sub_C]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ 0 < 1
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[simp]
lemma iso_hom_base_inv_base {X Y : LocallyRingedSpace.{u}} (e : X ≅ Y) :
    e.hom.base ≫ e.inv.base = 𝟙 _

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.hom.base ≫ e.inv.base = 𝟙 ↑X.toPresheafedSpace

Tactic:
rw [← SheafedSpace.comp_base, ← LocallyRingedSpace.comp_toShHom]

Result:
X Y : LocallyRingedSpace
e : X ≅ Y
⊢ (Hom.toShHom (e.hom ≫ e.inv)).base = 𝟙 ↑X.toPresheafedSpace

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
⊢ (Hom.toShHom (e.hom ≫ e.inv)).base = 𝟙 ↑X.toPresheafedSpace

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_neg_one (x : ℝ) : x ^ (-1 : ℝ) = x⁻¹

Proof state:
x : ℝ
⊢ x ^ ↑(-1) = x⁻¹

Tactic:
simp only [rpow_intCast, zpow_one, zpow_neg]

Result:
no goals

Proof state:
x : ℝ
⊢ x ^ (-1) = x⁻¹

Tactic:
suffices H : x ^ ((-1 : ℤ) : ℝ) = x⁻¹ by rwa [Int.cast_neg, Int.cast_one] at H

Result:
x : ℝ
⊢ x ^ ↑(-1) = x⁻¹

Proof state:
x : ℝ
H : x ^ ↑(-1) = x⁻¹
⊢ x ^ (-1) = x⁻¹

Tactic:
rwa [Int.cast_neg, Int.cast_one] at H

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem closure_eq_iInter_thickening (E : Set α) :
    closure E = ⋂ (δ : ℝ) (_ : 0 < δ), thickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ δ, ⋂ (_ : 0 < δ), thickening δ E

Tactic:
exact cthickening_eq_iInter_thickening rfl.ge E

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ closure E = ⋂ δ, ⋂ (_ : 0 < δ), thickening δ E

Tactic:
rw [← cthickening_zero]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ δ, ⋂ (_ : 0 < δ), thickening δ E
-- Mathlib/Order/WithBot.lean
@[simp] lemma bot_lt_coe (a : α) : ⊥ < (a : WithBot α)

Proof state:
α : Type u_1
inst✝ : LT α
a : α
⊢ ⊥ < ↑a

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
private lemma map_map_of_eq.{w}  {C : Type u} [Category.{v} C] (V : Cᵒᵖ ⥤ Type w) {X Y Z : C}
    {α : X ⟶ Y} {β : Y ⟶ Z} {γ : X ⟶ Z} {φ} :
    α ≫ β = γ → V.map α.op (V.map β.op φ) = V.map γ.op φ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
V : Cᵒᵖ ⥤ Type w
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
γ : X ⟶ Z
φ : V.obj (op Z)
⊢ α ≫ β = γ → V.map α.op (V.map β.op φ) = V.map γ.op φ

Tactic:
rintro rfl

Result:
C : Type u
inst✝ : Category.{v, u} C
V : Cᵒᵖ ⥤ Type w
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
φ : V.obj (op Z)
⊢ V.map α.op (V.map β.op φ) = V.map (α ≫ β).op φ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
V : Cᵒᵖ ⥤ Type w
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
φ : V.obj (op Z)
⊢ V.map α.op (V.map β.op φ) = V.map (α ≫ β).op φ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem forall_dual_apply_eq_zero_iff (v : V) : (∀ φ : Module.Dual K V, φ v = 0) ↔ v = 0

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
v : V
⊢ (∀ (φ : Dual K V), φ v = 0) ↔ v = 0

Tactic:
rw [← eval_apply_eq_zero_iff K v, LinearMap.ext_iff]

Result:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
v : V
⊢ (∀ (φ : Dual K V), φ v = 0) ↔ ∀ (x : Dual K V), ((eval K V) v) x = 0 x

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
v : V
⊢ (∀ (φ : Dual K V), φ v = 0) ↔ ∀ (x : Dual K V), ((eval K V) v) x = 0 x

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_inf_principal_neBot_of_image_mem {f : Filter β} {m : α → β} (hf : NeBot f) {s : Set α}
    (hs : m '' s ∈ f) : NeBot (comap m f ⊓ 𝓟 s)

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ (comap m f ⊓ 𝓟 s).NeBot

Tactic:
rw [neBot_inf_comap_iff_map', map_principal, ← frequently_mem_iff_neBot]

Result:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ ∃ᶠ (x : β) in f, x ∈ m '' s

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : f.NeBot
s : Set α
hs : m '' s ∈ f
⊢ ∃ᶠ (x : β) in f, x ∈ m '' s

Tactic:
exact Eventually.frequently hs

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem mul_top' : a * ∞ = if a = 0 then 0 else ∞

Proof state:
a : ℝ≥0∞
⊢ a * ⊤ = if a = 0 then 0 else ⊤

Tactic:
convert WithTop.mul_top' a

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_nonpos (f : R → R) (a : A) (h : ∀ x ∈ σₙ R a, f x ≤ 0) :
    cfcₙ f a ≤ 0

Proof state:
case neg.inl
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
hf : ¬ContinuousOn f (σₙ R a)
⊢ cfcₙ f a ≤ 0

Tactic:
simp only [cfcₙ_apply_of_not_continuousOn _ hf, le_rfl]

Result:
no goals

Proof state:
case pos.intro
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁵ : OrderedCommSemiring R
inst✝¹⁴ : Nontrivial R
inst✝¹³ : StarRing R
inst✝¹² : MetricSpace R
inst✝¹¹ : IsTopologicalSemiring R
inst✝¹⁰ : ContinuousStar R
inst✝⁹ : ∀ (α : Type ?u.1025025) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ σₙ R a, f x ≤ 0
h₁ : ContinuousOn f (σₙ R a)
h₂ : f 0 = 0
⊢ cfcₙ f a ≤ 0

Tactic:
simpa using cfcₙ_mono h

Result:
no goals