mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : ↥S
e : s • x = f m
⊢ ∃ a, Function.uncurry (mk' f) a = x

Tactic:
exact ⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩

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

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
⊢ ∀ (m : (A.coproductCocone B).pt ⟶ s.pt),
    (∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ m = s.ι.app j) →
      m = ofHom (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯).toRingHom

Tactic:
rintro ⟨m : A ⊗[ℤ] B →+* s.pt⟩ hm
    apply CommRingCat.hom_ext
    apply RingHom.toIntAlgHom_injective
    apply Algebra.TensorProduct.liftEquiv.symm.injective
    apply Subtype.ext
    rw [Algebra.TensorProduct.liftEquiv_symm_apply_coe, Prod.mk.injEq]
    constructor
    · ext a
      simp [map_one, mul_one, ← hm (Discrete.mk WalkingPair.left)]
    · ext b
      simp [map_one, ← hm (Discrete.mk WalkingPair.right)]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = LocalizedModule.mk (g m) s
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
simpa [map, lift, iso_localizedModule_eq_refl S M₀]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_1.refine_2
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ (binaryProductFunctor.obj X).map x✝ ≫
      ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom =
    ((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
      (prod.functor.obj X).map x✝

Tactic:
apply Limits.prod.hom_ext

Goal state after:
case refine_1.refine_2.h₁
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.fst =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.fst

case h₂
X X✝ Y✝ : Type u
x✝ : X✝ ⟶ Y✝
⊢ ((binaryProductFunctor.obj X).map x✝ ≫
        ((limit.isLimit (pair X Y✝)).conePointUniqueUpToIso (binaryProductLimit X Y✝)).symm.hom) ≫
      prod.snd =
    (((limit.isLimit (pair X X✝)).conePointUniqueUpToIso (binaryProductLimit X X✝)).symm.hom ≫
        (prod.functor.obj X).map x✝) ≫
      prod.snd
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: case refine_2
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
          (NatIso.ofComponents
              (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm) ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
              ⋯).hom ≫
          prod.functor.map x✝¹).app
      x✝

Tactic:
apply Limits.prod.hom_ext

Goal state after:
case refine_2.h₁
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.fst =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.fst

case h₂
X✝ Y✝ : Type u
x✝¹ : X✝ ⟶ Y✝
x✝ : Type u
⊢ (binaryProductFunctor.map x✝¹ ≫
            (NatIso.ofComponents
                (fun Y ↦ ((limit.isLimit (pair Y✝ Y)).conePointUniqueUpToIso (binaryProductLimit Y✝ Y)).symm)
                ⋯).hom).app
        x✝ ≫
      prod.snd =
    ((NatIso.ofComponents (fun Y ↦ ((limit.isLimit (pair X✝ Y)).conePointUniqueUpToIso (binaryProductLimit X✝ Y)).symm)
                ⋯).hom ≫
            prod.functor.map x✝¹).app
        x✝ ≫
      prod.snd
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case intro.refine_2
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (RingHom.ker (MvPolynomial.mapAlgHom f).toRingHom).FG

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
case intro.refine_2
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (RingHom.ker ↑(MvPolynomial.mapAlgHom f)).FG
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
X Y : Grothendieck F
f : X ⟶ Y
⊢ (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯

Tactic:
simp only [map_map, map_obj_base, map_obj_fiber, NatTrans.comp_app, Cat.Hom.comp_toFunctor,
      comp_obj, Cat.Hom₂.eqToHom_toNatTrans, eqToHom_app, Functor.comp_map, eqToHom_refl, map_comp,
      eqToHom_map, eqToHom_trans_assoc, Category.comp_id, Category.id_comp]

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

Goal state before:
pp: C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
      ((prod.functor.obj X).mapCone c).π.app j =
    s.π.app j

Tactic:
apply Limits.prod.hom_ext

Goal state after:
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.fst =
    s.π.app j ≫ prod.fst

case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.snd =
    s.π.app j ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s))

Tactic:
apply Limits.prod.hom_ext

Goal state after:
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m ≫ prod.fst = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫ prod.fst

case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m ≫ prod.snd = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫ prod.snd
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
refine ⟨Finset.univ.image g' ∪ s.image aeval_h, ?_⟩

Goal state after:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
⊢ Ideal.span ↑(Finset.image g' Finset.univ ∪ Finset.image (⇑aeval_h) s) = RingHom.ker f.toRingHom
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inl
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
i : Fin n
⊢ g' i ∈ ↑(RingHom.ker f.toRingHom)

Tactic:
change f (g' i) = 0

Goal state after:
case inl
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
i : Fin n
⊢ f (g' i) = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
⊢ ∀ (Y_1 X_1 : C) (z : Y_1 ⟶ X_1), Epi z → ∀ (v : Y_1 ⟶ X) (u : X_1 ⟶ Y) (sq : CommSq v z f u), sq.HasLift

Tactic:
intro A B z hz u v sq

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ sq.HasLift
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap f.toRingHom ⊥ = Ideal.map g.toRingHom (Ideal.comap (f.comp g).toRingHom ⊥)

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap ↑(f.comp g) ⊥)
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
⊢ (StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).hom ≫
      (pre F G).map { base := StructuredArrow.Hom.right g, fiber := eqToHom ⋯ } =
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).hom

Tactic:
by
      simp only [StructuredArrow.mk_right]
      generalize_proofs
      apply Grothendieck.ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P

Tactic:
by
  constructor
  · intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩
    exact of_isPullback h₂ h₁
  · intro h
    constructor
    intro _ _ _ _ _ _ _ _ h₁ h₂
    exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra ↑R ↑T := (CommRingCat.Hom.hom g).toAlgebra
⊢ P
    ((CommRingCat.Hom.hom
          (colimit.isoColimitCocone
              { cocone := CommRingCat.pushoutCocone ↑R ↑S ↑T,
                isColimit := CommRingCat.pushoutCoconeIsColimit ↑R ↑S ↑T }).inv).comp
      (CommRingCat.Hom.hom
        ({ cocone := CommRingCat.pushoutCocone ↑R ↑S ↑T,
                  isColimit := CommRingCat.pushoutCoconeIsColimit ↑R ↑S ↑T }.cocone.ι.app
          WalkingSpan.left)))

Tactic:
hP'.cancel_right_isIso

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra ↑R ↑T := (CommRingCat.Hom.hom g).toAlgebra
⊢ P
    (CommRingCat.Hom.hom
      ({ cocone := CommRingCat.pushoutCocone ↑R ↑S ↑T,
                isColimit := CommRingCat.pushoutCoconeIsColimit ↑R ↑S ↑T }.cocone.ι.app
        WalkingSpan.left))
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i

Tactic:
Sigma.ext_iff,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : (g (h a) h₁).fst = (g r hx).fst ∧ (g (h a) h₁).snd ≍ (g r hx).snd
⊢ (h a).r ≫ (h a).i = r.r ≫ r.i
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g = f'
⊢ P (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g)

Tactic:
apply P.comp_mem _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : P.IsStableUnderComposition
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.universally f
hg : P.universally g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) ⋯ ≫ pullback.fst i₂ g = f'
⊢ P (pullback.lift f' (i₁ ≫ f) ⋯)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → P f') ∧
      ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → Q f'

Tactic:
← forall_and

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1), IsPullback x_4 x_2 x_3 f → P x_4 ∧ Q x_4
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom ≫ M ◁ μ ≫ μ = lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ

Tactic:
simp_rw [← Category.assoc]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ ((lift (lift f₁ f₂) f₃ ≫ (α_ M M M).hom) ≫ M ◁ μ) ≫ μ = (lift f₁ (lift f₂ f₃) ≫ M ◁ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_fst
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
A B : C
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ fst ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)

Tactic:
simp [CartesianMonoidalCategory.prodComparison, ← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case h_snd
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁶ : Category.{v₁, u₁} D
inst✝⁵ : CartesianMonoidalCategory D
F : C ⥤ D
A B : C
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (pair A B) F
inst✝¹ : PreservesLimit (pair A B) (F ⋙ G)
inst✝ : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ (prodComparisonIso (F ⋙ G) A B).hom ≫ snd ((F ⋙ G).obj A) ((F ⋙ G).obj B) =
    (G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)).hom ≫
      snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)

Tactic:
simp [CartesianMonoidalCategory.prodComparison, ← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
⊢ ε F = (preservesTerminalIso F).inv

Tactic:
by
  change (εIso F).symm.inv = _; congr; ext

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ ∑ i ∈ (ℛ R c).index, (toConv id).ofConv ((ℛ R c).left i) * (toConv (antipode R)).ofConv ((ℛ R c).right i) =
    (ofConv 1) c

Tactic:
simp [sum_mul_antipode_eq_algebraMap_counit (ℛ R c)]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, (f x • b.toDual (b x)) (b i) = f i

Tactic:
LinearMap.smul_apply,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ x ∈ f.support, f x • (b.toDual (b x)) (b i) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ d, (f (b d) • b.coord d) m = f m

Tactic:
LinearMap.smul_apply,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ ∑ x, f (b x) • (b.coord x) m = f m
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ d, (f d • b.dualBasis d) (b i) = f i

Tactic:
LinearMap.smul_apply,

Goal state after:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ x, f x • (b.dualBasis x) (b i) = f i