mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case pair.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

pp: case pair.pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }

Tactic:
· refine
          ⟨[{   left := ⟨⟨⟩⟩
                right := single i
                hom := ObjectProperty.homMk (homOfLE (a.hom.le.trans (by simp))) },
              { left := ⟨⟨⟩⟩
                right := pair i i'
                hom := ObjectProperty.homMk (homOfLE
                  (le_inf ((a.hom.le).trans (by simp)) b.hom.le)) }, _],
                ?_, rfl⟩
        exact
          List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.singleton _)))

Goal state after:
case pair.pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
⊢ U ⊔ V = iSup ι

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔ x✝ ∈ ↑(iSup ι)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔ ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) → ∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
x✝ : ↑X
⊢ (∃ i, x✝ ∈ ↑(WalkingPair.casesOn i.down U V)) → x✝ ∈ ↑(U ⊔ V)
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
⊢ stalkPushforward C (𝟙 X) ℱ x = (stalkFunctor C x).map (Pushforward.id ℱ).hom

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ ((pushforward C (𝟙 X)).obj ℱ).germ U✝ ((ConcreteCategory.hom (𝟙 X)) x) hxU✝ ≫ stalkPushforward C (𝟙 X) ℱ x =
    ((pushforward C (𝟙 X)).obj ℱ).germ U✝ ((ConcreteCategory.hom (𝟙 X)) x) hxU✝ ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ stalkPushforward C (f ≫ g) ℱ x =
    stalkPushforward C g ((pushforward C f).obj ℱ) ((ConcreteCategory.hom f) x) ≫ stalkPushforward C f ℱ x

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : TopCat
ℱ : Presheaf C X
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
U✝ : Opens ↑Z
hxU✝ : (ConcreteCategory.hom (f ≫ g)) x ∈ U✝
⊢ ((pushforward C (f ≫ g)).obj ℱ).germ U✝ ((ConcreteCategory.hom (f ≫ g)) x) hxU✝ ≫ stalkPushforward C (f ≫ g) ℱ x =
    ((pushforward C (f ≫ g)).obj ℱ).germ U✝ ((ConcreteCategory.hom (f ≫ g)) x) hxU✝ ≫
      stalkPushforward C g ((pushforward C f).obj ℱ) ((ConcreteCategory.hom f) x) ≫ stalkPushforward C f ℱ x
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case iUV
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ (i : Bool) → (if i = true then U₁ else U₂) ⟶ V

Tactic:
exact fun i => if h : i then eqToHom (if_pos h) ≫ i₁ else eqToHom (if_neg h) ≫ i₂

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
⊢ F.stalkSpecializes ⋯ = 𝟙 (F.stalk x)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : x ∈ U✝
⊢ F.germ U✝ x hxU✝ ≫ F.stalkSpecializes ⋯ = F.germ U✝ x hxU✝ ≫ 𝟙 (F.stalk x)
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
⊢ F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
U✝ : Opens ↑X
hxU✝ : z ∈ U✝
⊢ F.germ U✝ z hxU✝ ≫ F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.germ U✝ z hxU✝ ≫ F.stalkSpecializes ⋯
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
⊢ F.stalkSpecializes h ≫ (stalkFunctor C x).map f = (stalkFunctor C y).map f ≫ G.stalkSpecializes h

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
U✝ : Opens ↑X
hxU✝ : y ∈ U✝
⊢ F.germ U✝ y hxU✝ ≫ F.stalkSpecializes h ≫ (stalkFunctor C x).map f =
    F.germ U✝ y hxU✝ ≫ (stalkFunctor C y).map f ≫ G.stalkSpecializes h
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
⊢ ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x =
    stalkPushforward C f F y ≫ F.stalkSpecializes h

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U✝ : Opens ↑Y
hxU✝ : (Hom.hom f) y ∈ U✝
⊢ ((pushforward C f).obj F).germ U✝ ((Hom.hom f) y) hxU✝ ≫
      ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x =
    ((pushforward C f).obj F).germ U✝ ((Hom.hom f) y) hxU✝ ≫ stalkPushforward C f F y ≫ F.stalkSpecializes h
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case hcover
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ (U₁ ≤ ⨆ t, if t = true then U₁ else U₂) ∧ U₂ ≤ ⨆ t, if t = true then U₁ else U₂

Tactic:
constructor

Goal state after:
case hcover.left
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ U₁ ≤ ⨆ t, if t = true then U₁ else U₂

case hcover.right
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ U₂ ≤ ⨆ t, if t = true then U₁ else U₂
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
⊢ U ⊔ V = iSup ι

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔ x✝ ∈ ↑(iSup ι)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) ↔
    ∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) →
    ∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
x✝ : ↑X
⊢ (∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)) →
    x✝ ∈ ↑(U ⊔ V)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
x✝ y✝ : (i : ι) → φ i
⊢ (fun i ↦ (x✝ + y✝) (f i)) = (fun i ↦ x✝ (f i)) + fun i ↦ y✝ (f i)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
x✝¹ y✝ : (i : ι) → φ i
x✝ : α
⊢ (x✝¹ + y✝) (f x✝) = ((fun i ↦ x✝¹ (f i)) + fun i ↦ y✝ (f i)) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
m✝ : R
x✝ : (i : ι) → φ i
⊢ (fun i ↦ (m✝ • x✝) (f i)) = (RingHom.id R) m✝ • fun i ↦ x✝ (f i)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
m✝ : R
x✝¹ : (i : ι) → φ i
x✝ : α
⊢ (m✝ • x✝¹) (f x✝) = ((RingHom.id R) m✝ • fun i ↦ x✝¹ (f i)) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹⁰ : Semiring R
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
⊢ (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂

Tactic:
ext

Goal state after:
case hl
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹⁰ : Semiring R
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
x✝ : M₁
⊢ ((f₁ + g₁).coprod (f₂ + g₂) ∘SL inl R M₁ M₂) x✝ = ((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inl R M₁ M₂) x✝

case hr
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹⁰ : Semiring R
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
x✝ : M₂
⊢ ((f₁ + g₁).coprod (f₂ + g₂) ∘SL inr R M₁ M₂) x✝ = ((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inr R M₁ M₂) x✝
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2

Tactic:
ext

Goal state after:
case hl
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
x✝ : M₁
⊢ ((r • a.1).coprod (r • a.2) ∘SL inl R M₁ M₂) x✝ = ((r • a.1.coprod a.2) ∘SL inl R M₁ M₂) x✝

case hr
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
x✝ : M₂
⊢ ((r • a.1).coprod (r • a.2) ∘SL inr R M₁ M₂) x✝ = ((r • a.1.coprod a.2) ∘SL inr R M₁ M₂) x✝
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
⊢ (∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ) ↔
    τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'}

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ (∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ) →
    τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'}

case mpr
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ id = (fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
x✝ : R
⊢ id x✝ = ((fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1)) x✝
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 • p.2
⊢ (fun p ↦ p.1 • p.2) ∘ Prod.map ⇑σ ⇑φ = ⇑φ ∘ fun p ↦ p.1 • p.2

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 • p.2
x✝ : R × A
⊢ ((fun p ↦ p.1 • p.2) ∘ Prod.map ⇑σ ⇑φ) x✝ = (⇑φ ∘ fun p ↦ p.1 • p.2) x✝