mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : ℤ → Module.End R V
hf : ∀ (x : V), BddBelow (Function.support fun y ↦ (f y) x)
n : ℤ
⊢ ncoeff (of_coeff f hf) n = f (-n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
⊢ ∀ (s : Set (Tropical R)), ¬BddBelow s → sInf s = sInf ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
⊢ star (toConv comul) = toConv (↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ∘ₗ comul)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
inst✝³ : CommSemiring R
inst✝² : StarRing R
n : Type u_8
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x✝ : n
⊢ star (toConv comul) = toConv (↑(TensorProduct.comm R R R) ∘ₗ comul)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R✝ : Type u_1
E : Type u_2
F : Type u_3
inst✝³¹ : Semiring R✝
inst✝³⁰ : InvolutiveStar R✝
inst✝²⁹ : AddCommMonoid E
inst✝²⁸ : Module R✝ E
inst✝²⁷ : StarAddMonoid E
inst✝²⁶ : StarModule R✝ E
inst✝²⁵ : AddCommMonoid F
inst✝²⁴ : Module R✝ F
inst✝²³ : StarAddMonoid F
inst✝²² : StarModule R✝ F
G : Type u_4
inst✝²¹ : AddCommMonoid G
inst✝²⁰ : Module R✝ G
inst✝¹⁹ : StarAddMonoid G
inst✝¹⁸ : StarModule R✝ G
R : Type u_5
A : Type u_6
C : Type u_7
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : NonUnitalNonAssocSemiring A
inst✝¹⁴ : Module R A
inst✝¹³ : SMulCommClass R A A
inst✝¹² : IsScalarTower R A A
inst✝¹¹ : StarRing A
inst✝¹⁰ : StarModule R A
inst✝⁹ : AddCommMonoid C
inst✝⁸ : Module R C
inst✝⁷ : StarAddMonoid C
inst✝⁶ : StarModule R C
n : Type u_8
inst✝⁵ : DecidableEq n
B : n → Type u_9
inst✝⁴ : (i : n) → AddCommMonoid (B i)
inst✝³ : (i : n) → Module R (B i)
inst✝² : (i : n) → StarAddMonoid (B i)
inst✝¹ : ∀ (i : n), StarModule R (B i)
inst✝ : Fintype n
m : Type u_10
⊢ star (toConv comul) = toConv (↑(TensorProduct.comm R (n → R) (n → R)) ∘ₗ comul)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : WithConv ((m → R) →ₗ[R] n → R)
⊢ toMatrix' (star f).ofConv = (toMatrix' f.ofConv).map star

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : WithConv ((m → R) →ₗ[R] n → R)
⊢ IsSelfAdjoint f ↔ ∀ (i : n) (j : m), IsSelfAdjoint (toMatrix' f.ofConv i j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n m R
⊢ star (toConv (toLin' A)) = toConv (toLin' (A.map star))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n m R
⊢ IsSelfAdjoint (toConv (toLin' A)) ↔ ∀ (i : n) (j : m), IsSelfAdjoint (A i j)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : Semiring R
inst✝⁸ : InvolutiveStar R
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : StarAddMonoid E
inst✝⁴ : StarModule R E
inst✝³ : AddCommMonoid F
inst✝² : Module R F
inst✝¹ : StarAddMonoid F
inst✝ : StarModule R F
f : WithConv (End R E)ˣ
⊢ (End R E)ˣ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
f : WithConv (End R E)
hf : IsUnit f.ofConv
⊢ IsUnit (star f).ofConv

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
α : R
x : V
⊢ x ∈ (star f).ofConv.eigenspace α ↔ star x ∈ f.ofConv.eigenspace (star α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Category.{v_1, w} J
inst✝ : HasLimitsOfShape J C
X : TopCat
F : J ⥤ Presheaf C X
H : ∀ (j : J), (F.obj j).IsSheaf
c : Cone F
hc : IsLimit c
⊢ c.pt.IsSheaf

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
⊢ spectrum R (star f).ofConv = star (spectrum R f.ofConv)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
n : Γ
u v : V
⊢ ((of R).symm (A (u + v))).coeff n = ((of R).symm (A u)).coeff n + ((of R).symm (A v)).coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
n : Γ
r : R
v : V
⊢ ((of R).symm (A (r • v))).coeff n = (RingHom.id R) r • ((of R).symm (A v)).coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝¹ x✝ : HVertexOperator Γ R V W
⊢ (fun n ↦ { toFun := fun v ↦ ((of R).symm ((x✝¹ + x✝) v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) =
    (fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝¹ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) + fun n ↦
      { toFun := fun v ↦ ((of R).symm (x✝ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝¹ : R
x✝ : HVertexOperator Γ R V W
⊢ (fun n ↦ { toFun := fun v ↦ ((of R).symm ((x✝¹ • x✝) v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) =
    (RingHom.id R) x✝¹ • fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
⊢ Function.Injective ⇑coeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝¹ x✝ : V
⊢ (of R) { coeff := fun g ↦ (f g) (x✝¹ + x✝), isPWO_support' := ⋯ } =
    (of R) { coeff := fun g ↦ (f g) x✝¹, isPWO_support' := ⋯ } +
      (of R) { coeff := fun g ↦ (f g) x✝, isPWO_support' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝¹ : R
x✝ : V
⊢ (of R) { coeff := fun g ↦ (f g) (x✝¹ • x✝), isPWO_support' := ⋯ } =
    (RingHom.id R) x✝¹ • (of R) { coeff := fun g ↦ (f g) x✝, isPWO_support' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
g' : Γ'
hg' : ¬A (((of R).symm (B u)).coeff g') = 0
hAB : ((of R).symm (B u)).coeff g' = 0
⊢ A (((of R).symm (B u)).coeff g') = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u : U
⊢ (Function.support fun g' ↦ A ((coeff B g') u)).IsPWO

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
⊢ A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
⊢ A.compHahnSeries B (r • u) = r • A.compHahnSeries B u

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
⊢ ∀ (x y : U),
    (of R) (A.compHahnSeries B (x + y)).ofIterate =
      (of R) (A.compHahnSeries B x).ofIterate + (of R) (A.compHahnSeries B y).ofIterate

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ✝ : Type u_1
inst✝¹⁴ : PartialOrder Γ✝
R✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
inst✝¹³ : CommRing R✝
inst✝¹² : AddCommGroup V✝
inst✝¹¹ : Module R✝ V✝
inst✝¹⁰ : AddCommGroup W✝
inst✝⁹ : Module R✝ W✝
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
⊢ ∀ (m : R) (x : U),
    (of R) (A.compHahnSeries B (m • x)).ofIterate = (RingHom.id R) m • (of R) (A.compHahnSeries B x).ofIterate

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
g : Lex (Γ' × Γ)
⊢ coeff (A.comp B) g = coeff A (ofLex g).2 ∘ₗ coeff B (ofLex g).1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pullback

Goal state before:
pp: C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
D : Type u₃
inst✝⁷ : Category.{v₃, u₃} D
G : C ⥤ D
A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁵ : G.IsContinuous J K
inst✝⁴ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasLeftKanExtension F
inst✝³ : RepresentablyFlat G
inst✝² : HasSheafify K A
inst✝¹ : HasSheafify J A
inst✝ : PreservesFiniteLimits G.op.lan
⊢ PreservesFiniteLimits (sheafPullback G A J K)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pullback

Goal state before:
pp: C : Type v₁
inst✝¹¹ : SmallCategory C
D : Type v₁
inst✝¹⁰ : SmallCategory D
G : C ⥤ D
A : Type u₁
inst✝⁹ : Category.{v₁, u₁} A
J : GrothendieckTopology C
K : GrothendieckTopology D
FA : A → A → Type u_1
CA : A → Type v₁
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : PreservesLimits (forget A)
inst✝⁵ : HasColimits A
inst✝⁴ : HasLimits A
inst✝³ : PreservesFilteredColimits (forget A)
inst✝² : (forget A).ReflectsIsomorphisms
inst✝¹ : G.IsContinuous J K
inst✝ : RepresentablyFlat G
⊢ PreservesFiniteLimits (G.sheafPullback A J K)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
U : Opens ↑↑Y
x : ↑↑X
hx : (ConcreteCategory.hom α.base) x ∈ U
⊢ Y.presheaf.germ U ((ConcreteCategory.hom α.base) x) hx ≫ Hom.stalkMap α x =
    α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ X.presheaf.germ (h.functor.obj V) ((ConcreteCategory.hom f) x) ⋯ ≫ (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝)) ≫
        (presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.functor.op.whiskerLeft ((Sheaf.forget A Y).map u)) ≫
          ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj Y✝).obj) ⋯)).hom =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝)) ≫
        ObjectProperty.homMk (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj X✝).obj) ⋯) ≫
          (sheafPullback A hf).map u).hom

Tactic:
rw [ObjectProperty.FullSubcategory.comp_hom, ObjectProperty.FullSubcategory.comp_hom,
      ObjectProperty.FullSubcategory.comp_hom, ObjectProperty.FullSubcategory.comp_hom]

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map
            (⋯.functor.op.whiskerLeft ((Sheaf.forget A Y).map u))).hom ≫
        (ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj Y✝).obj) ⋯)).hom =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).map (⋯.pullbackIso.hom.app ((Sheaf.forget A Y).obj X✝))).hom ≫
      (ObjectProperty.homMk
            (sheafifyLift (Opens.grothendieckTopology ↑X) (𝟙 ((sheafPullback A hf).obj X✝).obj) ⋯)).hom ≫
        ((sheafPullback A hf).map u).hom
Module: Mathlib.Topology.Sheaves.Functors

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
⊢ Sheaf.pullback A f ≅ sheafPullback A hf

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
w : α.hom.base = β.hom.base
⊢ (Opens.map α.hom.base).op = (Opens.map β.hom.base).op

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map β.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ (X.restrictStalkIso h x).inv = Hom.stalkMap (X.ofRestrict h) x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ α.hom = β.hom

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ IsIso (Hom.stalkMap (X.ofRestrict h) x)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ Hom.stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f g : X ⟶ Y
h : f.hom.base = g.hom.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap f.hom x = (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g.hom x
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ Hom.stalkMap (α ≫ β) x = Hom.stalkMap β ((ConcreteCategory.hom α.base) x) ≫ Hom.stalkMap α x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

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

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

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

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

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

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ (ConcreteCategory.hom (α ≫ β).base) x = x

Tactic:
by

Goal state after: