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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheaf ↔ F.IsSheafPairwiseIntersections

Tactic:
rw [isSheaf_iff_isSheafOpensLeCover, isSheafOpensLeCover_iff_isSheafPairwiseIntersections]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_1
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
hι : U ⊔ V = iSup ι
⊢ (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) →
    ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj X_1 ⟶
      ((Pairwise.diagram ι).op ⋙ F.presheaf).obj X_1

Tactic:
rintro ((_ | _) | (_ | _))
    exacts [s.fst, s.snd, s.fst ≫ F.1.map (homOfLE inf_le_left).op,
      s.snd ≫ F.1.map (homOfLE inf_le_left).op]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
⊢ stalkPullbackInv C f F x ≫ stalkPullbackHom C f F x = 𝟙 (((pullback C f).obj F).stalk x)

Tactic:
ext V hV
    dsimp
    rw [germ_stalkPullbackInv_assoc, Category.comp_id, germToPullbackStalk_stalkPullbackHom]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ (Set.univ.pi fun i ↦ ↑(s i)) ⊆ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i))

Tactic:
· simp only [Set.subset_def, mem_closure_iff]
    intro x hx U hU hxU
    rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩
    refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
    · simp_all [Finset.sum_pi_single]
    · exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝² x✝¹ x✝ : F
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝² x✝¹ x✝ : F
⊢ ∀ (x : α), (x✝² * x✝¹ * x✝) x = (x✝² * (x✝¹ * x✝)) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ 1 * x✝ = x✝

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (1 * x✝) x = x✝ x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ x✝ * 1 = x✝

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (x✝ * 1) x = x✝ x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ 0 * x✝ = 0

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (0 * x✝) x = 0 x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
f : F
⊢ f * 0 = 0

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
f : F
⊢ ∀ (x : α), (f * 0) x = 0 x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
f g h : F
⊢ f * (g + h) = f * g + f * h

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
f g h : F
⊢ ∀ (x : α), (f * (g + h)) x = (f * g + f * h) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
x✝² x✝¹ x✝ : F
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
x✝² x✝¹ x✝ : F
⊢ ∀ (x : α), ((x✝² + x✝¹) * x✝) x = (x✝² * x✝ + x✝¹ * x✝) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
⊢ ↑0 = 0

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
⊢ ∀ (x : α), ↑0 x = 0 x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
n : ℕ
⊢ ∀ (x : α), ↑(n + 1) x = (↑n + 1) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
x✝ : ℕ
⊢ ∀ (x : α), (IntCast.intCast ↑x✝) x = ↑x✝ x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = -↑(n + 1)

Tactic:
apply DFunLike.ext

Goal state after:
F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
n : ℕ
⊢ ∀ (x : α), (IntCast.intCast (Int.negSucc n)) x = (-↑(n + 1)) x
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : ↑(RingCat.FilteredColimits.colimit R)
m n : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j)
    (b c : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
        (Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            b +
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            c) =
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            b +
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c

Tactic:
by
    rintro ⟨U, a⟩ ⟨V₁, b₁⟩ ⟨V₂, b₂⟩
    obtain ⟨s, α, β, h₁, h₂, h₃, h₄⟩ := crown₄
      (leftToMax U V₁ ≫ leftToMax (max U V₁) (max U V₂)) (leftToMax U (max V₁ V₂))
      (leftToMax U V₂ ≫ rightToMax (max U V₁) (max U V₂)) (leftToMax U (max V₁ V₂))
      (rightToMax U V₁ ≫ leftToMax (max U V₁) (max U V₂))
      (leftToMax V₁ V₂ ≫ rightToMax U (max V₁ V₂))
      (rightToMax U V₂ ≫ rightToMax (max U V₁) (max U V₂))
      (rightToMax V₁ V₂ ≫ rightToMax U (max V₁ V₂))
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ β α ?_
    dsimp
    -- We use this pattern instead of a single `simp` to avoid heatbeat modifications
    rw [H, H, H]
    simp only [← ConcreteCategory.comp_apply, ← Functor.map_comp]
    simp only [map_add, ← ConcreteCategory.comp_apply, ← Functor.map_comp, h₁, h₂, h₃, h₄, H]
    simp only [Functor.map_comp, RingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
      Category.assoc, AddCommGrpCat.hom_comp, AddMonoidHom.coe_comp, smul_add]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
h : (fun fb ↦ (bil fb.1) fb.2) = fun fb ↦ ∑ i, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
⊢ Continuous fun fb ↦ ∑ i, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2

Tactic:
have : ContinuousAdd C := toContinuousAdd R C

Goal state after:
case intro
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
h : (fun fb ↦ (bil fb.1) fb.2) = fun fb ↦ ∑ i, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
this : ContinuousAdd C
⊢ Continuous fun fb ↦ ∑ i, fb.1 i • (bil ⇑(Finsupp.single i 1)) fb.2
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
inst✝ : Mul α
⊢ mapMulHom (MulHom.id α) = MonoidHom.id (WithOne α)

Tactic:
ext x
  induction x <;> rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝¹⁶ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁵ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝¹⁴ : RingHomInvPair σ₂₃ σ₃₂
inst✝¹³ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝¹² : RingHomInvPair σ₁₃ σ₃₁
inst✝¹¹ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁰ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : AddCommMonoid M₁
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
M₃ : Type u_6
inst✝⁴ : TopologicalSpace M₃
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
⊢ ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
⊢ (piScalarRightHom R S N ι) (x ⊗ₜ[R] f) = fun j ↦ f j • x

Tactic:
ext j
  simp [piScalarRightHom, piScalarRightHomBil]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ (∀ (y : ↑B), ∃ y_1, (ConcreteCategory.hom fBC) y_1 = (ConcreteCategory.hom (pushout.inl φ ψ)) y) ∧
    ∀ (y : ↑C), ∃ y_1, (ConcreteCategory.hom fBC) y_1 = (ConcreteCategory.hom (pushout.inr φ ψ)) y

Tactic:
exact ⟨fun x ↦ ⟨.X (.inl x), by simp [fBC, PBC]⟩, fun x ↦ ⟨.X (.inr x), by simp [fBC, PBC]⟩⟩

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ g₁ (ρ (i₂ (σ (ι₃ x)))) - i₂ (f₁ y) = 0

Tactic:
← hy,

Goal state after:
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ g₁ (i₁ y) - i₂ (f₁ y) = 0
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_3
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑P
⊢ (CommRingCat.Hom.hom g) ((ConcreteCategory.hom π) x) =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩) ≫
          c.ι.app c'.pt))
      ((ConcreteCategory.hom π) x)

Tactic:
suffices (π ≫ g) x = (g' ≫ F.map (c'.ι.app none) ≫ c.ι.app _) x by
      simpa only [CommRingCat.hom_comp, CommRingCat.hom_ofHom,
        RingHom.liftOfRightInverse_comp_apply, coe_comp, Function.comp_apply] using! this

Goal state after:
case refine_3
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑P
⊢ (ConcreteCategory.hom (π ≫ g)) x =
    (ConcreteCategory.hom
        (g' ≫ F.map (c'.ι.app none) ≫ c.ι.app (((Functor.const (WidePushoutShape ↥s)).obj c'.pt).obj none)))
      x
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: case inst
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (commaObj (𝟭 T) (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})

Tactic:
apply Over.closedUnderLimitsOfShape_discrete_empty _

Goal state after: