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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₀ : Type u_3
inst✝³ : SMul R₀ R
inst✝² : SMul R₀ M
inst✝¹ : IsScalarTower R₀ R R
inst✝ : IsScalarTower R₀ R M
r : R₀
m : M
s : ↥S
⊢ r • mk m s = mk (r • m) s

Tactic:
rw [OreLocalization.smul_oreDiv]
  simp

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd {a} * Multiplicative.ofAdd m) =
    of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)

Tactic:
of,

Goal state after:
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd {a} * Multiplicative.ofAdd m) =
    FreeAbelianGroup.of (Multiplicative.ofAdd {a}) * FreeAbelianGroup.of (Multiplicative.ofAdd m)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x y : Multiplicative (Multiset α)
⊢ (Multiset.map f (Multiplicative.toAdd (x * y))).prod = (Multiset.map f x + Multiset.map f y).prod

Tactic:
rw [← Multiset.map_add]

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f✝ f : α → R
x y : Multiplicative (Multiset α)
⊢ (Multiset.map f (Multiplicative.toAdd (x * y))).prod = (Multiset.map f (x + y)).prod
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ (↑c * ↑s * ↑s' * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    (↑c * ↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * ↑s' * r) • m

Tactic:
mul_comm _ (s' : R),

Goal state after:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ (↑s' * (↑c * ↑s) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    (↑s' * (↑c * ↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2) * r) • m
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
s : Set α
hfs : s.Finite
hxs : x.IsSupported s
⊢ x.IsSupported ↑hfs.toFinset

Tactic:
by rwa [Set.Finite.coe_toFinset]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
K : J ⥤ C
E : C ⥤ D
inst✝¹ : E.IsEquivalence
inst✝ : HasColimit (K ⋙ E)
⊢ HasColimit K

Tactic:
rw [hasColimit_iff_of_iso
    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
K : J ⥤ C
E : C ⥤ D
inst✝¹ : E.IsEquivalence
inst✝ : HasColimit (K ⋙ E)
⊢ HasColimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ (adj.homEquiv (K.obj j) (((const J).obj Y).obj j')).symm (K.map f ≫ t.app j') =
    (adj.homEquiv (K.obj j) Y).symm (t.app j) ≫ ((const J).obj Y).map f

Tactic:
← adj.homEquiv_naturality_right_symm,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ (adj.homEquiv (K.obj j) (((const J).obj Y).obj j')).symm (K.map f ≫ t.app j') =
    (adj.homEquiv (K.obj j) (((const J).obj Y).obj j')).symm (t.app j ≫ G.map (((const J).obj Y).map f))
Module: Mathlib.CategoryTheory.Adjunction.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj (F.op.obj X))).map f ≫ (adj.homEquiv (unop X) (K.obj j')).symm (t.app j') =
    (adj.homEquiv (unop X) (K.obj j)).symm (t.app j) ≫ K.map f

Tactic:
← adj.homEquiv_naturality_right_symm,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ (unop ((const J).op.obj (F.op.obj X))).map f ≫ (adj.homEquiv (unop X) (K.obj j')).symm (t.app j') =
    (adj.homEquiv (unop X) (K.obj j')).symm (t.app j ≫ G.map (K.map f))
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case eq
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ofHom (algebraMap R A) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
ext r
    trans algebraMap R (A ⊗[R] B) r
    · exact Algebra.TensorProduct.includeLeft.commutes (R := R) r
    · exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm

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_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : AddCommMonoid M''
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
inst✝¹¹ : Module A M'
inst✝¹⁰ : IsLocalization S A
inst✝⁹ : Module R M
inst✝⁸ : Module R M'
inst✝⁷ : Module R M''
inst✝⁶ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ : M →ₗ[R] M''
inst✝⁵ : IsLocalizedModule S f
N : Type ?u.59
N' : Type ?u.61
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
r : R
h : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (r • h)) ⋯ = (RingHom.id R) r • lift S f (g ∘ₗ h) ⋯

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)
    simp only [lift_comp, LinearMap.smul_comp, LinearMap.comp_smul, RingHom.id_apply]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (ofObj X).op Z ↔ ofObj (fun i ↦ op (X i)) Z

Tactic:
simp only [op_iff, ofObj_iff]

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
⊢ (∃ i, X i = unop Z) ↔ ∃ i, op (X i) = Z
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: J : Type v
F : J → Type (max v u)
x✝¹ : Cone (Discrete.functor F)
x✝ :
  x✝¹.pt ⟶
    { pt := (j : J) → F j,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => ↾fun f ↦ f j }.pt
w :
  ∀ (j : Discrete J),
    x✝ ≫
        { pt := (j : J) → F j,
                π :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => ↾fun f ↦ f j }.π.app
          j =
      x✝¹.π.app j
⊢ x✝ = ↾fun x j ↦ (ConcreteCategory.hom (x✝¹.π.app { as := j })) x

Tactic:
ext x j

Goal state after:
J : Type v
F : J → Type (max v u)
x✝¹ : Cone (Discrete.functor F)
x✝ :
  x✝¹.pt ⟶
    { pt := (j : J) → F j,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => ↾fun f ↦ f j }.pt
w :
  ∀ (j : Discrete J),
    x✝ ≫
        { pt := (j : J) → F j,
                π :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => ↾fun f ↦ f j }.π.app
          j =
      x✝¹.π.app j
x : x✝¹.pt
j : J
⊢ (ConcreteCategory.hom x✝).toFun x j =
    (ConcreteCategory.hom (↾fun x j ↦ (ConcreteCategory.hom (x✝¹.π.app { as := j })) x)).toFun x j
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
⊢ (CostructuredArrow.toOver P F X).Full

Tactic:
by
  constructor
  intro A B f
  refine ⟨CostructuredArrow.homMk (F.preimage f.left) trivial ?_, ?_⟩
  · simpa using f.w
  · ext; simp

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1.inr
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
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
apply AddSubmonoid.mem_sup_left
          exact ⟨X i, map_X _ _⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ (fiberwiseColimit X✝).map f ≫ colim.map ((Grothendieck.ι F c₂).whiskerLeft α) =
    colim.map ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y✝).map f

Tactic:
apply colimit.hom_ext; simp

Goal state after:
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
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
obtain ⟨m, f', hf', s, hs⟩ := FinitePresentation.out (R := R) (A := A)

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
⊢ (RingHom.ker f.toRingHom).FG
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : U.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : U.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ P V

Tactic:
obtain ⟨W, q₃, q₄, hq'⟩ := IsFiltered.span q₁ h.right

Goal state after:
case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : U.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : U.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
W : C
q₃ : Z ⟶ W
q₄ : V.right ⟶ W
hq' : q₁ ≫ q₃ = StructuredArrow.Hom.right h ≫ q₄
⊢ P V
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝¹ : Algebra.FinitePresentation B C
algebraizeInst✝ : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation

Tactic:
exact Algebra.FinitePresentation.trans A B C

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

Goal state before:
pp: case e_6.e_8.e_7
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F✝ : D ⥤ Cat
G✝ : C✝ ⥤ D
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
inst✝ : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₂
X✝ Y✝ : C
f : X✝ ⟶ Y✝
d : ↑(F.obj X✝)
this : (α.app Y✝).toFunctor.obj ((F.map f).toFunctor.obj d) = (G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d)
⊢ eqToHom ⋯ ≍ 𝟙 ((G.map f).toFunctor.obj ((α.app X✝).toFunctor.obj d))

Tactic:
apply eqToHom_heq_id_dom

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

Goal state before:
pp: C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₁
⊢ IsIso (colimit.pre H (map α))

Tactic:
let i := (colimitFiberwiseColimitIso _).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso _

Goal state after:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
⊢ IsIso (colimit.pre H (map α))
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ (P.strictLimitsOfShape J).isoClosure = P.limitsOfShape J

Tactic:
refine le_antisymm ?_ ?_
  · rw [isoClosure_le_iff]
    apply strictLimitsOfShape_le_limitsOfShape
  · intro X ⟨h⟩
    have := h.hasLimit
    exact ⟨limit h.diag, strictLimitsOfShape.limit h.diag h.prop_diag_obj,
      ⟨h.isLimit.conePointUniqueUpToIso (limit.isLimit _)⟩⟩

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
⊢ P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal

Tactic:
refine ⟨fun hP X Y f hf ↦ ?_, fun hP ↦ ⟨fun {Y X S} g f hf hcomp ↦ ?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : P.HasOfPostcompProperty Q
X Y : C
f : X ⟶ Y
hf : Q f
⊢ P.diagonal f

case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
⊢ P g
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) μ ≫ μ) ≫ μ

Tactic:
← Category.id_comp μ

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (fst A A ≫ ι) (𝟙 (A ⊗ A) ≫ μ) ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ (ι ⊗ₘ ι) ≫ μ = (β_ A A).hom ≫ μ ≫ ι

Tactic:
mul_inv A,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ (ι ⊗ₘ ι) ≫ μ = (β_ A A).hom ≫ (β_ A A).hom ≫ (ι ⊗ₘ ι) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A Y Y' : C
inst✝ : Closed A
g : Y ⟶ Y'
⊢ curry (uncurry ((ihom A).map g)) = curry ((ihom.ev A).app Y ≫ g)

Tactic:
rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_comp]

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

Goal state before:
pp: case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i q : ι
a✝ : l q ≠ 0
q_ne : q ≠ i
⊢ (ε i) (l q • e q) = 0

Tactic:
simp [h.eval_of_ne q_ne.symm, smul_eq_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ x = 0

Tactic:
← hsec x,

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ (span R s).mkQ (sec x) = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ finrank K ↥p + finrank K ↥(K ∙ v) = finrank K ↥p + 1 + finrank K ↥(p ⊓ K ∙ v)

Tactic:
add_assoc,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ finrank K ↥p + finrank K ↥(K ∙ v) = finrank K ↥p + (1 + finrank K ↥(p ⊓ K ∙ v))
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : ↥p ≃ₗ[K] ↥q
f₂ : V ≃ₗ[K] V₂
⊢ finrank K (V ⧸ p) = finrank K (V₂ ⧸ q)

Tactic:
by
      rw [← @add_right_cancel_iff _ _ _ (finrank K p), Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₁, Submodule.finrank_quotient_add_finrank,
        LinearEquiv.finrank_eq f₂]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
f : M ≃ M
hf : IsOrthogonal B ⇑f
x y : M
⊢ (B (f x)) y = (B x) (f.symm y)

Tactic:
simpa using hf x (f.symm y)

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B (f (x + y))) (f (x + y)) = (B (x + y)) (x + y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
simp only [map_add, LinearMap.add_apply, hf x, hf y, show B y x = B x y from hB.eq y x] at this

Goal state after:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f y)) (f x) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

pp: case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ ?refine_1 ≫ G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
    ?refine_2 ≫ G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))

Tactic:
· exact c.π.app WalkingParallelPair.zero

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.π.app WalkingParallelPair.zero ≫
      G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)) =
    ?refine_2 ≫ G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))