mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this✝ : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
g' : MvPolynomial (Fin n) R →+* S := g.toRingHom
hg : Surjective ⇑g'
hg' : (ker g').FG
this : g'.comp MvPolynomial.C = f
⊢ Q R S f

Tactic:
clear_value g'

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this✝ : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
g' : MvPolynomial (Fin n) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : g'.comp MvPolynomial.C = f
⊢ Q R S f
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
m : (Cofork.ofπ f ⋯).pt ⟶ s.pt
w : (Cofork.ofπ f ⋯).π ≫ m = s.π
⊢ m = Cofork.IsColimit.desc r.isColimit s.π ⋯

Tactic:
· apply Cofork.IsColimit.hom_ext r.isColimit
    exact w.trans (Cofork.IsColimit.π_desc' r.isColimit _ _).symm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l ≫ (IsPullback.cone h).fst = 𝟙 X
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f

Tactic:
IsPullback.cone_fst,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l ≫ a = 𝟙 X
h₂ : l ≫ (IsPullback.cone h).snd = 𝟙 X
⊢ Mono f
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f
⊢ l' ≫ (IsPullback.cone h).fst = l' ≫ (IsPullback.cone h).snd

Tactic:
IsPullback.cone_fst,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
l' : Z ⟶ (IsPullback.cone h).pt
e : (l' ≫ (IsPullback.cone h).fst) ≫ f = (l' ≫ (IsPullback.cone h).snd) ≫ f
⊢ l' ≫ a = l' ≫ (IsPullback.cone h).snd
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case left.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P f

pp: case left.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P e.toRingHom

Tactic:
exacts [H, hP' e]

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S R' S' : CommRingCat
f : R ⟶ S
g : R ⟶ R'
f' : R' ⟶ S'
g' : S ⟶ S'
hsq : IsPushout g f f' g'
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f
algInst✝⁴ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑R ↑R' := (CommRingCat.Hom.hom g).toAlgebra
algInst✝² : Algebra ↑R' ↑S' := (CommRingCat.Hom.hom f').toAlgebra
algInst✝¹ : Algebra ↑S ↑S' := (CommRingCat.Hom.hom g').toAlgebra
algInst✝ : Algebra ↑R ↑S' := ((CommRingCat.Hom.hom f').comp (CommRingCat.Hom.hom g)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑R ↑R' ↑S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑R ↑S'))
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f'

Tactic:
have : IsScalarTower R S S' := .of_algebraMap_eq fun x ↦ congr($(hsq.1.1).hom x)

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S R' S' : CommRingCat
f : R ⟶ S
g : R ⟶ R'
f' : R' ⟶ S'
g' : S ⟶ S'
hsq : IsPushout g f f' g'
hf : toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f
algInst✝⁴ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑R ↑R' := (CommRingCat.Hom.hom g).toAlgebra
algInst✝² : Algebra ↑R' ↑S' := (CommRingCat.Hom.hom f').toAlgebra
algInst✝¹ : Algebra ↑S ↑S' := (CommRingCat.Hom.hom g').toAlgebra
algInst✝ : Algebra ↑R ↑S' := ((CommRingCat.Hom.hom f').comp (CommRingCat.Hom.hom g)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑R ↑R' ↑S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑R ↑S'))
this : IsScalarTower ↑R ↑S ↑S'
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f'
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
X : C
h : P.isoClosure.LimitOfShape J X
⊢ P.limitsOfShape J X

Tactic:
choose obj h₁ h₂ using h.prop_diag_obj

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
h : P.isoClosure.LimitOfShape J X
obj : J → C
h₁ : ∀ (j : J), P (obj j)
h₂ : ∀ (j : J), Nonempty (h.diag.obj j ≅ obj j)
⊢ P.limitsOfShape J X
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
⊢ Q.isoClosure.retractClosure ≤ (ofObj Y).isoClosure

Tactic:
retractClosure_isoClosure

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
⊢ Q.retractClosure ≤ (ofObj Y).isoClosure
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁
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₃
⊢ (((lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
              (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
            lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯)
              ⋯) ≫
          fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
        fst (fst f' g') i₁) ≫
      snd f' g' =
    ((𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫
        fst (fst f' g') i₁) ≫
      snd f' g'

Tactic:
simp [Category.assoc, condition]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
this : IsIso f
⊢ MorphismProperty.isomorphisms C φ

Tactic:
exact ⟨h₂.desc (Cocone.mk _ (inv f ≫ c₁.ι)),
      h₁.hom_ext (fun j ↦ by simp [reassoc_of% (hφ j)]),
      h₂.hom_ext (by simp [hφ])⟩

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ (s : PullbackCone (fst g h) (snd f g)) → s.pt ⟶ pullback (fst f g) (fst f h)

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)), ?refine_1 s ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst

pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)), ?refine_1 s ≫ fst (fst f g) (fst f h) = s.snd

pp: case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = ?refine_1 s

Tactic:
· intro c
    refine pullback.lift c.snd
        (pullback.lift (c.snd ≫ pullback.fst _ _) (c.fst ≫ pullback.snd _ _) ?_) ?_
    · simp [pullback.condition, ← c.condition_assoc]
    · simp

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)),
    lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯ ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ =
      s.fst

case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)),
    lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h) = s.snd

case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

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
X : C
h : P.isoClosure.ColimitOfShape J X
⊢ P.colimitsOfShape J X

Tactic:
choose obj h₁ h₂ using h.prop_diag_obj

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
h : P.isoClosure.ColimitOfShape J X
obj : J → C
h₁ : ∀ (j : J), P (obj j)
h₂ : ∀ (j : J), Nonempty (h.diag.obj j ≅ obj j)
⊢ P.colimitsOfShape J X
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
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
⊢ g = gr ≫ pullback.snd (g ≫ f) f

Tactic:
simp [gr]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ ∀ {X' X Y : ModuleCat R} (f : X' ⟶ X) (g : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y),
    (M.monoidalClosedHomEquiv X' Y).symm (f ≫ g) =
      (MonoidalCategory.tensorLeft M).map f ≫ (M.monoidalClosedHomEquiv X Y).symm g

Tactic:
intros
                ext : 1
                apply TensorProduct.ext'
                intro m n
                rfl

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ 1 ≤ m ^ lift.{u, v} #(β a)

Tactic:
rw [← power_zero]

Goal state after:
α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ ?m.139 ^ 0 ≤ m ^ lift.{u, v} #(β a)

α : Type u
β : α → Type v
inst✝ : ∀ (a : α), Finite (β a)
m : Cardinal.{max u v} := ⋯
a : α
⊢ Cardinal.{max u v}
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: 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 ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ ¬l i = 0

Tactic:
rwa [← lc_def, h.dual_lc] at hi

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

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
e.rank_eq,

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_1
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ
⊢ Module.rank Kᵐᵒᵖ (ι → Kᵐᵒᵖ) = #(V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
e.rank_eq,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ι : Type u_2
h : Infinite ι
b : Module.Basis ι K V
e : (V →ₗ[K] K) ≃ₗ[K] ι → K
⊢ Module.rank K (ι → K) = #(V →ₗ[K] K)
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
f : ((V ⧸ p) × ↥p) ≃ₗ[K] V
⊢ Module.rank K (V ⧸ p) + Module.rank K ↥p = Module.rank K V

Tactic:
exact rank_prod'.symm.trans f.rank_eq

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Products

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
⊢ ∀ (s : Cocone (Discrete.functor Z)) (j : Discrete ι),
    (coproductCocone Z).ι.app j ≫ ↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i })) = s.ι.app j

Tactic:
rintro s ⟨i⟩
    ext (x : Z i)
    simpa only [Discrete.functor_obj_eq_as, coproductCocone, Cofan.mk_pt, Functor.const_obj_obj,
      Cofan.mk_ι_app, hom_comp, LinearMap.coe_comp, Function.comp_apply] using!
      DirectSum.toModule_lof (ι := ι) R (M := fun i ↦ Z i) i x

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: 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
F : WalkingParallelPair ⥤ C
| pullbackFst F ≫ F.map WalkingParallelPairHom.right

Tactic:
pullbackFst_eq_pullback_snd

Goal state after:
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
F : WalkingParallelPair ⥤ C
| pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
    F.map WalkingParallelPairHom.right
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
x : P ⊗[R] (M →ₗ[R] Q)
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) x = (lTensorHomToHomLTensor (RingHom.id R) M P Q) x

Tactic:
lTensorHomEquivHomLTensor_toLinearMap

Goal state after:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
x : P ⊗[R] (M →ₗ[R] Q)
⊢ (lTensorHomToHomLTensor (RingHom.id R) M P Q) x = (lTensorHomToHomLTensor (RingHom.id R) M P Q) x
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.SeparatingRight ↔ B.flip.ker = ⊥

Tactic:
rw [← flip_separatingLeft, separatingLeft_iff_ker_eq_bot]

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

Goal state before:
pp: case h₀
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R M
inst✝² : Module R M₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
⊢ ∀ b ∈ vi.support, b ≠ i → (RingHom.id R) (vi b) • (B (v b)) (v i) = 0

Tactic:
intro j _hj hij
    replace hij : B (v j) (v i) = 0 := hO hij
    rw [hij, RingHom.id_apply, smul_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
⊢ False

Tactic:
let φs := (evalEquiv R M).symm φ

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsReflexive R M
s : Set (M →ₗ[R] R)
inst✝ : Projective R ((M →ₗ[R] R) ⧸ span R s)
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, f z ≠ 0
hn : span R s ≠ ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (evalEquiv R M).symm φ
⊢ False
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫
        colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
    q ≫ h

Tactic:
by
  slice_lhs 1 3 => rw [map_π_preserves_coequalizer_inv_colimMap]
  slice_lhs 2 3 => rw [coequalizer.π_desc]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
W : Submodule R M
inst✝ : Projective R M
h : W.dualAnnihilator = ⊤
⊢ W = ⊥

Tactic:
refine W.eq_bot_iff.mpr fun v hv ↦ (forall_dual_apply_eq_zero_iff R v).mp fun f ↦ ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
W : Submodule R M
inst✝ : Projective R M
h : W.dualAnnihilator = ⊤
v : M
hv : v ∈ W
f : Dual R M
⊢ f v = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Pullbacks

Goal state before:
pp: C : Type u
𝒞 : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasColimit (pair Y Z)
inst✝ : HasColimit (parallelPair (f ≫ coprod.inl) (g ≫ coprod.inr))
ι₁ : Y ⟶ Y ⨿ Z := coprod.inl
ι₂ : Z ⟶ Y ⨿ Z := coprod.inr
c : Y ⨿ Z ⟶ coequalizer (f ≫ ι₁) (g ≫ ι₂) := coequalizer.π (f ≫ ι₁) (g ≫ ι₂)
⊢ f ≫ ι₁ ≫ c = g ≫ ι₂ ≫ c

Tactic:
by
          rw [← Category.assoc, ← Category.assoc, coequalizer.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (KernelFork.ofι g ⋯)

Tactic:
letI gr := regularOfIsPullbackSndOfRegular hn.regularMono comm t
    have q := (HasZeroMorphisms.comp_zero k hn.Z).symm
    convert! gr.isLimit

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ f' ≫ Arrow.Hom.right e.inv ≫ g = 0

Tactic:
by
    have := Arrow.w e.inv
    dsimp at this
    rw [← reassoc_of% this, hf.w, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ e = 0

Tactic:
calc
      e = biprod.inr ≫ biprod.desc (0 : X ⟶ R) e := by rw [biprod.inr_desc]
      _ = biprod.inr ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
      _ = biprod.inr ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
      _ = (biprod.inr ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
      _ = 0 := HasZeroMorphisms.comp_zero _ _

Goal state after: