mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Sieve.functorPushforward H (imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
⊢ Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback m (imageSieve f a))) ∈ K (H.obj Z)

Tactic:
refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_) hh

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Sieve.functorPushforward H (imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
⊢ imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a) ≤
    Sieve.functorPullback H (Sieve.pullback m (imageSieve f a))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (E.inter F.toPreOneHypercover).sieve₁ p₁ p₂ ∈ J W

Tactic:
by
    rw [PreOneHypercover.sieve₁_inter h]
    refine J.bind_covering (E.mem₁ _ _ _ _ (by simpa using! h)) fun _ _ _ ↦ ?_
    exact J.pullback_stable _
      (F.mem₁ _ _ _ _ (by simpa [Category.assoc, ← pullback.condition]))

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

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
⊢ Sieve.functorPushforward (Over.star X) S ∈ (J.over X) ((Over.star X).obj U)

Tactic:
refine J.superset_covering ?_ (J.pullback_stable prod.snd hs)

Goal state after:
C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
⊢ Sieve.pullback prod.snd S ≤ (Sieve.overEquiv ((Over.star X).obj U)) (Sieve.functorPushforward (Over.star X) S)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
exact Or.inr ((isIso_iff_mk_eq_top _).mp ((Simple.mono_isIso_iff_nonzero i).mpr h))

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | ∀ x ∈ X, ∃ U f, R f ∧ x ∈ U}
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | ∀ x ∈ Y, ∃ U f, R f ∧ x ∈ U}
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
⊢ ∃ U f, S.bind Ti f ∧ x ∈ U

Tactic:
rcases hTi f hf x hU with ⟨V, g, hg, hV⟩

Goal state after:
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | ∀ x ∈ X, ∃ U f, R f ∧ x ∈ U}
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | ∀ x ∈ Y, ∃ U f, R f ∧ x ∈ U}
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : Ti f hf g
hV : x ∈ V
⊢ ∃ U f, S.bind Ti f ∧ x ∈ U
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ≅ G
X : SheafOfModules S
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ X.val.presheaf.map (α.hom.app (Opposite.unop U)).op ≫ X.val.presheaf.map (α.inv.app (Opposite.unop U)).op =
    𝟙 (X.val.presheaf.obj (Opposite.op (G.obj (Opposite.unop U))))

Tactic:
simp only [← Functor.map_comp, ← op_comp,
      Iso.inv_hom_id_app, op_id, CategoryTheory.Functor.map_id]

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

Goal state before:
pp: case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
⊢ x ∈ U → x ∈ iSup (coveringOfPresieve U R)

Tactic:
hxU

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ U
⊢ x ∈ iSup (coveringOfPresieve U R)
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: 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
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
⊢ objPairwiseOfFamily sf ∈ ((Pairwise.diagram U).op ⋙ F).sections

Tactic:
rintro (i | ⟨i, j⟩) (i' | ⟨i', j'⟩) (_ | _ | _ | _)

Goal state after:
case single.single.id_single
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
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.id_single i))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.single i))

case single.pair.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
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.left i j'))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j'))

case single.pair.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
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i i' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.right i' i))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i' i))

case pair.pair.id_pair
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
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.id_pair i j))))
      (objPairwiseOfFamily sf (op (Pairwise.pair i j))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case hcover
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
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✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↑X
⊢ x ∈ U → x ∈ iSup V

Tactic:
hxU

Goal state after:
case hcover
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
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✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↑X
hxU : x ∈ U
⊢ x ∈ iSup V
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)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
⊢ x ∈ U → (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty

Tactic:
hxU

Goal state after:
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)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
⊢ (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
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✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
x : ↑X
⊢ x ∈ U → x ∈ iSup V

Tactic:
hxU

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
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✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
x : ↑X
hxU : x ∈ U
⊢ x ∈ iSup V
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝¹ : ContinuousAdd M
this✝ : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this : IsModuleTopology R P
⊢ instTopologicalSpaceProd ≤ moduleTopology R (M × N)

Tactic:
have : ContinuousAdd P := ModuleTopology.continuousAdd R P

Goal state after:
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this✝ : IsModuleTopology R P
this : ContinuousAdd P
⊢ instTopologicalSpaceProd ≤ moduleTopology R (M × N)
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ IsEffective R S

Tactic:
refine Module.FaithfullyFlat.lTensor_reflects_exact _ _ _ _ <|
    AddMonoidHom.exact_iff_of_surjective_of_bijective_of_injective
      ((Algebra.linearMap R S).lTensor T) ((TensorProduct.includeLeftSubRight R S).lTensor T)
      (Algebra.linearMap T (T ⊗[R] S)) (TensorProduct.includeLeftSubRight T (T ⊗[R] S))
      (TensorProduct.rid R R T).toAddMonoidHom (AddMonoidHom.id (T ⊗[R] S))
      (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S).toAddMonoidHom ?_ ?_
      (TensorProduct.rid R R T).surjective Function.bijective_id
      ((TensorProduct.AlgebraTensorModule.distribBaseChange R T S S).injective) |>.mpr ‹_›

Goal state after:
case refine_1
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ (↑(Algebra.linearMap T (T ⊗[R] S))).comp (TensorProduct.rid R R T).toAddEquiv.toAddMonoidHom =
    (AddMonoidHom.id (T ⊗[R] S)).comp ↑(LinearMap.lTensor T (Algebra.linearMap R S))

case refine_2
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ (↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S))).comp (AddMonoidHom.id (T ⊗[R] S)) =
    (↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)).toAddMonoidHom.comp
      ↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S))
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : FinCategory C
⊢ Finite (Arrow C)

Tactic:
by
  rw [Arrow.finite_iff]
  exact ⟨inferInstance⟩

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))
y : K₂
⊢ g₁ 0 = i₂ (ι₂ y)

Tactic:
by rw [map_zero, hι₂.apply_apply_eq_zero]

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

Goal state before:
pp: case mpr
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₃
⊢ x ∈ Set.range ⇑F → (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0

Tactic:
· rintro ⟨y, rfl⟩
    exact (δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ (ι₂ y) congr($hF y)
      _ (by rw [map_zero, hι₂.apply_apply_eq_zero])).trans π₁.map_zero

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
m : M
x y : ↥(f.eqLocus g)
⊢ ⟨m ⊗ₜ[R] ↑(x + y), ⋯⟩ = ⟨m ⊗ₜ[R] ↑x, ⋯⟩ + ⟨m ⊗ₜ[R] ↑y, ⋯⟩

Tactic:
simp [tmul_add]

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
m : M
x y : ↥f.ker
⊢ ⟨m ⊗ₜ[R] ↑(x + y), ⋯⟩ = ⟨m ⊗ₜ[R] ↑x, ⋯⟩ + ⟨m ⊗ₜ[R] ↑y, ⋯⟩

Tactic:
simp [tmul_add]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A B : P.Over Q X
g : A ⟶ B
⊢ ((𝟭 (P.Over Q X)).map g ≫ Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj B).left) B.hom ⋯) ⋯ ⋯).left =
    (Over.homMk (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯) ⋯ ⋯ ≫ (map Q hPf ⋙ pullback P Q f).map g).left

Tactic:
apply pullback.hom_ext <;> simp

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
q : ℕ
⊢ Nat.Prime q → MixedCharZero R q → P

Tactic:
q_prime

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ p > 0, MixedCharZero R p → P
q : ℕ
q_prime : Nat.Prime q
⊢ MixedCharZero R q → P
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Seq α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ ↑s'.tail = (↑s').tail

Tactic:
cases s' using Subtype.recOn

Goal state after:
case mk
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s : Seq α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
r✝ : R s ⟨val✝, property✝⟩
this : s.head = head ⟨val✝, property✝⟩ ∧ R s.tail (tail ⟨val✝, property✝⟩)
r : R s.tail (tail ⟨val✝, property✝⟩)
⊢ ↑(tail ⟨val✝, property✝⟩) = (↑⟨val✝, property✝⟩).tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ (map f (a :: s)).head :: (map f (a :: s)).tail = f a :: map f s

Tactic:
map_eq

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ (f (a :: s).head :: map f (a :: s).tail).head :: (f (a :: s).head :: map f (a :: s).tail).tail = f a :: map f s
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
⊢ ↑(cons b s') k.succ = ↑s' k

Tactic:
cases s' using Subtype.recOn

Goal state after:
case mk
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
e : some a = ↑(cons b ⟨val✝, property✝⟩) (k + 1)
⊢ ↑(cons b ⟨val✝, property✝⟩) k.succ = ↑⟨val✝, property✝⟩ k
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
⊢ m = n

Tactic:
by have := h1.terminates; have := h2.terminates; rw [← h1.length, h2.length]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
by
  by_cases h : s.Terminates
  · simpa [length'_of_terminates h] using length_le_iff
  · simpa [length'_of_not_terminates h] using forall_not_of_not_exists h n

Goal state after: