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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : Z ⟶ X
⊢ mapPreimage K G F f ≫ F.obj.map g.op = mapPreimage K G F (G.map g ≫ f)

Tactic:
mapPreimage_comp,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : Z ⟶ X
⊢ mapPreimage K G F f ≫ F.obj.map g.op = mapPreimage K G F f ≫ mapPreimage K G F (G.map g)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case pullback
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
⊢ Sieve.functorPushforward G (Sieve.pullback f S) ∈ K (G.obj Y)

Tactic:
| pullback X S _ Y f ih =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x✝¹)) ≫ ((proj K B).mapCone c✝).π.app x✝ = x✝¹.π.app x✝

Tactic:
rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F✝ : J × K ⥤ Type v
inst✝ : IsFiltered K
F : J ⥤ K ⥤ Type v
⊢ IsIso (colimitLimitToLimitColimitCone F)

Tactic:
have : IsIso (colimitLimitToLimitColimitCone F).hom := by
    suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso
    infer_instance
  apply Cone.cone_iso_of_hom_iso

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
· rintro ⟨W, a, b, h, w⟩
    let T := Over.mk (b ≫ W.hom)
    let c : T ⟶ Y₁ := Over.homMk g (by dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f])
    let d : T ⟶ W := Over.homMk b
    refine ⟨T, c, 𝟙 Z, ?_, by simp [T, c]⟩
    rw [show c ≫ f = d ≫ a by ext; exact w]
    exact S.downward_closed 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 : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
⊢ E.toPreOneHypercover.sieve₁' i j = ⊤

Tactic:
eq_top_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
⊢ ⊤ ≤ E.toPreOneHypercover.sieve₁' i j
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
down✝ : U ≤ V
a₂✝ : U ⟶ V
a✝ : (fun f ↦ Set.inclusion ⋯) { down := { down := down✝ } } = (fun f ↦ Set.inclusion ⋯) a₂✝
⊢ { down := { down := down✝ } } = a₂✝

Tactic:
congr!

Goal state after:
Module: Mathlib.Topology.Category.TopCat.OpenNhds

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
x : ↑X
U V W : OpenNhds x
down✝ : U ≤ V
a₂✝ : U ⟶ V
a✝ : (fun f ↦ Set.inclusion ⋯) { down := { down := down✝ } } = (fun f ↦ Set.inclusion ⋯) a₂✝
⊢ { down := { down := down✝ } } = a₂✝

Tactic:
congr!

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) = U

Tactic:
apply le_antisymm

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) ≤ U

case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case refine_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
x : ↑X
⊢ x ∈ ↑(⋯.functor.obj U) ↔ x ∈ ↑((map (inclusionTopIso X).inv).obj U)

Tactic:
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨x, trivial⟩, h, rfl⟩⟩

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
R : Sieve X
hR : ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ x ∈ Y, ∃ U f, S.arrows f ∧ x ∈ U}
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
⊢ ∃ U f, R.arrows f ∧ x ∈ U

Tactic:
rcases hR hf _ hU with ⟨V, g, hg, hV⟩

Goal state after:
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Sieve X
hS : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
R : Sieve X
hR : ∀ ⦃Y : Opens T⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | ∀ x ∈ Y, ∃ U f, S.arrows f ∧ x ∈ U}
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S.arrows f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : (Sieve.pullback f R).arrows g
hV : x ∈ V
⊢ ∃ U f, R.arrows f ∧ x ∈ U
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology = pretopology T

Tactic:
apply le_antisymm

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology ≤ pretopology T

case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ (grothendieckTopology T).toPretopology
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (pushforwardEq h ℱ).hom.app U = ℱ.map (eqToHom ⋯)

Tactic:
simp [pushforwardEq]

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

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

Tactic:
apply le_antisymm

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ iSup (coveringOfPresieve U R) ≤ U

case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ U ≤ 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
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
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
⊢ (ConcreteCategory.hom (f.hom.app (op (iSup U)))) s = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t

Tactic:
refine eq_of_locally_eq G U _ _ (fun _ ↦ ?_)
  rw [← NatTrans.naturality_apply, h, ht, ← ConcreteCategory.comp_apply, ← Functor.map_comp]
  rfl

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
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
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app (op U)))

Tactic:
conv at hsurj =>
    enter [t]
    rw [Subtype.forall' (p := (· ∈ U))]
  intro t
  -- We use the axiom of choice to pick around each point `x` an open neighborhood `V` and a
  -- preimage under `f` on `V`.
  choose V mV iVU sf heq using hsurj t
  -- These neighborhoods clearly cover all of `U`.
  have V_cover : U ≤ iSup V := by
    intro x hxU
    simp only [Opens.mem_iSup]
    exact ⟨⟨x, hxU⟩, mV ⟨x, hxU⟩⟩
  suffices IsCompatible F.obj V sf by
    -- Since `F` is a sheaf, we can glue all the local preimages together to get a global preimage.
    obtain ⟨s, s_spec, -⟩ := F.existsUnique_gluing' V U iVU V_cover sf this
    · use s
      apply G.eq_of_locally_eq' V U iVU V_cover
      intro x
      rw [← ConcreteCategory.comp_apply, ← f.1.naturality, ConcreteCategory.comp_apply, s_spec, heq]
  intro x y
  -- What's left to show here is that the sections `sf` are compatible, i.e. they agree on
  -- the intersections `V x ⊓ V y`. We prove this by showing that all germs are equal.
  apply section_ext
  intro z hz
  -- Here, we need to use injectivity of the stalk maps.
  apply hinj z ((iVU x).le ((inf_le_left : V x ⊓ V y ≤ V x) hz))
  rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply]
  simp_rw [← ConcreteCategory.comp_apply, f.1.naturality, ConcreteCategory.comp_apply, heq,
    ← ConcreteCategory.comp_apply, ← G.1.map_comp]
  rfl

Goal state after:
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
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M →L[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
by
  simp only [ContinuousLinearMap.ext_iff, pi_apply, funext_iff]
  exact forall_comm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ IsModuleTopology R R

Tactic:
by
  /- By a previous lemma it suffices to show that the identity from (R,usual) to
  (R, module topology) is continuous. -/
  apply of_continuous_id
  /-
  The idea needed here is to rewrite the identity function as the composite of `r ↦ (r,1)`
  from `R` to `R × R`, and multiplication `R × R → R`.
  -/
  rw [show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp]
  /-
  It thus suffices to show that each of these maps are continuous. For this claim to even make
  sense, we need to topologise `R × R`. The trick is to do this by giving the first `R` the usual
  topology `τR` and the second `R` the module topology. To do this we have to "fight mathlib"
  a bit with `@`, because there is more than one topology on `R` here.
  -/
  apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R))
      (moduleTopology R R)
  · /-
    The map R × R → R is `•`, so by a fundamental property of the module topology,
    this is continuous. -/
    exact @continuous_smul _ _ _ _ (moduleTopology R R) <| ModuleTopology.continuousSMul ..
  · /-
    The map `R → R × R` sending `r` to `(r,1)` is a map into a product, so it suffices to show
    that each of the two factors is continuous. But the first is the identity function
    on `(R, usual topology)` and the second is a constant function. -/
    exact @Continuous.prodMk _ _ _ _ (moduleTopology R R) _ _ _ continuous_id <|
      @continuous_const _ _ _ (moduleTopology R R) _

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

Goal state before:
pp: case refine_2
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 ⇑φ
⊢ ContinuousAdd B'

Tactic:
apply ContinuousAdd.mk

Goal state after:
case refine_2
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' := ⋯
hφo : IsOpenQuotientMap ⇑φ
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ) inst✝³] fun p ↦ p.1 + p.2
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ IsIso ((forget₂ (TopModuleCat R) TopCat).map F)

Tactic:
TopCat.isIso_iff_isHomeomorph,

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ IsHomeomorph ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F))
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.trans
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝² y✝ x y z : Prequotient F
x✝¹ : Relation F x y
x✝ : Relation F y z
h₁ : descFunLift F s x = descFunLift F s y
h₂ : descFunLift F s y = descFunLift F s z
⊢ descFunLift F s x = descFunLift F s z

Tactic:
| trans x y z _ _ h₁ h₂ =>

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

Goal state before:
pp: case pos
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ True ≠ f (eqToHom ⋯ ≫ Hom.snd b)

Tactic:
conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]

Goal state after:
case pos
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ True ≠ False
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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ piScalarRightHom R S N ι ∘ₗ piScalarRightInv R S N ι = LinearMap.id

Tactic:
ext i x j

Goal state after:
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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : N
j : ι
⊢ ((piScalarRightHom R S N ι ∘ₗ piScalarRightInv R S N ι) ∘ₗ single S (fun i ↦ N) i) x j =
    (LinearMap.id ∘ₗ single S (fun i ↦ N) i) x j
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : MvPolynomial (Fin n) ↑R →ₐ[↑R] ↑S
h₁ : Function.Surjective ⇑π
h₂ : (ker π.toRingHom).FG
⊢ iP ≫ CommRingCat.ofHom ↑π = f

Tactic:
by ext1; exact π.comp_algebraMap

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ Limits.HasFiniteProducts ((toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
by
  refine ⟨fun n ↦ ⟨fun D ↦ ?_⟩⟩
  have := hQp.createsFiniteProductsForget hQi R
  exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)

Goal state after:
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
g : ↑a ∈ IsLocalRing.maximalIdeal R
a_cast_zero : (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)) ↑a = 0
⊢ False

Tactic:
map_natCast

Goal state after:
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
g : ↑a ∈ IsLocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
⊢ False
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ Algebra ℚ R

Tactic:
rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : Nonempty (Algebra ℚ R)
⊢ Algebra ℚ R
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s.get? 0 = (cons x s.tail).get? 0

Tactic:
simp only [get?_cons_zero, get?_cons_succ, get?_tail]

Goal state after:
case zero
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s.get? 0 = some x
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case succ
α : Type u
s : Seq α
x : α
h : s.head = some x
n✝ : ℕ
⊢ s.get? (n✝ + 1) = (cons x s.tail).get? (n✝ + 1)

Tactic:
simp only [get?_cons_zero, get?_cons_succ, get?_tail]

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

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n + 1).succ.succ = s₂.get n.succ

Tactic:
rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons,
      get_interleave_right n (tail s₁) (tail s₂)]

Goal state after:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₂.tail.get n = s₂.get n.succ
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:
by
    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
s : Stream' α
n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ (take (n✝ + 1) s)[0]? = some (s.get 0)

Tactic:
simp only [length_take, zero_lt_succ, List.getElem?_eq_getElem]

Goal state after:
α : Type u
s : Stream' α
n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ some (take (n✝ + 1) s)[0] = some (s.get 0)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length = s.length + 1

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length ≤ s.length + 1

case a
α : Type u
s : Computation α
h : s.Terminates
⊢ s.length + 1 ≤ s.think.length
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ s.length' = ↑(s.length h)

Tactic:
simp [length', h]

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

Goal state before:
pp: α : Type u
s : Seq α
h : ¬s.Terminates
⊢ s.length' = ⊤

Tactic:
simp [length', h]

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

Goal state before:
pp: case inl
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
h✝ : k < m
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

pp: case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
hk : m ≤ k
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k

Tactic:
· rw [get_drop, get_append_left, get_append_left, List.getElem_drop]; simpa [hm]

Goal state after:
case inr
α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
k : ℕ
hk : m ≤ k
⊢ (drop n (x ++ₛ a)).get k = (List.drop n x ++ₛ a).get k
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.pure
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : (f a).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
exact ⟨_, _, n + 1, results_pure _, h, rfl⟩

Goal state after: