mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Algebra.IsPushout R R' S S'

Tactic:
refine Algebra.IsPushout.of_equiv e' ?_

Goal state after:
R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S)) = algebraMap S S'
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
⊢ Subring.closure (Set.range ⇑(ConcreteCategory.hom a) ∪ Set.range ⇑(ConcreteCategory.hom b)) = ⊤

Tactic:
algebraize [f.hom, g.hom]
  let e := ((isPushout_tensorProduct R A B).isoIsPushout A B H).commRingCatIsoToRingEquiv
  rw [← Subring.comap_map_eq_self_of_injective e.symm.injective (.closure _), RingHom.map_closure,
    ← top_le_iff, ← Subring.map_le_iff_le_comap, Set.image_union]
  simp only [AlgHom.toRingHom_eq_coe, ← Set.range_comp, ← RingHom.coe_comp]
  rw [← hom_comp, ← hom_comp, IsPushout.inl_isoIsPushout_inv, IsPushout.inr_isoIsPushout_inv,
    hom_ofHom, hom_ofHom]
  exact le_top.trans (Algebra.TensorProduct.closure_range_union_range_eq_top R A B).ge

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

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
x : ↑(limit.cone (cospan f g)).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)
⊢ (ConcreteCategory.hom ((cospan f g).map (𝟙 none))) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app none)) x) =
    (ConcreteCategory.hom ((cospan f g).map Hom.inl)) ((ConcreteCategory.hom ((limit.cone (cospan f g)).π.app left)) x)

Tactic:
simp; rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
h : P ≤ Q
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure

Tactic:
obtain ⟨R, _, hR⟩ := EssentiallySmall.exists_small_le' Q
    exact ⟨R, inferInstance, h.trans hR⟩

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (F.map (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst).hom))
      ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).snd =
    (unop X).snd

Tactic:
simp; rfl

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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| eqToHom ⋯ ≫ (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
enter [

Goal state after:
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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| eqToHom ⋯ ≫ (F.map (𝟙 Z)).toFunctor.map (eqToHom ⋯) ≫ eqToHom ⋯
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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| eqToHom ⋯ ≫ eqToHom ⋯

Tactic:
eqToHom_trans

Goal state after:
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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
| eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: case w_fiber
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)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ eqToHom ⋯ ≫ { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }.fiber =
    (({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
        { base := eqToHom ⋯, fiber := eqToHom ⋯ }).fiber

Tactic:
simp only [Grothendieck.ι_obj, eqToHom_refl,
        Grothendieck.comp_base, Category.comp_id, Grothendieck.comp_fiber, Functor.map_id]
      conv_rhs => enter [2, 1]; rw [eqToHom_map (F.map (𝟙 Z)).toFunctor]
      conv_rhs => rw [eqToHom_trans, eqToHom_trans]

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber

Tactic:
dsimp [comp, id]
      rw [← NatIso.naturality_2 ((Cat.Hom.toNatIso <| eqToIso (F.map_id Y.base)) ≪≫
        (eqToIso Cat.Hom.id_toFunctor)) f.fiber]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ eqToHom ⋯ ≫
      ({ base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ } ≫
          { base := e₁.hom, fiber := e₂.hom }).fiber =
    (𝟙 Y).fiber

Tactic:
have := Functor.congr_hom congr($((F.mapIso e₁).inv_hom_id).toFunctor) e₂.inv

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
this :
  ((F.mapIso e₁).inv ≫ (F.mapIso e₁).hom).toFunctor.map e₂.inv =
    eqToHom ⋯ ≫ (𝟙 (F.obj Y.base)).toFunctor.map e₂.inv ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫
      ({ base := e₁.inv, fiber := (F.map e₁.inv).toFunctor.map e₂.inv ≫ eqToHom ⋯ } ≫
          { base := e₁.hom, fiber := e₂.hom }).fiber =
    (𝟙 Y).fiber
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_4
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)
⊢ ∀ (x y : MvPolynomial (Fin n) A),
    x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) →
      y ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) →
        x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid →
          y ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid →
            x * y ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
intro x₁ x₂ _ _ h₁ h₂
        obtain ⟨_, ⟨p₁, rfl⟩, q₁, hq₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
        obtain ⟨_, ⟨p₂, rfl⟩, q₂, hq₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
        rw [add_mul, mul_add, add_assoc, ← map_mul]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · refine add_mem (Ideal.mul_mem_left _ _ hq₂) (Ideal.mul_mem_right _ _ hq₁)

Goal state after:
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 : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
s : Cocone (F ⋙ G)
j : C
⊢ G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j

Tactic:
apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j :)
  · intro j₁ j₂ k₁ k₂ f w h
    rw [← w]
    rw [← s.w f] at h
    simpa using! h
  · intro j₁ j₂ k₁ k₂ f w h
    rw [← w] at h
    rw [← s.w f]
    simpa using! h
  · exact s.w (𝟙 _)

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
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)
x : RXm
⊢ (eval₂Hom (algebraMap R A) fun i ↦ f' (MvPolynomial.X i)) x = f' x

Tactic:
← aeval_eq_eval₂Hom,

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)
x : RXm
⊢ (MvPolynomial.aeval fun i ↦ f' (MvPolynomial.X i)) x = f' x
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ hG.hom ≫ (lift F M hM).map PUnit.unit = G.map PUnit.unit ≫ h.hom.app Y

Tactic:
erw [← Iso.eq_inv_comp, ← Category.assoc, hh]

Goal state after:
case star.of.unit
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
G : WithInitial C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), hG.symm.hom ≫ G.map (starInitial.to (incl.obj x)) = M x ≫ h.symm.hom.app x
Y : C
⊢ (lift F M hM).map PUnit.unit = (M Y ≫ h.symm.hom.app Y) ≫ h.hom.app Y
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ IsLimit c.op → IsColimit c

Tactic:
intro h
    exact (IsColimit.equivIsoColimit c.opUnopIso).toFun (((IsLimit.postcomposeHomEquiv _ _).invFun
      ((IsLimit.whiskerEquivalenceEquiv walkingParallelPairOpEquiv.symm).toFun h)).unop)

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
⊢ (ker f).FG

Tactic:
have : ker f = ⊥ := by rw [← RingHom.injective_iff_ker_eq_bot]; exact hf.1
    rw [this]
    exact Submodule.fg_bot

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ m ≫ pullback.snd f (a₁ ≫ g) =
    pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      pullback.snd f (a₁ ≫ g)

Tactic:
apply PullbackCone.IsLimit.hom_ext h.isLimit

Goal state after:
case h₁.h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ (m ≫ pullback.snd f (a₁ ≫ g)) ≫ (IsPullback.cone h).fst =
    (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        pullback.snd f (a₁ ≫ g)) ≫
      (IsPullback.cone h).fst

case h₁.h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
m : s.pt ⟶ pullback f (a₁ ≫ g)
hm :
  ∀ (j : WalkingCospan),
    m ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
                (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).π.app
          j =
      s.π.app j
⊢ (m ≫ pullback.snd f (a₁ ≫ g)) ≫ (IsPullback.cone h).snd =
    (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        pullback.snd f (a₁ ≫ g)) ≫
      (IsPullback.cone h).snd
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F

Tactic:
refine ⟨fun {K} ↦ ?_⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ PreservesLimit K F
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
⊢ (b : Fin (n + 1)) → f b ⟶ c₂.pt

Tactic:
refine Fin.cases ?_ ?_
      · apply c₂.inl
      · intro i
        apply c₁.ι.app ⟨i⟩ ≫ c₂.inr

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ ≫ f' =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ g ≫ i₃

Tactic:
e₂,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ ≫ f' =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ ≫ g'
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ (A.binaryCofan B).inr ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) = g

Tactic:
ext1; exact lift_comp_includeRight _ _ fun _ _ ↦ .all _ _

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ ι ≫ ι = 𝟙 A

Tactic:
apply lift_left_mul_ext ι[A]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ lift (ι ≫ ι) ι ≫ μ = lift (𝟙 A) ι ≫ μ
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 : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

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 : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0

Tactic:
· intro q _ q_ne
    simp [h.eval_of_ne q_ne.symm, smul_eq_mul]

Goal state after:
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 : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_1
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
hst : Disjoint s (sec '' t)
⊢ #↑s + #↑(sec '' t) = Module.rank R M

Tactic:
Cardinal.mk_image_eq,

Goal state after:
case refine_1
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
hst : Disjoint s (sec '' t)
⊢ #↑s + #↑t = Module.rank R M

case refine_1
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
hst : Disjoint s (sec '' t)
⊢ Injective sec
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ X Xᘁ ⊗≫ f ▷ Xᘁ ⊗≫ (η_ Y Yᘁ ▷ Y ⊗≫ Y ◁ ε_ Y Yᘁ) ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ) = η_ X Xᘁ ≫ f ▷ Xᘁ ≫ g ▷ Xᘁ

Tactic:
rw [evaluation_coevaluation'']; monoidal

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
s t : Submodule R M
| Module.rank R ↥s + Module.rank R ↥t

Tactic:
enter [

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
s t : Submodule R M
| Module.rank R ↥s + Module.rank R ↥t
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ (∀ (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      opEquiv.mapMatrix.symm (opEquiv.mapMatrix a_1 * opEquiv.mapMatrix a) = opEquiv.mapMatrix.symm 1 → m ≤ n) ↔
    ∀ (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
refine forall_comm.trans <| .trans (forall_congr' ?_) (transposeAddEquiv ..).forall_congr_right

Goal state after:
R : Type u_1
inst✝ : Semiring R
n m : ℕ
⊢ ∀ (a : Matrix (Fin m) (Fin n) R),
    (∀ (a_1 : Matrix (Fin n) (Fin m) R),
        opEquiv.mapMatrix.symm (opEquiv.mapMatrix a * opEquiv.mapMatrix a_1) = opEquiv.mapMatrix.symm 1 → m ≤ n) ↔
      ∀ (g : Matrix (Fin m) (Fin n) R), g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv a = 1 → m ≤ n
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : HasRankNullity.{u, u_2} R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Module.Finite R M
S : Type u_1
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
N : Submodule S M
⊢ finrank R (M ⧸ N) = finrank R M - finrank R ↥N

Tactic:
by
  rw [← (N.restrictScalars R).finrank_quotient_add_finrank]
  exact Nat.eq_sub_of_add_eq rfl

Goal state after: