mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : C ⥤ D
inst✝¹ : G.CommShift B
τ : F ⟶ G
inst✝ : CommShift τ B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ x✝¹)).hom.app x✝ ≫
        (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) x✝¹).map (τ.app x✝) =
    τ.app ((shiftFunctor (PullbackShift C φ) x✝¹).obj x✝) ≫
      G.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app x✝ ≫ (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj x✝)

Tactic:
rw [← τ.naturality_assoc]

Goal state after:
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
G : C ⥤ D
inst✝¹ : G.CommShift B
τ : F ⟶ G
inst✝ : CommShift τ B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
      (commShiftIso F (φ x✝¹)).hom.app x✝ ≫
        (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) x✝¹).map (τ.app x✝) =
    F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝) ≫
      τ.app ((shiftFunctor C (φ x✝¹)).obj x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app x✝ ≫ (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj x✝)
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 : (B x) (μ x • x) = 0
⊢ μ x = 0

Tactic:
map_smulₛₗ

Goal state after:
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 : J₁' (μ x) • (B x) x = 0
⊢ μ x = 0
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
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
convert! hw

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
w : n → R
hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0
⊢ ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0

Tactic:
convert! hw

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (update v j x k)) i' = (e.repr (v k)) i'

Tactic:
rw [update_of_ne h]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: 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}
⊢ Set.InjOn (fun x_1 ↦ x ^ x_1) ↑(range (orderOf x))

Tactic:
by simpa using pow_injOn_Iio_orderOf

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

Goal state before:
pp: case mpr
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ M.det = 0 → ∃ v, v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
contrapose!
    intro h
    have : Function.Injective (Matrix.toLin' M) := by
      simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
    have : M * (LinearEquiv.ofInjectiveEndo _ this).symm.toMatrix' = 1 := by
      refine Matrix.toLin'.injective (LinearMap.ext fun v => ?_)
      rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]
      exact (LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v
    exact Matrix.det_ne_zero_of_right_inverse this

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

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ ∑ a ∈ (b₁.repr x).support,
      ∑ x_1 ∈ (b₂.repr y).support, ρ₁₂ ((b₁.repr x) a) • σ₁₂ ((b₂.repr y) x_1) • (B (b₁ a)) (b₂ x_1) =
    ∑ x_1 ∈ (b₁.repr x).support,
      ∑ x_2 ∈ (b₂.repr y).support, ρ₁₂ ((b₁.repr x) x_1) • (B (b₁ x_1)) ((b₂.repr y) x_2 • b₂ x_2)

Tactic:
map_smulₛₗ

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

Goal state before:
pp: case mpr.refine_2.calc_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ∑ x, M.map (⇑(algebraMap A K)) i x * (⇑(algebraMap A K) ∘ fun i ↦ f (v i) ⋯) x =
    ∑ x, (algebraMap A K).mapMatrix M i x * ((algebraMap A K) b • v) x

Tactic:
Function.comp_apply,

Goal state after:
case mpr.refine_2.calc_1
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ∑ x, M.map (⇑(algebraMap A K)) i x * (algebraMap A K) (f (v x) ⋯) =
    ∑ x, (algebraMap A K).mapMatrix M i x * ((algebraMap A K) b • v) x
Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry

Goal state before:
pp: case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ (toLinearMap✝¹.toFun m) = Q₁ m
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } = { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
toLinearMap✝¹ : M₁ →ₗ[R] M₂
map_app'✝¹ : ∀ (m : M₁), Q₂ (toLinearMap✝¹.toFun m) = Q₁ m
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h :
  (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝¹, map_app' := map_app'✝¹ } =
    (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ Q₂ (f ((↑f.symm).toFun m)) = Q₂ m

Tactic:
congr

Goal state after:
case e_6
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f : Q₁.IsometryEquiv Q₂
m : M₂
⊢ f ((↑f.symm).toFun m) = m
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case mk.mk
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q Q' : QuadraticMap R M N
toFun✝¹ : M → N
toFun_smul✝¹ : ∀ (a : R) (x : M), toFun✝¹ (a • x) = (a * a) • toFun✝¹ x
exists_companion'✝¹ : ∃ B, ∀ (x y : M), toFun✝¹ (x + y) = toFun✝¹ x + toFun✝¹ y + (B x) y
toFun✝ : M → N
toFun_smul✝ : ∀ (a : R) (x : M), toFun✝ (a • x) = (a * a) • toFun✝ x
exists_companion'✝ : ∃ B, ∀ (x y : M), toFun✝ (x + y) = toFun✝ x + toFun✝ y + (B x) y
h :
  { toFun := toFun✝¹, toFun_smul := toFun_smul✝¹, exists_companion' := exists_companion'✝¹ }.toFun =
    { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }.toFun
⊢ { toFun := toFun✝¹, toFun_smul := toFun_smul✝¹, exists_companion' := exists_companion'✝¹ } =
    { toFun := toFun✝, toFun_smul := toFun_smul✝, exists_companion' := exists_companion'✝ }

Tactic:
congr

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
decompose'✝¹ : M → ⨁ (i : ι), ↥(ℳ i)
left_inv✝ : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝¹
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝¹
decompose'✝ : M → ⨁ (i : ι), ↥(ℳ i)
yl : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
right_inv✝ : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
⊢ { decompose' := decompose'✝¹, left_inv := left_inv✝, right_inv := xr } =
    { decompose' := decompose'✝, left_inv := yl, right_inv := right_inv✝ }

Tactic:
congr

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
σ : Type u_4
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike σ M
inst✝ : AddSubmonoidClass σ M
ℳ : ι → σ
decompose'✝¹ : M → ⨁ (i : ι), ↥(ℳ i)
left_inv✝ : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝¹
xr : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝¹
decompose'✝ : M → ⨁ (i : ι), ↥(ℳ i)
yl : Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
right_inv✝ : Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) decompose'✝
⊢ decompose'✝¹ = decompose'✝
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ ∑ i ∈ DFinsupp.support r,
      ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n) =
    DFinsupp.sum r fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0

Tactic:
congr

Goal state after:
case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n : ι
⊢ (fun i ↦ ↑((DFinsupp.sum r' fun x aj ↦ (of (fun i ↦ ↥(A i)) (i + x)) (GradedMonoid.GMul.mul (r i) aj)) n)) = fun i ↦
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) i (r i)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ ∑ i ∈ DFinsupp.support r', ↑(((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n) =
    (fun i ri ↦ DFinsupp.sum r' fun j rj ↦ if i + j = n then ↑ri * ↑rj else 0) x✝ (r x✝)

Tactic:
congr

Goal state after:
case e_f.e_f
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : SetLike σ R
inst✝³ : AddSubmonoidClass σ R
A : ι → σ
inst✝² : AddMonoid ι
inst✝¹ : SetLike.GradedMonoid A
inst✝ : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)
r r' : ⨁ (i : ι), ↥(A i)
n x✝ : ι
⊢ (fun i ↦ ↑(((of (fun i ↦ ↥(A i)) (x✝ + i)) (GradedMonoid.GMul.mul (r x✝) (r' i))) n)) = fun i ↦
    (fun j rj ↦ if x✝ + j = n then ↑(r x✝) * ↑rj else 0) i (r' i)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < (Multiset.map Prod.snd s).sum
⊢ (Multiset.map Prod.fst s).prod n = 0

Tactic:
by
  have := listProd_apply_eq_zero' (l := s.toList) (by simpa using hs)
    (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
  simpa [← Multiset.prod_coe, ← Multiset.map_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
m : M
⊢ ((foldl Q f hf) n) ((ι Q) m) = (f m) n

Tactic:
rw [← foldr_reverse, reverse_ι, foldr_ι]

Goal state after:
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
⊢ (ι Q).range ≤ (ι Q).range ^ ↑⟨1, ⋯⟩

Tactic:
exact (pow_one _).ge

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

Goal state before:
pp: R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
x✝ : (i : ι ⊕ ι') → N i
⊢ (f fun t ↦ Sum.rec (fun i ↦ x✝ (Sum.inl i)) (fun i' ↦ x✝ (Sum.inr i')) t) = f x✝

Tactic:
congr

Goal state after:
case e_6
R : Type uR
ι : Type uι
ι' : Type uι'
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
f : MultilinearMap R N M₂
x✝ : (i : ι ⊕ ι') → N i
⊢ (fun t ↦ Sum.rec (fun i ↦ x✝ (Sum.inl i)) (fun i' ↦ x✝ (Sum.inr i')) t) = x✝
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ ((f fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i ↦
      s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) =
    (f fun x_1 ↦ x) fun x ↦ y

Tactic:
congr

Goal state after:
case e_5.e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ (fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inl i))) = fun x_1 ↦ x

case e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ (fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = fun x ↦ y
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
m n : ℕ
a : Fin m → M
b : Fin n → M
⊢ (List.ofFn fun i ↦ (ι R) (a i)).prod * (List.ofFn fun i ↦ (ι R) (b i)).prod =
    (List.ofFn (⇑(ι R) ∘ a)).prod * (List.ofFn (⇑(ι R) ∘ b)).prod

Tactic:
congr

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

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (f n.succ) (Matrix.vecCons (v 0) fun i ↦ v i.succ) = (f (n + 1)) v

Tactic:
congr

Goal state after:
case succ.e_6
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
ih :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (v : Fin n → M),
    (liftAlternating f) (List.ofFn fun i ↦ (ι R) (v i)).prod = (f n) v
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
v : Fin (n + 1) → M
⊢ (Matrix.vecCons (v 0) fun i ↦ v i.succ) = v
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
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ (ιMulti R (m + n)) (Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t))) =
    (ιMulti R (m + n))
      ((v ∘ ⇑(ofFinEmbEquiv.symm (disjUnion h))) ∘
        ⇑(finSumFinEquiv.symm.trans
            ((↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t))).trans
              ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h).trans ↑(orderIsoOfFin (disjUnion h)).symm))))

Tactic:
congr

Goal state after:
case e_6
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ Fin.append (v ∘ ⇑(ofFinEmbEquiv.symm s)) (v ∘ ⇑(ofFinEmbEquiv.symm t)) =
    (v ∘ ⇑(ofFinEmbEquiv.symm (disjUnion h))) ∘
      ⇑(finSumFinEquiv.symm.trans
          ((↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t))).trans
            ((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h).trans ↑(orderIsoOfFin (disjUnion h)).symm)))
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₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range ⇑(ConcreteCategory.hom S.f)))

Tactic:
← LinearMap.coe_range,

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₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R ↑(ConcreteCategory.hom S.f).range)
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x✝ : ↑(M F)
x : (j : J) × ↑(F.obj j)
⊢ ∀ (b : (j : J) × ↑(F.obj j)),
    ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
            forget AddMonCat).ColimitTypeRel
        x b →
      colimitSMulAux F r x = colimitSMulAux F r b

Tactic:
y

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x✝ : ↑(M F)
x y : (j : J) × ↑(F.obj j)
⊢ ((((F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙
          forget AddMonCat).ColimitTypeRel
      x y →
    colimitSMulAux F r x = colimitSMulAux F r y
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.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w)

Tactic:
convert! hw

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
v : ι → ↑S.X₁
hv : LinearIndependent R v
w : ι' → ↑S.X₃
hw : LinearIndependent R w
⊢ ⇑(ConcreteCategory.hom S.g) ∘ Function.invFun ⇑(Hom.hom S.g) ∘ w = w
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: 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) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c • (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)

Tactic:
apply (mono_iff_injective F'.m).1
      · infer_instance
      rw [map_smul]
      change (F'.e ≫ F'.m) _ = _ • (F'.e ≫ F'.m) _
      simp_rw [F'.fac, (Classical.indefiniteDescription (fun z => f z = _) _).2]
      rfl

Goal state after: