mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ 0).obj (Opposite.op X)
⊢ (opEquiv' 0 a a ⋯).symm f = ((shiftFunctorZero Cᵒᵖ ℤ).hom.app (Opposite.op X)).unop ≫ f.unop

Tactic:
simp [opEquiv'_symm_apply, opEquiv_symm_apply, shiftFunctorAdd'_add_zero,
    opShiftFunctorEquivalence_zero_unitIso_inv_app]

Goal state after:
Module: Mathlib.CategoryTheory.Center.Localization

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
r : CatCenter C
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X : C
⊢ (r.localization L W).app (L.obj X) = L.map (r.app X)

Tactic:
by
  dsimp [localization]
  simp only [Localization.liftNatTrans_app, Functor.id_obj, Functor.whiskerRight_app,
    NatTrans.naturality, Functor.comp_map, Functor.id_map, Iso.hom_inv_id_app_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
⊢ Function.Surjective ⇑(({ repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }.constr ℕ) id)

Tactic:
refine fun m ↦ ⟨Finsupp.single m 1, ?_⟩

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
m : ↑M
⊢ (({ repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }.constr ℕ) id) (Finsupp.single m 1) = m
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : EnoughInjectives C
this✝ : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, max u v} (Ext X Y 0)

Tactic:
rw [small_congr Ext.homEquiv₀]
      infer_instance

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

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ solution.π.ker
⊢ relations.toQuotient x ∈ ⊥

Tactic:
h,

Goal state after:
case mpr
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : relations.G →₀ A
hx : x ∈ Submodule.span A (Set.range relations.relation)
⊢ relations.toQuotient x ∈ ⊥
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: case pos
ι : 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 x) i'

Tactic:
h,

Goal state after:
case pos
ι : 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 j)) i' = (e.repr x) i'
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
this : Fintype n
⊢ M.det ≠ 0 ↔ M.SeparatingRight

Tactic:
separatingRight_iff_det_ne_zero

Goal state after:
n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
this : Fintype n
⊢ M.det ≠ 0 ↔ M.det ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
j : ι
hD : D j * ∏ x with x ≠ j, D x = 1
h : D j = 0
⊢ False

Tactic:
h,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → F
j : ι
hD : 0 * ∏ x with x ≠ j, D x = 1
h : D j = 0
⊢ False
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map (g.comp f)) x = x

Tactic:
h,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ (map (QuadraticMap.Isometry.id Q₁)) x = x
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0

Tactic:
exact one_mem_graded _

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ [], r j ∈ A (i j)
⊢ 1 ∈ A 0

Tactic:
exact one_mem_graded _

Goal state after:
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✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
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
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
⊢ toLinearMap₂'Aux σ₁ σ₂ ((toMatrix₂Aux R (fun i ↦ Pi.single i 1) fun j ↦ Pi.single j 1) f) = f

Tactic:
refine ext_basis (Pi.basisFun R₁ n) (Pi.basisFun R₂ m) fun i j => ?_
  simp_rw [Pi.basisFun_apply, Matrix.toLinearMap₂'Aux_single, LinearMap.toMatrix₂Aux_apply]

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ diag2 a ha =
    SpecialLinearGroup.transvection ⋯ a * SpecialLinearGroup.transvection ⋯ (-a⁻¹) *
            SpecialLinearGroup.transvection ⋯ a *
          SpecialLinearGroup.transvection ⋯ (-1) *
        SpecialLinearGroup.transvection ⋯ 1 *
      SpecialLinearGroup.transvection ⋯ (-1)

Tactic:
by
  ext i j
  fin_cases i <;> fin_cases j <;>
  simp [diag2_coe', transvection_coe, mul_add, add_mul, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha]

Goal state after:
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₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ σ₂ (y x✝¹) •> σ₁ (x x✝³) •> M x✝³ x✝¹ = σ₁ (x x✝³) •> σ₂ (y x✝¹) •> M x✝³ x✝¹

Tactic:
by
    rw [smul_comm]

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

Goal state before:
pp: case succ
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ ↑(T ^ ↑n) * ↑T = !![1, ↑n + 1; 0, 1]

Tactic:
h,

Goal state after:
case succ
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ !![1, ↑n; 0, 1] * ↑T = !![1, ↑n + 1; 0, 1]
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case pred
n : ℕ
h : ↑(T ^ (-↑n)) = !![1, -↑n; 0, 1]
⊢ ↑(T ^ (-↑n)) * ↑T⁻¹ = !![1, -↑n - 1; 0, 1]

Tactic:
h,

Goal state after:
case pred
n : ℕ
h : ↑(T ^ (-↑n)) = !![1, -↑n; 0, 1]
⊢ !![1, -↑n; 0, 1] * ↑T⁻¹ = !![1, -↑n - 1; 0, 1]
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:
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.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
a : R
x y : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (a • x + y) - Q (a • x) - Q y = a • (Q (x + y) - Q x - Q y)

Tactic:
h,

Goal state after:
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
a : R
x y : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ Q (a • x) + Q y + (B (a • x)) y - Q (a • x) - Q y = a • (Q x + Q y + (B x) y - Q x - Q y)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : AddMonoid ι
inst✝ : Semiring R
i j : ι
a b : R
⊢ (of (fun x ↦ R) i) a * (of (fun x ↦ R) j) b = (of (fun i ↦ R) (i + j)) (a * b)

Tactic:
by
  rw [DirectSum.of_mul_of, Mul.gMul_mul]

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

Goal state before:
pp: 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
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
B' : BilinMap R M N
h' : ∀ (x y : M), Q' (x + y) = Q' x + Q' y + (B' x) y
x y : M
⊢ Q (x + y) + Q' (x + y) = Q x + Q' x + (Q y + Q' y) + ((B + B') x) y

Tactic:
h,

Goal state after:
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
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
B' : BilinMap R M N
h' : ∀ (x y : M), Q' (x + y) = Q' x + Q' y + (B' x) y
x y : M
⊢ Q x + Q y + (B x) y + Q' (x + y) = Q x + Q' x + (Q y + Q' y) + ((B + B') x) y
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: 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✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : QuadraticMap R M N
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ -Q (x + y) = -Q x + -Q y + ((-B) x) y

Tactic:
h,

Goal state after:
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✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : QuadraticMap R M N
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ -(Q x + Q y + (B x) y) = -Q x + -Q y + ((-B) x) y
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'
⊢ (toLinearMap₂' R) J' ∘ₗ toLin' A = ((toLinearMap₂' R) J).compl₂ (toLin' A') ↔ J.IsAdjointPair J' A A'

Tactic:
h,

Goal state after:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'
⊢ (toMatrix₂' R) ((toLinearMap₂' R) J' ∘ₗ toLin' A) = (toMatrix₂' R) (((toLinearMap₂' R) J).compl₂ (toLin' A')) ↔
    J.IsAdjointPair J' A A'
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
⊢ (toLinearMap₂ b₂ b₂) J' ∘ₗ (toLin b₁ b₂) A = ((toLinearMap₂ b₁ b₁) J).compl₂ ((toLin b₂ b₁) A') ↔
    J.IsAdjointPair J' A A'

Tactic:
h,

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
n' : Type u_13
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : M₁ →ₗ[R] M₂ →ₗ[R] R), B = B' ↔ (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁ b₂) B'
⊢ (toMatrix₂ b₁ b₂) ((toLinearMap₂ b₂ b₂) J' ∘ₗ (toLin b₁ b₂) A) =
      (toMatrix₂ b₁ b₂) (((toLinearMap₂ b₁ b₁) J).compl₂ ((toLin b₂ b₁) A')) ↔
    J.IsAdjointPair J' A A'
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

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
p : Submodule R (CliffordAlgebra Q)
n : ℕ
⊢ Submodule.map reverse (p ^ n) = Submodule.map reverse p ^ n

Tactic:
by
  simp_rw [reverse, Submodule.map_comp, Submodule.map_pow, Submodule.map_unop_pow]

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

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
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x : CliffordAlgebra Q
this : x ∈ ⨆ i, (ι Q).range ^ i
⊢ P x

Tactic:
induction this using Submodule.iSup_induction' with

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

Goal state before:
pp: case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
hf0 : toTrivSqZeroExt ((ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0

Tactic:
h,

Goal state after:
case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
hf0 : toTrivSqZeroExt ((algebraMap R (ExteriorAlgebra R M)) r) = (0, x)
⊢ x = 0 ∧ r = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case pos
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : i = 0
⊢ (ι R) (f i) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
h,

Goal state after:
case pos
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : i = 0
⊢ (ι R) (f 0) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
ι : Type u_5
⊢ Module R (M [⋀^ι]→ₗ[R] N)

Tactic:
by
  infer_instance

Goal state after:
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 (Sum.elim (⇑(ConcreteCategory.hom S.f) ∘ v) (Function.invFun (Hom.hom S.g).toFun ∘ w))

Tactic:
by
  apply linearIndependent_leftExact hS'.exact hv _ hS'.mono_f rfl
  dsimp
  convert! hw
  ext
  apply Function.rightInverse_invFun ((epi_iff_surjective _).mp hS'.epi_g)

Goal state after:
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
j : J
x y : ↑(F.obj j)
⊢ M.mk F ⟨j, x⟩ + M.mk F ⟨j, y⟩ = M.mk F ⟨j, x + y⟩

Tactic:
by
  apply AddMonCat.FilteredColimits.colimit_add_mk_eq'

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
⊢ m - m' ∈ (Hom.hom S.f).range

Tactic:
rw [hS.moduleCat_range_eq_ker]

Goal state after:
ι : Type u_1
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
β : Type u_4
u : ι ⊕ β → ↑S.X₂
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
hv : ⊤ ≤ span R (range v)
hw : ⊤ ≤ span R (range (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr))
m : ↑S.X₂
a✝ : m ∈ ⊤
cm : β →₀ R
hm : (cm.sum fun i a ↦ a • (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) i) = (ConcreteCategory.hom S.g) m
m' : ↑S.X₂ := cm.sum fun j a ↦ a • u (Sum.inr j)
⊢ m - m' ∈ (Hom.hom S.g).ker
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
⊢ (imageIsoRange f).hom ≫ ↟(Hom.hom f).range.subtype = Limits.image.ι f

Tactic:
rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_4
inst✝² : DecidableEq ι
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M [⋀^ι]→ₗ[R] N
⊢ ∀ (r : (relations R ι M).R), (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation r) = 0

Tactic:
rintro (⟨m, i, x, y⟩ | ⟨m, i, r, x⟩ | ⟨v, i, j, hm, hij⟩)

Goal state after:
case add
R : Type u
inst✝⁹ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_4
inst✝² : DecidableEq ι
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M [⋀^ι]→ₗ[R] N
m : ι → M
i : ι
x y : M
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.add m i x y)) = 0

case smul
R : Type u
inst✝⁹ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_4
inst✝² : DecidableEq ι
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M [⋀^ι]→ₗ[R] N
m : ι → M
i : ι
r : R
x : M
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.smul m i r x)) = 0

case alt
R : Type u
inst✝⁹ : CommRing R
n : ℕ
M✝ : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
ι : Type u_4
inst✝² : DecidableEq ι
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
hm : v i = v j
hij : i ≠ j
⊢ (Finsupp.linearCombination R fun m ↦ f m) ((relations R ι M).relation (Rels.alt v i j hm hij)) = 0
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
j : J
X : Cᵒᵖ
⊢ (c.ι.app j ≫ { app := fun X ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }).app X = (s.ι.app j).app X

Tactic:
exact (hc X).fac ((evaluation R X).mapCocone s) j

Goal state after:
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
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
⊢ ∀ (k : J), PreservesColimitsOfShape K (tensorLeft F ⋙ (evaluation J C).obj k)

Tactic:
intro k

Goal state after:
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
K : Type u_5
inst✝² : Category.{v_5, u_5} K
inst✝¹ : HasColimitsOfShape K C
inst✝ : ∀ (X : C), PreservesColimitsOfShape K (tensorLeft X)
F : J ⥤ C
k : J
⊢ PreservesColimitsOfShape K (tensorLeft F ⋙ (evaluation J C).obj k)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ {c : Cᵒᵖ} (s s' : op d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t

Tactic:
intro c s s'

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
c : Cᵒᵖ
s s' : op d ⟶ F.op.obj c
⊢ ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t