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

Goal state before:
pp: case h
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : (Sieve.coverByImage G (unop U)).arrows f'
⊢ (f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x) ≫ ℱ'.obj.map f'.op =
    (((f.unop ≫ x) ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)) ≫
      ℱ'.obj.map (Nonempty.some hf').lift.op

Tactic:
simp only [Category.assoc]

Goal state after:
case h
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
Y' : D
f' : Y' ⟶ unop U
hf' : (Sieve.coverByImage G (unop U)).arrows f'
⊢ f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x ≫ ℱ'.obj.map f'.op =
    f.unop ≫
      x ≫ ℱ.map (Nonempty.some hf').map.op ≫ α.app (op (Nonempty.some hf').1) ≫ ℱ'.obj.map (Nonempty.some hf').lift.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h.e_a
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ (x✝ ≫ α.app X) ≫ ℱ'.obj.map (Nonempty.some hf).map.op =
    (x✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (Nonempty.some hf).1)

Tactic:
simp only [Category.assoc]

Goal state after:
case h.e_a
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ x✝ ≫ α.app X ≫ ℱ'.obj.map (Nonempty.some hf).map.op =
    x✝ ≫ ℱ.map (Nonempty.some hf).map.op ≫ α.app (op (Nonempty.some hf).1)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
h₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (congrIndexOneOfEq ⋯ ⋯) (v₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) (v₁ k) = u₁ k

Tactic:
by
  subst h₀
  simp [h₁]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs : (e.hom ≫ e.inv).s₀ = (𝟙 E).s₀
w✝¹ : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (𝟙 E).h₀ i ≫ eqToHom ⋯
w✝ : ∀ (i j : E.I₀) (k : E.I₁ i j), (e.hom ≫ e.inv).s₁ k = (congrIndexOneOfEq ⋯ ⋯) ((𝟙 E).s₁ k)
hh :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).h₁ k = (𝟙 E).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 E).s₁ k)).inv ≫ eqToHom ⋯
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
simpa using hh i j k

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs : (e.inv ≫ e.hom).s₀ = (𝟙 F).s₀
w✝¹ : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (𝟙 F).h₀ i ≫ eqToHom ⋯
w✝ : ∀ (i j : F.I₀) (k : F.I₁ i j), (e.inv ≫ e.hom).s₁ k = (congrIndexOneOfEq ⋯ ⋯) ((𝟙 F).s₁ k)
hh :
  ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).h₁ k = (𝟙 F).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 F).s₁ k)).inv ≫ eqToHom ⋯
⊢ e.inv.h₁ k ≫ e.hom.h₁ (e.inv.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
simpa using hh i j k

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J : Type u_1
⊢ IsConnected (WidePullbackShape J)

Tactic:
by
  apply IsConnected.of_constant_of_preserves_morphisms
  intro α F H
  suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
  rintro ⟨⟩
  exacts [rfl, H (.term _)]

Goal state after:
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₂
x✝² : C
x✝¹ : x✝² ⟶ W
x✝ : (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2))).arrows x✝¹
⊢ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) ≫ F.f i₁.2 = (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2)) ≫ F.f i₂.2

Tactic:
by simpa [Category.assoc, ← pullback.condition]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝⁶ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasWeakSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝³ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
⊢ Epi ((F.obj M).freeHomEquiv.symm ((F.obj M).freeHomEquiv (G.mapFreeHom F η)))

Tactic:
simp only [mapFreeHom, Equiv.symm_apply_apply, epi_comp_iff_of_epi]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (E.refineOneHypercover F).sieve₁' i j = (F i j).sieve₀

Tactic:
by
  rw [PreOneHypercover.sieve₁']
  congr
  ext <;> simp [PreOneHypercover.toPullback]

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:
by
    refine J.superset_covering ?_ (J.pullback_stable prod.snd hs)
    intro y f hf
    dsimp [Sieve.overEquiv]
    rw [← Presieve.functorPushforward_comp]
    refine ⟨_, _, prod.lift (f ≫ prod.fst) (𝟙 _), hf, Limits.prod.hom_ext ?_ ?_⟩ <;> simp

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ hf.functor.obj U
⊢ (c' : Opens ↑X) × (hf.functor.obj c' ≅ V)

Tactic:
refine ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ ?_⟩

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ hf.functor.obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CompatiblePreserving (Opens.grothendieckTopology ↑Y) hf.functor

Tactic:
by
  have : Mono f := (TopCat.mono_iff_injective f).mpr hf.injective
  apply compatiblePreservingOfDownwardsClosed
  intro U V i
  refine ⟨(Opens.map f).obj V, eqToIso <| Opens.ext <| Set.image_preimage_eq_of_subset fun x h ↦ ?_⟩
  obtain ⟨_, _, rfl⟩ := i.le h
  exact ⟨_, rfl⟩

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible U sf
⊢ ∃! s,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i

Tactic:
exact (Types.isLimit_iff _).mp (h.isSheafPairwiseIntersections U) _ cpt.sectionPairwise.prop

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ IsSeparable {f | ∀ (i : Fin n), (f i).2 ∈ s}

Tactic:
have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by
      apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)
    rwa [Set.univ_prod] at this

Goal state after:
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 ⇑φ
⊢ moduleTopology S B' = TopologicalSpace.coinduced (⇑φ) inferInstance

Tactic:
by
  let : TopologicalSpace B' := moduleTopology S B'
  have : IsModuleTopology S B' := ⟨rfl⟩
  exact (isQuotientMap_of_surjectiveₛₗ hσ φ hφ).eq_coinduced

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝

Tactic:
apply Quot.sound

Goal state after:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M₂
inst✝ : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (↑(LinearEquiv.ofEq p q h)).toFun

Tactic:
by
    have h' : (fun x ↦ x ∈ p) = (fun x ↦ x ∈ q) := by simp [h]
    exact (Homeomorph.ofEqSubtypes h').continuous

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: case mp
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Nonempty (FinCategory C)

Tactic:
refine ⟨?_, fun a b ↦ ?_⟩

Goal state after:
case mp.refine_1
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
⊢ Fintype C

case mp.refine_2
C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
⊢ Fintype (a ⟶ b)
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : IsFiltered J
D : J ⥤ C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : (Functor.const J).obj X ⟶ D
inst✝ : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
⊢ ∃ j q, p ≫ q = s.app j ∧ q ≫ c.ι.app j = f

Tactic:
obtain ⟨j, q, hq⟩ := exists_hom_of_isColimit (X := Under.mk p) hc' (Under.homMk f rfl)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : SmallCategory J
inst✝¹ : IsFiltered J
D : J ⥤ C
c : Cocone D
hc : IsColimit c
X A : C
p : X ⟶ A
s : (Functor.const J).obj X ⟶ D
inst✝ : IsFinitelyPresentable (Under.mk p)
f : A ⟶ c.pt
h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f
this : Nonempty J
hc' : IsColimit (Under.liftCocone D s c (p ≫ f) h) := Under.isColimitLiftCocone D s c (p ≫ f) h hc
j : J
q : Under.mk p ⟶ (Under.lift D s).obj j
hq : q ≫ (Under.liftCocone D s c (p ≫ f) h).ι.app j = Under.homMk f ⋯
⊢ ∃ j q, p ≫ q = s.app j ∧ q ≫ c.ι.app j = f
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
⊢ IsCardinalPresentable (e.functor.obj X) κ

Tactic:
by
  refine ⟨fun J _ _ ↦ ⟨fun {Y} ↦ ?_⟩⟩
  have := preservesColimitsOfShape_of_isCardinalPresentable X κ J
  suffices PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) from
    ⟨fun {c} hc ↦ ⟨isColimitOfReflects uliftFunctor.{v₁}
        (isColimitOfPreserves (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) hc)⟩⟩
  have iso : coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁} ≅
    e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃} :=
    NatIso.ofComponents (fun Z ↦
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) (by
        intro _ _ f
        ext ⟨g⟩
        simp [Adjunction.homEquiv_unit])
  exact preservesColimit_of_natIso Y iso.symm

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
C₂ : Type u_11
inst✝⁷ : AddCommGroup K₂
inst✝⁶ : Module R K₂
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
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₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x y : K₃
⊢ π₁ (ρ (i₂ (σ (ι₃ (x + y))))) = π₁ (ρ (i₂ (σ (ι₃ x)))) + π₁ (ρ (i₂ (σ (ι₃ y))))

Tactic:
← map_add

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
C₂ : Type u_11
inst✝⁷ : AddCommGroup K₂
inst✝⁶ : Module R K₂
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
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₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x y : K₃
⊢ π₁ (ρ (i₂ (σ (ι₃ (x + y))))) = π₁ (ρ (i₂ (σ (ι₃ x))) + ρ (i₂ (σ (ι₃ y))))
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)
a : c₁ ⟶ c₂
⊢ ∀ (j : WalkingSpan),
    (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app j ≫ Under.Hom.right a.hom =
      (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app j

Tactic:
by rintro (_ | _ | _) <;> simp [← Under.comp_right]

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
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
⊢ ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))) ≃ₗ[A ⊗[R] S]
    A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))

Tactic:
let e₄' : (RingHom.ker φ) ≃ₗ[R] (A ⊗[R] S) ⊗[S] (RingHom.ker (algebraMap S T)) :=
    e₃ ≪≫ₗ _root_.TensorProduct.comm _ _ _ ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange _ _ S _ _).symm.restrictScalars R ≪≫ₗ
      (AlgebraTensorModule.congr (.refl S _) ePp.symm.toLinearEquiv).restrictScalars R ≪≫ₗ
      (_root_.TensorProduct.comm _ _ _).restrictScalars R

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
⊢ ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))) ≃ₗ[A ⊗[R] S]
    A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
⊢ ↑(r ^ n) = 0

Tactic:
rw [← one_mul (↑(r ^ n) : R), ← a_unit.val_inv_mul, mul_assoc, ← Nat.cast_mul,
        ← q_eq_a_mul_rn, CharP.cast_eq_zero R q, mul_zero]

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

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Tactic:
rintro rfl
    simp [TerminatedAt]

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

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : x ∈ s
⊢ ∃ i, some x = s.get? i

Tactic:
change (some x ∈ s.1) at h
    rwa [Stream'.mem_iff_exists_get_eq] at h

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.tail = (s₁.tail ⋈ s₂.tail).even

Tactic:
rw [interleave_eq, even_cons_cons, tail_cons]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : (fun x ↦ l[x]?) n = none
⊢ (fun x ↦ l[x]?) (n + 1) = none

Tactic:
rw [List.getElem?_eq_none_iff] at h ⊢
    exact Nat.le_succ_of_le h

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)

Tactic:
rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ x = y

Tactic:
apply List.ext_getElem hl

Goal state after:
α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ ∀ (i : ℕ) (h₁ : i < x.length) (h₂ : i < y.length), x[i] = y[i]
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
i✝ : ℕ
h₁✝ : i✝ < (take n (x ++ₛ a)).length
h₂✝ : i✝ < (List.take n x).length
⊢ (take n (x ++ₛ a))[i✝] = (List.take n x)[i✝]

Tactic:
rw [List.getElem_take, take_get, get_append_left]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C ((pure s.get).thinkN s.length)

Tactic:
get_eq_of_mem s M

Goal state after:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C ((pure a).thinkN s.length)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
have h' := h

Goal state after:
case pos
α : Type u
x : α
s : Seq α
h h' : (cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
have h' := h

Goal state after:
case neg
α : Type u
x : α
s : Seq α
h h' : ¬(cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1