harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_id : conjugateEquiv adj₁ adj₁ (𝟙 _) = 𝟙 _

Proof state:
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
x✝ : D
⊢ ((conjugateEquiv adj₁ adj₁) (𝟙 L₁)).app x✝ = (𝟙 R₁).app x✝

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ (conjugateEquiv adj₁ adj₁) (𝟙 L₁) = 𝟙 R₁

Tactic:
ext

Result:
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
x✝ : D
⊢ ((conjugateEquiv adj₁ adj₁) (𝟙 L₁)).app x✝ = (𝟙 R₁).app x✝
-- Mathlib/Topology/Bases.lean
theorem IsSeparable.mono {s u : Set α} (hs : IsSeparable s) (hu : u ⊆ s) : IsSeparable u

Proof state:
α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : u ⊆ s
⊢ IsSeparable u

Tactic:
rcases hs with ⟨c, c_count, hs⟩

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
s u : Set α
hu : u ⊆ s
c : Set α
c_count : c.Countable
hs : s ⊆ closure c
⊢ IsSeparable u

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
s u : Set α
hu : u ⊆ s
c : Set α
c_count : c.Countable
hs : s ⊆ closure c
⊢ IsSeparable u

Tactic:
exact ⟨c, c_count, hu.trans hs⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateCol_add (M : Matrix n n R) (j : n) (u v : n → R) :
    det (updateCol M j <| u + v) = det (updateCol M j u) + det (updateCol M j v)

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
simp [updateRow_transpose, det_transpose]

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (M.updateCol j (u + v)).det = (M.updateCol j u).det + (M.updateCol j v).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ (Mᵀ.updateRow j u).det + (Mᵀ.updateRow j v).det = (M.updateCol j u).det + (M.updateCol j v).det
-- Mathlib/GroupTheory/PGroup.lean
theorem of_card {n : ℕ} (hG : Nat.card G = p ^ n) : IsPGroup p G := fun g =>
  ⟨n, by rw [← hG, pow_card_eq_one']⟩

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
hG : Nat.card G = p ^ n
g : G
⊢ g ^ p ^ n = 1

Tactic:
rw [← hG, pow_card_eq_one']

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma le_schnirelmannDensity_iff {x : ℝ} :
    x ≤ schnirelmannDensity A ↔ ∀ n : ℕ, 0 < n → x ≤ #{a ∈ Ioc 0 n | a ∈ A} / n :=
  (le_ciInf_iff ⟨0, fun _ ⟨_, hx⟩ => hx ▸ by positivity⟩).trans Subtype.forall

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
x x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.range fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n
w✝ : { n // 0 < n }
hx : (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) w✝ = x✝¹
⊢ 0 ≤ (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) w✝

Tactic:
positivity

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
lemma tendsto_nhds_compactOpen {l : Filter α} {f : α → C(Y, Z)} {g : C(Y, Z)} :
    Tendsto f l (𝓝 g) ↔
      ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → ∀ᶠ a in l, MapsTo (f a) K U

Proof state:
α : Type u_1
Y : Type u_3
Z : Type u_4
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
l : Filter α
f : α → C(Y, Z)
g : C(Y, Z)
⊢ Tendsto f l (𝓝 g) ↔
    ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → MapsTo (⇑g) K U → ∀ᶠ (a : α) in l, MapsTo (⇑(f a)) K U

Tactic:
simp [nhds_compactOpen]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[simp]
lemma prodComparisonNatTrans_id :
    prodComparisonNatTrans (𝟭 C) A = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
A : C
⊢ prodComparisonNatTrans (𝟭 C) A = 𝟙 ((curriedTensor C).obj A ⋙ 𝟭 C)

Tactic:
ext

Result:
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
A x✝ : C
⊢ (prodComparisonNatTrans (𝟭 C) A).app x✝ = (𝟙 ((curriedTensor C).obj A ⋙ 𝟭 C)).app x✝

Proof state:
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
A x✝ : C
⊢ (prodComparisonNatTrans (𝟭 C) A).app x✝ = (𝟙 ((curriedTensor C).obj A ⋙ 𝟭 C)).app x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_sub_left (h : a ∣ c) : a ∣ b - c ↔ a ∣ b

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ c
⊢ a ∣ b - c ↔ a ∣ b

Tactic:
simpa only [← sub_eq_add_neg] using dvd_add_left (dvd_neg.2 h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_inj {i j : Fin n} : rev i = rev j ↔ i = j :=
  ⟨fun h => by simpa using congrArg rev h, congrArg _⟩

Proof state:
n : Nat
i j : Fin n
h : i.rev = j.rev
⊢ i = j

Tactic:
simpa using congrArg rev h

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
lemma completedLFunction_const_mul (a : ℂ) (Φ : ZMod N → ℂ) (s : ℂ) :
    completedLFunction (fun j ↦ a * Φ j) s = a * completedLFunction Φ s

Proof state:
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
⊢ ∑ i : ZMod N, ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaEven (toAddCircle i) s) +
      ∑ i : ZMod N, ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaOdd (toAddCircle i) s) =
    ∑ i : ZMod N, a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaEven (toAddCircle i) s)) +
      ∑ i : ZMod N, a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaOdd (toAddCircle i) s))

Tactic:
congr with i <;> ring

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
⊢ completedLFunction (fun j => a * Φ j) s = a * completedLFunction Φ s

Tactic:
simp only [completedLFunction, mul_add, mul_sum]

Result:
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
⊢ ∑ i : ZMod N, ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaEven (toAddCircle i) s) +
      ∑ i : ZMod N, ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaOdd (toAddCircle i) s) =
    ∑ i : ZMod N, a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaEven (toAddCircle i) s)) +
      ∑ i : ZMod N, a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaOdd (toAddCircle i) s))
-- Mathlib/Topology/Inseparable.lean
theorem IsClosed.continuous_piecewise_of_specializes [DecidablePred (· ∈ s)] (hs : IsClosed s)
    (hf : Continuous f) (hg : Continuous g) (hspec : ∀ x, g x ⤳ f x) :
    Continuous (s.piecewise f g)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x => x ∈ s
hs : IsClosed s
hf : Continuous f
hg : Continuous g
hspec : ∀ (x : X), g x ⤳ f x
⊢ Continuous (s.piecewise f g)

Tactic:
simpa only [piecewise_compl] using hs.isOpen_compl.continuous_piecewise_of_specializes hg hf hspec

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
lemma Γevaluation_naturality_apply (x : X) (a : Y.presheaf.obj (op ⊤)) :
    residueFieldMap f x (Y.Γevaluation (f.base x) a) =
      X.Γevaluation x (f.c.app (op ⊤) a) :=
  evaluation_naturality_apply f ⟨x, by simp only [Opens.map_top]; trivial⟩ a

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ ⊤

Tactic:
trivial

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ (Opens.map f.base).obj ⊤

Tactic:
simp only [Opens.map_top]

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ ⊤
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetAux'_cons (a : α) (l : List α) :
    powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)

Proof state:
α : Type u_1
a : α
l : List α
⊢ powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)

Tactic:
simp [powersetAux']

Result:
no goals
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_iff_forall_mem : IsBounded s ↔ ∀ x ∈ s, IsBounded s :=
  ⟨fun h _ _ ↦ h, fun h ↦ by
    rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
    exacts [isBounded_empty, h x hx]⟩

Proof state:
case inl
α : Type u_2
x✝ : Bornology α
h : ∀ x ∈ ∅, IsBounded ∅
⊢ IsBounded ∅

case inr.intro
α : Type u_2
x✝ : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
x : α
hx : x ∈ s
⊢ IsBounded s

Tactic:
exacts [isBounded_empty, h x hx]

Result:
no goals

Proof state:
α : Type u_2
x✝ : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
⊢ IsBounded s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

Result:
case inl
α : Type u_2
x✝ : Bornology α
h : ∀ x ∈ ∅, IsBounded ∅
⊢ IsBounded ∅

case inr.intro
α : Type u_2
x✝ : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
x : α
hx : x ∈ s
⊢ IsBounded s
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_sUnion {t : Set (Set α)} (h : t.PairwiseDisjoint id) (ht₀ : t.Finite)
    (ht₁ : ∀ x ∈ t, Set.Finite x) : ∏ᶠ a ∈ ⋃₀ t, f a = ∏ᶠ s ∈ t, ∏ᶠ a ∈ s, f a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Tactic:
rw [Set.sUnion_eq_biUnion]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i ∈ t, i), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i ∈ t, i), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Tactic:
exact finprod_mem_biUnion h ht₀ ht₁

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakDual.lean
theorem toSeminorm_comp (f : F →ₗ[𝕜] 𝕜) (g : E →ₗ[𝕜] F) :
    f.toSeminorm.comp g = (f.comp g).toSeminorm

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
f : F →ₗ[𝕜] 𝕜
g : E →ₗ[𝕜] F
x✝ : E
⊢ (f.toSeminorm.comp g) x✝ = (f ∘ₗ g).toSeminorm x✝

Tactic:
simp only [Seminorm.comp_apply, toSeminorm_apply, coe_comp, Function.comp_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
f : F →ₗ[𝕜] 𝕜
g : E →ₗ[𝕜] F
⊢ f.toSeminorm.comp g = (f ∘ₗ g).toSeminorm

Tactic:
ext

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
f : F →ₗ[𝕜] 𝕜
g : E →ₗ[𝕜] F
x✝ : E
⊢ (f.toSeminorm.comp g) x✝ = (f ∘ₗ g).toSeminorm x✝
-- Mathlib/Order/Filter/Map.lean
theorem neBot_inf_comap_iff_map {f : α → β} {F : Filter α} {G : Filter β} :
    NeBot (F ⊓ comap f G) ↔ NeBot (map f F ⊓ G)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (F ⊓ comap f G).NeBot ↔ (map f F ⊓ G).NeBot

Tactic:
rw [← map_neBot_iff, Filter.push_pull]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivativeFun_C (r : R) : derivativeFun (C R r) = 0

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
r : R
n : ℕ
⊢ (coeff R n) ((C R) r).derivativeFun = (coeff R n) 0

Tactic:
rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff R n).map_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ ((C R) r).derivativeFun = 0

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
r : R
n : ℕ
⊢ (coeff R n) ((C R) r).derivativeFun = (coeff R n) 0
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_mul_right_comm (M N P : Matrix m m R) : det (M * N * P) = det (M * P * N)

Proof state:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N P : Matrix m m R
⊢ (M * N * P).det = (M * P * N).det

Tactic:
rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Center.lean
theorem ext {X Y : Center C} (f g : X ⟶ Y) (w : f.f = g.f) : f = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f g : X ⟶ Y
w : f.f = g.f
⊢ f = g

Tactic:
cases f

Result:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
g : X ⟶ Y
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝, comm := comm✝ }.f = g.f
⊢ { f := f✝, comm := comm✝ } = g

Proof state:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
g : X ⟶ Y
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝, comm := comm✝ }.f = g.f
⊢ { f := f✝, comm := comm✝ } = g

Tactic:
cases g

Result:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f✝¹ : X.fst ⟶ Y.fst
comm✝¹ : ∀ (U : C), f✝¹ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝¹
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝¹, comm := comm✝¹ }.f = { f := f✝, comm := comm✝ }.f
⊢ { f := f✝¹, comm := comm✝¹ } = { f := f✝, comm := comm✝ }

Proof state:
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
f✝¹ : X.fst ⟶ Y.fst
comm✝¹ : ∀ (U : C), f✝¹ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝¹
f✝ : X.fst ⟶ Y.fst
comm✝ : ∀ (U : C), f✝ ▷ U ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ U ◁ f✝
w : { f := f✝¹, comm := comm✝¹ }.f = { f := f✝, comm := comm✝ }.f
⊢ { f := f✝¹, comm := comm✝¹ } = { f := f✝, comm := comm✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem comp_isClosedEmbedding (hf : HasCompactMulSupport f) {g : α' → α}
    (hg : IsClosedEmbedding g) : HasCompactMulSupport (f ∘ g)

Proof state:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ g ⁻¹' closure (g '' (g ⁻¹' mulSupport f)) ⊆ g ⁻¹' mulTSupport f

Tactic:
exact preimage_mono (closure_mono <| image_preimage_subset _ _)

Result:
no goals

Proof state:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ IsCompact (closure (g ⁻¹' mulSupport f))

Tactic:
refine IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_

Result:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ closure (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f

Proof state:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ closure (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f

Tactic:
rw [hg.isEmbedding.closure_eq_preimage_closure_image]

Result:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ g ⁻¹' closure (g '' (g ⁻¹' mulSupport f)) ⊆ g ⁻¹' mulTSupport f

Proof state:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ HasCompactMulSupport (f ∘ g)

Tactic:
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]

Result:
α : Type u_2
α' : Type u_3
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace α'
inst✝ : One β
f : α → β
hf : HasCompactMulSupport f
g : α' → α
hg : IsClosedEmbedding g
⊢ IsCompact (closure (g ⁻¹' mulSupport f))
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_compl_singleton_sup_pure (a : α) : 𝓝[≠] a ⊔ pure a = 𝓝 a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[≠] a ⊔ pure a = 𝓝 a

Tactic:
rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_comp {p : a ⟶ b} {f g h : b ⟶ c} {pf : a ⟶ c} {η : f ≅ g} {θ : g ≅ h}
    (η_f : p ≫ f ≅ pf) (η_g : p ≫ g ≅ pf) (η_h : p ≫ h ≅ pf)
    (ih_η : p ◁ η ≪≫ η_g = η_f) (ih_θ : p ◁ θ ≪≫ η_h = η_g) :
    p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ (p ◁ (η ≪≫ θ) ≪≫ η_h).hom = (p ◁ η ≪≫ p ◁ θ ≪≫ η_h).hom

Tactic:
simp

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = η_f

Tactic:
rw [← ih_η, ← ih_θ]

Result:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = p ◁ η ≪≫ p ◁ θ ≪≫ η_h

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f g h : b ⟶ c
pf : a ⟶ c
η : f ≅ g
θ : g ≅ h
η_f : p ≫ f ≅ pf
η_g : p ≫ g ≅ pf
η_h : p ≫ h ≅ pf
ih_η : p ◁ η ≪≫ η_g = η_f
ih_θ : p ◁ θ ≪≫ η_h = η_g
⊢ p ◁ (η ≪≫ θ) ≪≫ η_h = p ◁ η ≪≫ p ◁ θ ≪≫ η_h

Tactic:
apply Iso.ext (by simp)

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_inter_of_inter_eq (t : Set α) {s₁ s₂ s : Set α} (h : s₁ ∩ s = s₂ ∩ s) :
    t.ite s₁ s₂ ∩ s = s₁ ∩ s

Proof state:
α : Type u
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s

Tactic:
rw [← ite_inter, ← h, ite_same]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_comp' {g : β →ᵈ γ} {f : α →ᵈ β}
    (hne : ∃ x y : α, edist x y ≠ 0 ∧ edist x y ≠ ⊤) : ratio (g.comp f) = ratio g * ratio f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (g.comp f)) * edist x y = edist ((g.comp f) x) ((g.comp f) y)
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_left_inj hα.1 hα.2]
  at hgf

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
⊢ ratio (g.comp f) = ratio g * ratio f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (g.comp f)) = ↑(ratio g) * ↑(ratio f)
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
rwa [← ENNReal.coe_inj, ENNReal.coe_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
rcases hne with ⟨x, y, hα⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (g.comp f) = ratio g * ratio f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
have hgf := (edist_eq (g.comp f) x y).symm

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (g.comp f)) * edist x y = edist ((g.comp f) x) ((g.comp f) y)
⊢ ratio (g.comp f) = ratio g * ratio f
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem disjoint_closedBall_ball_iff (hδ : 0 ≤ δ) (hε : 0 < ε) :
    Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Tactic:
rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.mono (hf : LocallyIntegrable f μ) {g : X → F}
    (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖g x‖ ≤ ‖f x‖) :
    LocallyIntegrable g μ

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrable g μ

Tactic:
rw [← locallyIntegrableOn_univ] at hf ⊢

Result:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
hf : LocallyIntegrableOn f univ μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g univ μ

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
hf : LocallyIntegrableOn f univ μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g univ μ

Tactic:
exact hf.mono hg h

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma hasFPowerSeriesOnBall_pi_iff (hr : 0 < r) :
    HasFPowerSeriesOnBall (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e r ↔
      ∀ i, HasFPowerSeriesOnBall (f i) (p i) e r

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hr : 0 < r
⊢ HasFPowerSeriesOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e r ↔
    ∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r

Tactic:
simp_rw [← hasFPowerSeriesWithinOnBall_univ]

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hr : 0 < r
⊢ HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e r ↔
    ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hr : 0 < r
⊢ HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e r ↔
    ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) Set.univ e r

Tactic:
exact hasFPowerSeriesWithinOnBall_pi_iff hr

Result:
no goals