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

Goal state before:
pp: case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
s : Y ⟶ X
Z : Over X
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := Z.right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := Z.right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := Z.right, hom := s }
g : Z ⟶ { left := Y, right := Z.right, hom := s }
hg : ((Sieve.overEquiv { left := Y, right := Z.right, hom := s }).symm R).arrows g
⊢ (Sieve.overEquiv Z).symm (Sieve.pullback (Over.Hom.left g) S) ∈ (Precoverage.comap (Over.forget X) K).toGrothendieck Z

Tactic:
exact ih' hg Z.hom

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

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ ↑U
⊢ (ConcreteCategory.hom f) x ∈ ↑(hf.functor.obj ((map f).obj U))

Tactic:
exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
⊢ ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫ ((Opens.map f).op.lan.obj 𝒢).map j.hom =
    u.app j.left ≫
      ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom

Tactic:
have := NatTrans.congr_app ((Opens.map f).op.lanUnit.naturality u) j.left

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
this :
  ((𝟭 ((Opens ↑Y)ᵒᵖ ⥤ C)).map u ≫ (Opens.map f).op.lanUnit.app 𝒢).app j.left =
    ((Opens.map f).op.lanUnit.app ℱ ≫
          ((Opens.map f).op.lan ⋙ (whiskeringLeft (Opens ↑Y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (Opens.map f).op).map u).app
      j.left
⊢ ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫ ((Opens.map f).op.lan.obj 𝒢).map j.hom =
    u.app j.left ≫
      ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁵ : HasSheafify J AddCommGrpCat
inst✝⁴ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M N : SheafOfModules R
f : M ⟶ N
inst✝¹ : IsIso f
σ : M.QuasicoherentData
inst✝ : σ.IsFinitePresentation
i : (QuasicoherentData.ofIsIso f σ).I
⊢ (Presentation.ofIsIso (Hom.over f (σ.X i)) (σ.presentation i)).IsFinite

Tactic:
exact inferInstanceAs ((σ.presentation i).ofIsIso _).IsFinite

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 X
x : ↑X
⊢ ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) ⟶ F.stalk x

Tactic:
refine ?_ ≫ colimit.pre _ (OpenNhds.map f x).op

Goal state after:
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 X
x : ↑X
⊢ ((pushforward C f).obj F).stalk ((ConcreteCategory.hom f) x) ⟶
    colimit
      ((OpenNhds.map f x).op ⋙ ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
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
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ F.germ U ((ConcreteCategory.hom f) x) hU ≫ stalkPullbackHom C f F x ≫ stalkPullbackInv C f F x =
    F.germ U ((ConcreteCategory.hom f) x) hU ≫ 𝟙 (F.stalk ((ConcreteCategory.hom f) x))

Tactic:
germ_stalkPullbackHom_assoc,

Goal state after:
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
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op U) ≫
      ((pullback C f).obj F).germ ((Opens.map f).obj U) x hU ≫ stalkPullbackInv C f F x =
    F.germ U ((ConcreteCategory.hom f) x) hU ≫ 𝟙 (F.stalk ((ConcreteCategory.hom f) x))
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)
F : Presheaf C X
U V : Opens ↑X
x : ↑X
mU : x ∈ U
mV : x ∈ V
s : ToType (F.obj (op U))
t : ToType (F.obj (op V))
h : (ConcreteCategory.hom (F.germ U x mU)) s = (ConcreteCategory.hom (F.germ V x mV)) t
⊢ ∃ W, ∃ (_ : x ∈ W), ∃ iU iV, (ConcreteCategory.hom (F.map iU.op)) s = (ConcreteCategory.hom (F.map iV.op)) t

Tactic:
obtain ⟨W, iU, iV, e⟩ := (colimit.isColimit ((OpenNhds.inclusion x).op ⋙ F)).eq_iff.mp h
  exact ⟨(unop W).1, (unop W).2, iU.unop, iV.unop, e⟩

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

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

Tactic:
exact Continuous.comp hφo.continuous hA

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 ⇑φ
hA : Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 + p.2
hφ2 : (fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ = ⇑φ ∘ fun p ↦ p.1 + p.2
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ) inst✝³] (⇑φ ∘ fun p ↦ p.1 + p.2)

Tactic:
exact Continuous.comp hφo.continuous hA

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget MagmaCat).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toMagmaCatIso.isIso_hom

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

Goal state before:
pp: case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))

Tactic:
refine fun H ↦ ⟨fun {T} f g e ↦ ?_⟩

Goal state after:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
⊢ f = g
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
⊢ ∃! l, ∀ (j : J), ((Under.forget X).mapCocone c).ι.app j ≫ l = s.ι.app j

Tactic:
let s' : Cocone F := ⟨Under.mk ((F.obj i).hom ≫ s.ι.app i), fun j ↦ Under.homMk (s.ι.app j) (by
    obtain ⟨k, hik, hjk, -⟩ := IsFilteredOrEmpty.cocone_objs i j
    simp only [Functor.const_obj_obj, Under.mk_right, Under.mk_hom,
      ← s.w hjk, ← s.w hik]
    simp), fun j k e ↦ by ext; simpa using s.w e⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i : J
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i), ι := { app := fun j ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
⊢ ∃! l, ∀ (j : J), ((Under.forget X).mapCocone c).ι.app j ≫ l = s.ι.app j
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
j : ι
⊢ (piScalarRightHom R S N ι) (x ⊗ₜ[R] f) j = f j • x

Tactic:
simp [piScalarRightHom, piScalarRightHomBil]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
a : A
b : B
c : C
⊢ (prodRight R S A B C).symm (a ⊗ₜ[R] b, a ⊗ₜ[R] c) = a ⊗ₜ[R] (b, c)

Tactic:
apply (prodRight R S A B C).injective

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
a : A
b : B
c : C
⊢ (prodRight R S A B C) ((prodRight R S A B C).symm (a ⊗ₜ[R] b, a ⊗ₜ[R] c)) = (prodRight R S A B C) (a ⊗ₜ[R] (b, c))
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ coyoneda.obj (Opposite.op S)).obj i
f₂ : (F ⋙ coyoneda.obj (Opposite.op S)).obj j
e✝ :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) f₁ =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) f₂
k : J
hik : i ⟶ k
hjk : j ⟶ k
e : Under.Hom.right f₁ ≫ (F ⋙ Under.forget R).map hik = Under.Hom.right f₂ ≫ (F ⋙ Under.forget R).map hjk
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) f₁ =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) f₂

Tactic:
exact ⟨k, hik, hjk, Under.UnderMorphism.ext e⟩

Goal state after:
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 : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ ∀ (j : WalkingCospan),
    Over.Hom.left a.hom ≫ (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app j =
      (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app j

Tactic:
rintro (_ | _ | _)

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫ (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app none =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app none

case some.left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.left) =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.left)

case some.right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ Over.Hom.left a.hom ≫
      (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app (some WalkingPair.right) =
    (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app (some WalkingPair.right)
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:
rintro (_ | _ | _)

Goal state after:
case none
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₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app none ≫ Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app none

case some.left
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₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.left) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.left)

case some.right
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₂
⊢ (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯).ι.app (some WalkingPair.right) ≫
      Under.Hom.right a.hom =
    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯).ι.app (some WalkingPair.right)
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
⊢ Function.Injective ⇑(lTensor A g)

Tactic:
have hπ : Function.Surjective π := Finsupp.linearCombination_surjective _ Function.surjective_id

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type u_4
P : Type u_5
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
g : M →ₗ[R] N
hg : Function.Injective ⇑g
H : Function.Exact ⇑g ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
Q : Type (max u_1 u_6) := A →₀ R
π : Q →ₗ[R] A := Finsupp.linearCombination R fun a ↦ a
hπ : Function.Surjective ⇑π
⊢ Function.Injective ⇑(lTensor A g)
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : ↑(⟨x, hx⟩ * y) = ↑1
⊢ x⁻¹ ∈ S

Tactic:
S.coe_mul,

Goal state after:
case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : ↑⟨x, hx⟩ * ↑y = ↑1
⊢ x⁻¹ ∈ S
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
⊢ Function.Injective (map f)

Tactic:
by
  intro _ _ h
  rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
    (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
⊢ x ∈ lift (restrict h)

Tactic:
let y : E := ⟨x, h hx⟩
    exact (mem_lift y).2 ((mem_restrict h y).2 hx)

Goal state after:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ z • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p

Tactic:
rw [AddSubgroup.mem_zmultiples_iff]

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
i : ℕ
s : Stream' α
n✝ : ℕ
⊢ (drop i s).tail.get n✝ = (drop (i + 1) s).get n✝

Tactic:
simp [Nat.add_comm, Nat.add_left_comm]

Goal state after:
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')
s : Seq α
e : some a = ↑s 0
⊢ s.destruct = some (a, s.tail)

Tactic:
unfold destruct get? Functor.map

Goal state after:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' ↦ (a', s.tail)) (↑s 0) = some (a, s.tail)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ corec Stream'.cycleF Stream'.cycleG (a', a₁ :: l₁, a, l) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
corec_eq,

Goal state after:
case cons
α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
a₁ : α
l₁ : List α
ih :
  ∀ (a' : α),
    corec Stream'.cycleF Stream'.cycleG (a', l₁, a, l) = a' :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
a' : α
⊢ Stream'.cycleF (a', a₁ :: l₁, a, l) :: corec Stream'.cycleF Stream'.cycleG (Stream'.cycleG (a', a₁ :: l₁, a, l)) =
    a' :: a₁ :: l₁ ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.conts m = g.conts n

Tactic:
simp only [nth_cont_eq_succ_nth_contAux,
    contsAux_stable_of_terminated (Nat.pred_le_iff.mp n_le_m) terminatedAt_n]

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

Goal state before:
pp: α : Type u
a : α
c₂ : Computation α
⊢ (pure a <|> c₂).destruct = Sum.inl a

Tactic:
unfold_projs
    simp [orElse]

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

Goal state before:
pp: α : Type u
c₁ : Computation α
a : α
⊢ (c₁.think <|> pure a).destruct = Sum.inl a

Tactic:
unfold_projs
    simp [orElse]

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

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
⊢ (c₁.think <|> c₂.think).destruct = Sum.inr (c₁ <|> c₂)

Tactic:
unfold_projs
    simp [orElse]

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

Goal state before:
pp: α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a' ∈ t

Tactic:
rw [mem_unique ma h1]; exact h2

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix : (ringEquiv G f') ((of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i) x) = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
ringEquiv_of,

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix : ⟦⟨i, x⟩⟧ = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ Option.map (fun p ↦ { a := 1, b := ↑p.b }) ((IntFractPair.stream v).tail.get 0) =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
← Stream'.get_succ,

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ Option.map (fun p ↦ { a := 1, b := ↑p.b }) ((IntFractPair.stream v).get (Nat.succ 0)) =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
obtain ⟨pred_conts, pred_conts_eq⟩ := IH (n + 1) <| lt_add_one (n + 1)

Goal state after:
case succ.succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.degree ≤ 0

Tactic:
by
  simpa only [of_c_eq_zero ha hb hc] using degree_C_le

Goal state after: