mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom = (singleObjCyclesSelfIso c j A).hom ≫ f

Tactic:
← cancel_mono (singleObjCyclesSelfIso c j B).inv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom) ≫ (singleObjCyclesSelfIso c j B).inv =
    ((singleObjCyclesSelfIso c j A).hom ≫ f) ≫ (singleObjCyclesSelfIso c j B).inv
Module: Mathlib.Algebra.Homology.SingleHomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom =
    ((single C c j).obj A).homologyπ j ≫ (singleObjHomologySelfIso c j A).hom ≫ f

Tactic:
singleObjCyclesSelfIso_hom_naturality,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).hom ≫ f = ((single C c j).obj A).homologyπ j ≫ (singleObjHomologySelfIso c j A).hom ≫ f
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₂ L₃) ((homEquiv W L₁ L₂) f) = (homEquiv W L₁ L₃) f

Tactic:
dsimp only [homEquiv_apply]
  apply LocalizerMorphism.homMap_homMap

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

Tactic:
· apply (Y.isZero_of_isStrictlyGE b i (by lia)).eq_of_tgt

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ φ 0 = 0

Tactic:
rw [map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
inst✝³ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
x✝ : PullbackShift C φ
⊢ φ 0 = 0

Tactic:
rw [map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁).unop ≫ (shiftFunctor C 1).map T₂.mor₃.unop) ≫
      (shiftFunctor C 1).map c =
    a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃

Tactic:
replace hc₂ := ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫= hc₂

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
hT₂ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      (((opShiftFunctorEquivalence C 1).unitIso.inv.app T₂.obj₁).unop ≫ (shiftFunctor C 1).map T₂.mor₃.unop) ≫
        (shiftFunctor C 1).map c =
    ((opShiftFunctorEquivalence C 1).unitIso.hom.app T₂.obj₁).unop ≫
      a.unop ≫ ((opShiftFunctorEquivalence C 1).unitIso.inv.app T₁.obj₁).unop ≫ (shiftFunctor C 1).map T₁.mor₃.unop
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map a = c ≫ T₂.mor₃
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ (triangleOpEquivalence C).functor.obj (Opposite.op T) ∈ distinguishedTriangles

Tactic:
rw [mem_distTriang_op_iff']

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ∃ T',
    ∃ (_ : T' ∈ distinguishedTriangles),
      Nonempty
        ((triangleOpEquivalence C).functor.obj (Opposite.op T) ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
⊢ Functor.Linear R L

Tactic:
let := linear R L W
  constructor
  intro X Y f r
  change L.map (r • f) = ((Linear.toCatCenter R C r).localization L W).app (L.obj X) ≫ L.map f
  simp [← L.map_comp]

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

Goal state before:
pp: K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
μ : V₁ → K₁
h : ∑ a ∈ {x}, μ a • a ∈ Submodule.span K₁ ↑{x} ⊓ Submodule.orthogonalBilin B (Submodule.span K₁ ↑{x})
⊢ x ∈ Submodule.span K₁ ↑{x}

Tactic:
simp [Submodule.mem_span]

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Injective ⇑solution.fromQuotient ↔ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
constructor
  · intro h
    rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]
  · intro h
    rw [← LinearMap.ker_eq_bot, eq_bot_iff]
    intro x hx
    obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x
    replace hx : x ∈ LinearMap.ker solution.π := by
      simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx
    rw [h, ← range_map] at hx
    obtain ⟨x, rfl⟩ := hx
    simp only [toQuotient_map_apply, Submodule.zero_mem]

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

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
convert! hv

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

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : CommSemiring R
M : Matrix m n R
inst✝¹ : Fintype m
inst✝ : Fintype n
v : m → R
hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
convert! hv

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case calc_1
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
u : Rˣ
hu : u ∈ image (⇑f.toHomUnits) univ
⊢ #{g | f.toHomUnits g = u} = c

Tactic:
apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits
      · simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu
      · exact ⟨1, f.toHomUnits.map_one⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑σ ↑(↑ξ ^ n) = ↑1

Tactic:
ξ.prop

Goal state after:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ : ↥(rootsOfUnity n R)
⊢ ↑σ ↑1 = ↑1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ QuadraticMap.polar (⇑Q) a b • (ι Q) a - Q a • (ι Q) b = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
← map_smul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (ι Q) (QuadraticMap.polar (⇑Q) a b • a) - Q a • (ι Q) b = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (ι Q) (QuadraticMap.polar (⇑Q) a b • a) - Q a • (ι Q) b = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
← map_smul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (ι Q) (QuadraticMap.polar (⇑Q) a b • a) - (ι Q) (Q a • b) = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid N₂
inst✝¹³ : Module R N₂
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → R₁
y : m → R₂
⊢ (((toLinearMapₛₗ₂' R σ₁ σ₂) M) x) y = ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j

Tactic:
by
  rw [toLinearMapₛₗ₂', toMatrixₛₗ₂', LinearEquiv.coe_symm_mk, toLinearMap₂'Aux, mk₂'ₛₗ_apply]
  apply Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by
    rw [smul_comm]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
i✝ j✝ : Fin 2
⊢ ↑(diag2n hij c hc) i✝ j✝ = ↑(diag2 c⁻¹ ⋯) i✝ j✝

Tactic:
simp [diag2n_coe, diagonal_apply]

Goal state after:
F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
i✝ j✝ : Fin 2
⊢ (if i✝ = j✝ then if i✝ = 1 then c else if i✝ = 0 then c⁻¹ else 1 else 0) =
    if i✝ = j✝ then if i✝ = 0 then c⁻¹ else if i✝ = 1 then c else 1 else 0
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
f : (i : ι) → A i →ₗ[R] B
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
r : R
⊢ (toSemiring (fun i ↦ (f i).toAddMonoidHom) hone hmul) ((algebraMap R (⨁ (i : ι), A i)) r) = (algebraMap R B) r

Tactic:
by
      change toModule R _ _ f (algebraMap R _ r) = _
      rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' = DFinsupp.sum a fun x ai ↦ DFinsupp.sum a' fun x_1 aj ↦ (of A (x + x_1)) (GradedMonoid.GMul.mul ai aj)

Tactic:
by
  change mulHom _ a a' = _
  -- Porting note: I have no idea how the proof from ml3 worked it used to be
  -- simpa only [mul_hom, to_add_monoid, dfinsupp.lift_add_hom_apply, dfinsupp.sum_add_hom_apply,
  -- add_monoid_hom.dfinsupp_sum_apply, flip_apply, add_monoid_hom.dfinsupp_sum_add_hom_apply],
  rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply]
  dsimp only [DirectSum]
  rw [DFinsupp.sumAddHom_apply, AddMonoidHom.dfinsuppSum_apply]
  apply congrArg _
  funext x
  simp [AddMonoidHom.dfinsuppSum_apply, DFinsupp.sumAddHom_apply, DirectSum.toAddMonoid]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive ↑m
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
⊢ ∀ (m : M), motive m

Tactic:
by
  let ℳ' : ι → AddSubmonoid M := fun i ↦
    (⟨⟨ℳ i, fun x y ↦ AddMemClass.add_mem x y⟩, (ZeroMemClass.zero_mem _)⟩ : AddSubmonoid M)
  have t : DirectSum.Decomposition ℳ' :=
    { decompose' := DirectSum.decompose ℳ
      left_inv := fun _ ↦ (decompose ℳ).left_inv _
      right_inv := fun _ ↦ (decompose ℳ).right_inv _ }
  have mem : ∀ m, m ∈ iSup ℳ' := fun _m ↦
    (DirectSum.IsInternal.addSubmonoid_iSup_eq_top ℳ' (Decomposition.isInternal ℳ')).symm ▸ trivial
  -- Porting note: needs to use @ even though no implicit argument is provided
  exact fun m ↦ @AddSubmonoid.iSup_induction _ _ _ ℳ' _ _ (mem m)
    (fun i m h ↦ homogeneous ⟨m, h⟩) zero add

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y y' : M
⊢ polar (⇑Q) x (y - y') = polar (⇑Q) x y - polar (⇑Q) x y'

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, polar_add_right, polar_neg_right]

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
⊢ 0 = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

Tactic:
rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'

Goal state after:
case neg.inl
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : i ≠ 0
⊢ 0 = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

case neg.inr
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : j ≠ 0
⊢ 0 = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) 0 = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨0, ⋯⟩

Tactic:
rw [map_zero]

Goal state after:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ 0 = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨0, ⋯⟩
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (((DirectSum.coeAlgHom (evenOdd Q)).comp ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩)).toLinearMap ∘ₗ ι Q) m =
    ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q) m

Tactic:
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply,
        AlgHom.id_apply]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (DirectSum.coeAlgHom (evenOdd Q)) (((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((ι Q) m)) = (ι Q) m
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = (List.ofFn fun i ↦ (ι R) (v i)).prod

Tactic:
exact ⟨fun i => ⟨ι R (v i), LinearMap.mem_range_self _ _⟩, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ExteriorAlgebra R M
⊢ (liftAlternating (ιMulti R)) v = v

Tactic:
induction v using CliffordAlgebra.left_induction with

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

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (RingHom.id R) c •
      (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))

Tactic:
change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c •
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)
Module: Mathlib.Algebra.Category.ModuleCat.Free

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Function.Surjective ⇑(ConcreteCategory.hom S.g)
⊢ (⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g)) ∘ w = w

Tactic:
Function.RightInverse.comp_eq_id (Function.rightInverse_invFun hE),

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
w : ι' → ↑S.X₃
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range w)
hE : Function.Surjective ⇑(ConcreteCategory.hom S.g)
⊢ id ∘ w = w
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
ha : a • h m = 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)

Tactic:
← map_smul,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
ha : h (a • m) = 0
⊢ mk m s ∈ Set.range ⇑((IsLocalizedModule.map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
⊢ { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ } =
    X ◁
        IsTerminal.from
          (evaluationJointlyReflectsLimits (asEmptyCone (𝟙_ (J ⥤ C))) fun x ↦
            isLimitChangeEmptyCone C isTerminalTensorUnit (((evaluation J C).obj x).mapCone (asEmptyCone (𝟙_ (J ⥤ C))))
              (Iso.refl (asEmptyCone (𝟙_ C)).pt))
          Y ≫
      (ρ_ X).hom

Tactic:
ext
    simp only [Monoidal.tensorObj_obj, fst_def, asEmptyCone_pt, NatTrans.comp_app,
      Monoidal.tensorUnit_obj, Monoidal.whiskerLeft_app, Monoidal.rightUnitor_hom_app,
      Iso.cancel_iso_hom_right]
    congr
    subsingleton

Goal state after: