mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
⊢ ∑ σ, ↑↑(sign σ) * ∏ x, M (σ x) (p x) * N (p x) x = 0

Tactic:
obtain ⟨i, j, hpij, hij⟩ : ∃ i j, p i = p j ∧ i ≠ j := by
    rw [← Finite.injective_iff_bijective, Injective] at H
    push Not at H
    exact H
  exact
    sum_involution (fun σ _ => σ * Equiv.swap i j)
      (fun σ _ => by
        have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=
          Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])
        simp [this, sign_swap hij, -sign_swap', prod_mul_distrib])
      (fun σ _ _ => (not_congr mul_swap_eq_iff).mpr hij) (fun _ _ => mem_univ _) fun σ _ =>
      mul_swap_involutive i j σ

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
⊢ (adjp s A * A) i i = (Aᵀ * adjp s Aᵀ) i i

Tactic:
adjp_transpose,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
⊢ (adjp s A * A) i i = (Aᵀ * (adjp s A)ᵀ) i i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
⊢ (vecMulVec u v).det = 0

Tactic:
by
  obtain ⟨i, j, hij⟩ := exists_pair_ne n
  let uv' := ((vecMulVec u v).updateRow i v).updateRow j v
  have huv' : uv'.det = 0 := by
    refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij
    simp [uv', hij]
  have : vecMulVec u v =
      (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j) := by
    unfold uv'
    rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,
      updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,
      ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]
  rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',
    mul_zero, mul_zero]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
t : Cocone F
h : IsColimit t
x : t.pt
hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬(hom (t.ι.app x_1)) x_2 = x
⊢ (↾fun x ↦ { down := True }) ≠ ↾fun y ↦ { down := y ≠ x }

Tactic:
· intro he
    have := ConcreteCategory.congr_hom he x
    dsimp at this
    exact of_eq_true (congrArg ULift.down this).symm rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ M.mk F ⟨j₁, x⟩ * M.mk F ⟨j₂, y⟩ =
    M.mk F ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩

Tactic:
refine M.mk_eq F _ _ ?_

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
k j₁ : J
x : ↑(F.obj j₁)
f : ⟨j₁, x⟩.fst ⟶ k
j₂ : J
y : ↑(F.obj j₂)
g : ⟨j₂, y⟩.fst ⟶ k
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : k ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = g ≫ β
⊢ ∃ k_1 f_1 g_1,
    (ConcreteCategory.hom (F.map f_1))
        ⟨IsFiltered.max ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.fst ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.fst,
            (ConcreteCategory.hom
                  (F.map (IsFiltered.leftToMax ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.fst ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.fst)))
                ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.snd *
              (ConcreteCategory.hom
                  (F.map (IsFiltered.rightToMax ⟨⟨j₁, x⟩.fst, ⟨j₁, x⟩.snd⟩.fst ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.fst)))
                ⟨⟨j₂, y⟩.fst, ⟨j₂, y⟩.snd⟩.snd⟩.snd =
      (ConcreteCategory.hom (F.map g_1))
        ⟨k, (ConcreteCategory.hom (F.map f)) ⟨j₁, x⟩.snd * (ConcreteCategory.hom (F.map g)) ⟨j₂, y⟩.snd⟩.snd
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x₁ : ↑(F.obj j₁)
j₂ : J
y₂ : ↑(F.obj j₂)
j₃ : J
z₃ : ↑(F.obj j₃)
j : J
f₁ : j₁ ⟶ j
f₂ : j₂ ⟶ j
f₃ : j₃ ⟶ j
x y z : ↑(F.obj j)
h₁ : (ConcreteCategory.hom (F.map f₁)) x₁ = x
h₂ : (ConcreteCategory.hom (F.map f₂)) y₂ = y
h₃ : (ConcreteCategory.hom (F.map f₃)) z₃ = z
⊢ M.mk F ⟨j₁, x₁⟩ * M.mk F ⟨j₂, y₂⟩ * M.mk F ⟨j₃, z₃⟩ = M.mk F ⟨j₁, x₁⟩ * (M.mk F ⟨j₂, y₂⟩ * M.mk F ⟨j₃, z₃⟩)

Tactic:
simp only [← M.map_mk F f₁, ← M.map_mk F f₂, ← M.map_mk F f₃, h₁, h₂, h₃,
        colimit_mul_mk_eq', mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case convert_2.inr
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ : Perm (m ⊕ n)
hσn : σ ∉ (↑(sumCongrHom m n).range).toFinset
h1 : ¬∀ (x : m), ∃ y, Sum.inl y = σ (Sum.inl x)
a : m
ha : ¬∃ y, Sum.inl y = σ (Sum.inl a)
b : n
hx : σ (Sum.inl a) = Sum.inr b
⊢ fromBlocks A B 0 D (σ (Sum.inl a)) (Sum.inl a) = 0

Tactic:
rw [hx, fromBlocks_apply₂₁, zero_apply]

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₂ : Type v₂
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Fintype ι
⊢ ((MultilinearMap.mkPiRing R ι 0) fun x ↦ 1) = 0 fun x ↦ 1

Tactic:
rw [mkPiRing_apply, smul_zero, zero_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
x✝² x✝¹ : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ F.map (f₁ ×ₘ 𝟙 x₂) ≫ F.map (𝟙 y₁ ×ₘ f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))

Tactic:
simp only [← F.map_comp, Category.id_comp, Category.comp_id, prod_comp]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).map f ≫
          ↟(limitπLinearMap F x✝¹)))
      x✝ =
    (Hom.hom (↟(limitπLinearMap F x✝²) ≫ F.map f)) x✝

Tactic:
simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt)).map f ≫
          ofHom (limitπAlgHom F x✝¹)))
      x✝ =
    (Hom.hom (ofHom (limitπAlgHom F x✝²) ≫ F.map f)) x✝

Tactic:
simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
g g' : ↑(limit.cone (parallelPair f 0)).1
⊢ ⟨(ConcreteCategory.hom (kernel.ι f)) (g + g'), ⋯⟩ =
    ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩ + ⟨(ConcreteCategory.hom (kernel.ι f)) g', ⋯⟩

Tactic:
refine Subtype.ext ?_
        simp

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).map f ≫
          ofHom (limitπRingHom F x✝¹)))
      x✝ =
    (Hom.hom (ofHom (limitπRingHom F x✝²) ≫ F.map f)) x✝

Tactic:
simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ RingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget RingCat).sections
this✝ : (forget₂ RingCat SemiRingCat).ReflectsIsomorphisms
this : Small.{u, max u v} ↑((F ⋙ forget₂ RingCat SemiRingCat) ⋙ forget SemiRingCat).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget RingCat)).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget RingCat)).pt)).map f ≫
          ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x✝¹)))
      x✝ =
    (Hom.hom (ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ RingCat SemiRingCat) x✝²) ≫ F.map f)) x✝

Tactic:
simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommRingCat).sections
this✝¹ : (forget₂ CommRingCat RingCat).ReflectsIsomorphisms
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat).sections
F' : J ⥤ SemiRingCat := F ⋙ forget₂ CommRingCat RingCat ⋙ forget₂ RingCat SemiRingCat
this : Small.{u, max u v} ↑(F' ⋙ forget SemiRingCat).sections
x✝² x✝¹ : J
f : x✝² ⟶ x✝¹
x✝ : ↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).obj x✝²)
⊢ (Hom.hom
        (((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).map f ≫
          ofHom (SemiRingCat.limitπRingHom F' x✝¹)))
      x✝ =
    (Hom.hom (ofHom (SemiRingCat.limitπRingHom F' x✝²) ≫ F.map f)) x✝

Tactic:
simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

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

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
val✝ : Fintype J
⊢ (leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j ↦ X ⊗ f j) j

Tactic:
simp [leftDistributor_inv, Preadditive.sum_comp, ← whiskerLeft_comp,
    biproduct.ι_π, whiskerLeft_dite, comp_dite]

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X' : C
⊢ F.map f ▷ F.obj X' ≫ μ Y✝ X' = μ X✝ X' ≫ F.map (f ▷ X')

Tactic:
by
    simp_rw [← tensorHom_id, ← F.map_id, μ_natural]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

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 Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
i : IsIso (pushoutComparison G f g)
⊢ IsColimit (PushoutCocone.mk (G.map (pushout.inl f g)) (G.map (pushout.inr f g)) ⋯)

Tactic:
exact IsColimit.ofPointIso _ (i := i)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
W✝ W W'✝ : MorphismProperty C
W' : ?m.4
P Q : MorphismProperty C
inst✝¹ : P.HasTwoOutOfThreeProperty
inst✝ : Q.HasTwoOutOfThreeProperty
this : P.HasOfPostcompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty

Tactic:
have : P.HasOfPrecompProperty (P ⊓ Q) := .of_le _ _ inf_le_left

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
W✝ W W'✝ : MorphismProperty C
W' : ?m.4
P Q : MorphismProperty C
inst✝¹ : P.HasTwoOutOfThreeProperty
inst✝ : Q.HasTwoOutOfThreeProperty
this✝ : P.HasOfPostcompProperty (P ⊓ Q)
this : P.HasOfPrecompProperty (P ⊓ Q)
⊢ (P ⊓ Q).HasTwoOutOfThreeProperty
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ : C
⊢ tensorμ X₁ X₂ Y₁ Y₂ ≫ tensorδ X₁ X₂ Y₁ Y₂ = 𝟙 ((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂)

Tactic:
simp only [tensorμ, ← whiskerLeft_comp_assoc, tensorδ, assoc, Iso.inv_hom_id_assoc,
    Iso.hom_inv_id_assoc, hom_inv_whiskerRight_assoc, Iso.inv_hom_id, whiskerLeft_id, id_comp,
    Iso.hom_inv_id]

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

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ x.snd <• (x.fst ^ n * x.fst) = (x.fst ^ n * x.fst) •> x.snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0

Tactic:
rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsUnit (inl r) ↔ IsUnit r

Tactic:
rw [isUnit_iff_isUnit_fst, fst_inl]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
⊢ map LinearMap.id LinearMap.id ∘ₗ comul = comul ∘ₗ LinearMap.id

Tactic:
by simp only [map_id, LinearMap.id_comp, LinearMap.comp_id]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inl R A B

pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
· rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
⊢ map LinearMap.id = AlgHom.id R' (tsze R' M)

Tactic:
apply algHom_ext

Goal state after:
R' : Type u
M : Type v
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid M
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
⊢ ∀ (m : M), (map LinearMap.id) (inr m) = (AlgHom.id R' (tsze R' M)) (inr m)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝¹² : CommSemiring R'
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R' M
inst✝⁹ : Module R'ᵐᵒᵖ M
inst✝⁸ : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R' N
inst✝⁵ : Module R'ᵐᵒᵖ N
inst✝⁴ : IsCentralScalar R' N
inst✝³ : AddCommMonoid P
inst✝² : Module R' P
inst✝¹ : Module R'ᵐᵒᵖ P
inst✝ : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ map (g ∘ₗ f) = (map g).comp (map f)

Tactic:
apply algHom_ext

Goal state after:
R' : Type u
M : Type v
inst✝¹² : CommSemiring R'
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R' M
inst✝⁹ : Module R'ᵐᵒᵖ M
inst✝⁸ : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R' N
inst✝⁵ : Module R'ᵐᵒᵖ N
inst✝⁴ : IsCentralScalar R' N
inst✝³ : AddCommMonoid P
inst✝² : Module R' P
inst✝¹ : Module R'ᵐᵒᵖ P
inst✝ : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ ∀ (m : M), (map (g ∘ₗ f)) (inr m) = ((map g).comp (map f)) (inr m)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ x ^ (n + 1) * d = x ^ n * (x * d)

Tactic:
pow_succ,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ x ^ n * x * d = x ^ n * (x * d)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ x ^ (n + 1) * d = x ^ n * (x * d)

Tactic:
rw [pow_succ, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ ¬a ^ (n + 1) ∣ a ^ n * c

Tactic:
pow_succ,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ ¬a ^ n * a ∣ a ^ n * c
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
use ⟨a, ⟨r ^ n, n, rfl⟩⟩

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
r : R
map_unit : IsUnit ((algebraMap R S) r)
surj : ∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a
exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b
z : S
n : ℕ
a : R
hn : z * (algebraMap R S) r ^ n = (algebraMap R S) a
⊢ z * (algebraMap R S) ↑(a, ⟨r ^ n, ⋯⟩).2 = (algebraMap R S) (a, ⟨r ^ n, ⋯⟩).1
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case mem_closure_of_forall
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
h : ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → z ∈ I
x : R
hx : x ∈ s
⊢ x ∈ ↑I

pp: case mem_ideal_of_subset
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J

Tactic:
case mem_closure_of_forall => simpa only [I, SetLike.mem_coe, mem_mk'] using subset_closure hx

Goal state after:
case mem_ideal_of_subset
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})

Tactic:
· simp_rw [comap_sInf, le_iInf_iff]
    intro J hJ
    have : J.IsMaximal := hJ.right
    exact sInf_le ⟨comap_mono hJ.left, comap_isMaximal_of_surjective _ hf⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₁ ≫ h₁₂ ≫ v₁₃ = v₁₁ ≫ h₂₃

Tactic:
by rw [← Category.assoc, s.w]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ «i₂»
hi₂ : «i₂» = t₁.inl
H₁ : IsColimit t₁
H₂ : IsColimit t₂
⊢ IsColimit (t₁.flip.pasteHoriz t₂.flip hi₂)

Tactic:
exact pasteHorizIsPushout hi₂ (PushoutCocone.flipIsColimit H₁) (PushoutCocone.flipIsColimit H₂)

Goal state after: