mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i =
    ((single C (ComplexShape.up ℤ) i).obj I).pOpcycles i ≫
      (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I).inv ≫
        (singleObjOpcyclesSelfIso (ComplexShape.up ℤ) i I).hom ≫ opcyclesMap ι i

Tactic:
Iso.inv_hom_id_assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
I : C
inst✝² : Injective I
L : CochainComplex C ℤ
i : ℤ
ι : (singleFunctor C i).obj I ⟶ L
inst✝¹ : L.IsStrictlyGE i
inst✝ : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := (singleObjHomologySelfIso (ComplexShape.up ℤ) i I).inv ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
⊢ ι.f i ≫ pOpcycles L i = ((single C (ComplexShape.up ℤ) i).obj I).pOpcycles i ≫ opcyclesMap ι i
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ n₁ : ℕ
h : 1 + n₀ = n₁
⊢ AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯) ≫ AddCommGrpCat.ofHom (hS.extClass.precomp Y h) = 0

Tactic:
ext
        dsimp
        simp only [ShortComplex.ShortExact.extClass_comp_assoc]

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
⊢ Submodule.span A (Set.range relations.relation) ≤ solution.π.ker

Tactic:
rw [Submodule.span_le]

Goal state after:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Set.range relations.relation ⊆ ↑solution.π.ker
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.Quotient
hx : x ∈ solution.fromQuotient.ker
⊢ x ∈ ⊥

Tactic:
obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x

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 : relations.toQuotient x ∈ solution.fromQuotient.ker
⊢ relations.toQuotient x ∈ ⊥
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
i : ι
⊢ i ∈ s → ∃ d, f i = d ^ n

Tactic:
hi

Goal state after:
ι : Type u_2
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i ∈ s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝³ : Fintype ι'
inst✝² : Finite κ
inst✝¹ : Fintype κ'
inst✝ : DecidableEq ι'
⊢ (toLin b' c) (c.toMatrix ⇑c' * (toMatrix b' c') f) = (toLin b' c) ((toMatrix b' c) f)

Tactic:
by
    have := Classical.decEq κ'
    rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]

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

Goal state before:
pp: 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) ↔ ((algebraMap A K).mapMatrix M).det = 0
⊢ (∃ v, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
rw [← RingHom.map_det, IsFractionRing.to_map_eq_zero_iff] at this

Goal state after:
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, v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ (↑A⁻¹ * ↑A).det = 1

Tactic:
A.inv_mul,

Goal state after:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : GL n R
⊢ Matrix.det 1 = 1
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mp.refine_2
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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
⊢ (algebraMap A K) (0 i) = 0 i

Tactic:
Pi.zero_apply,

Goal state after:
case mp.refine_2
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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
⊢ (algebraMap A K) 0 = 0 i
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_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
h : (fun i ↦ f (v i) ⋯) = 0
i : n
this : b • v i = (algebraMap A K) (0 i)
⊢ v i = 0 i

Tactic:
Pi.zero_apply,

Goal state after:
case mpr.refine_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
h : (fun i ↦ f (v i) ⋯) = 0
i : n
this : b • v i = (algebraMap A K) 0
⊢ v i = 0 i
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_2.calc_2
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
⊢ (algebraMap A K) b • 0 i = 0

Tactic:
Pi.zero_apply,

Goal state after:
case mpr.refine_2.calc_2
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
⊢ (algebraMap A K) b • 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ 1 ≠ 0

Tactic:
norm_num

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (map f) ((map g) ((ι Q₁) m)) = (map (f.comp g)) ((ι Q₁) m)

Tactic:
rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]

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

Goal state before:
pp: 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✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
⊢ ∑ i_1, ∑ j_1, σ₂ (Pi.single j 1 j_1) •> σ₁ (Pi.single i 1 i_1) •> f i_1 j_1 = f i j

Tactic:
have : (∑ i', ∑ j', (if i = i' then (1 : S₁) else (0 : S₁)) •
        (if j = j' then (1 : S₂) else (0 : S₂)) • f i' j') =
      f i j := by
    simp_rw [← Finset.smul_sum]
    simp only [ite_smul, one_smul, zero_smul, sum_ite_eq, mem_univ, ↓reduceIte]

Goal state after:
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✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i', ∑ j', (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
⊢ ∑ i_1, ∑ j_1, σ₂ (Pi.single j 1 j_1) •> σ₁ (Pi.single i 1 i_1) •> f i_1 j_1 = f i j
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
α : Type u_3
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) l).prod

Tactic:
induction l with

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✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ (2 * 2) • Q x = ↑4 • Q x

Tactic:
norm_num

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ {i : ι} → A i →+ R

Tactic:
by intro i; exact (F : (⨁ i, A i) →+ R).comp (of _ i)

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f :
  { f //
    f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), f (GradedMonoid.GMul.mul ai aj) = f ai * f aj }
xi : ι
xv : A xi
⊢ ↑((fun F ↦ ⟨fun {i} ↦ (↑F).comp (of A i), ⋯⟩) ((fun f ↦ toSemiring (fun x ↦ ↑f) ⋯ ⋯) f)) xv = ↑f xv

Tactic:
exact toAddMonoid_of (fun _ => f.1) xi xv

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

Goal state before:
pp: case cons.e_a.e_a
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ (∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + ∑ x ∈ s, polar (⇑Q) (f a) (f x) =
    (∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
      ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0

Tactic:
rw [add_comm]

Goal state after:
case cons.e_a.e_a
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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ (∑ x ∈ s, polar (⇑Q) (f a) (f x) + ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) =
    (∑ x ∈ s, if ¬a = x then polar (⇑Q) (f a) (f x) else 0) +
      ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: case e'_2.e'_2
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = ↑v⁻¹ * x

Tactic:
· rw [mul_assoc, mul_assoc, ← mul_assoc _ _ J]
      rfl

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
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldr Q f hf) n) (List.map (⇑(ι Q)) l).prod = List.foldr (fun m n ↦ (f m) n) n l

Tactic:
induction l with

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ s ∈ powersetCard α n ↔ #s = n

Tactic:
rw [powersetCard, Set.mem_ofPred_eq]

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

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
⊢ basisRepr Q v = weightedSumSquares R fun i ↦ Q (v i)

Tactic:
ext w
  rw [basisRepr_apply, ← @associated_eq_self_apply R, map_sum, weightedSumSquares_apply]
  refine sum_congr rfl fun j hj => ?_
  rw [← @associated_eq_self_apply R, LinearMap.map_sum₂, sum_eq_single_of_mem j hj]
  · rw [map_smul, LinearMap.map_smul₂, smul_eq_mul, associated_apply, smul_eq_mul,
      smul_eq_mul, Module.End.smul_def, half_moduleEnd_apply_eq_half_smul]
    ring_nf
  · intro i _ hij
    rw [map_smul, LinearMap.map_smul₂, hv₂ hij]
    module

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

Goal state before:
pp: case zero
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 0 → M
x y : Fin 0
hfxy : f x = f y
h : x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
exact x.elim0

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
⊢ 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
hi

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
⊢ ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
⊢ m ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
hi

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
⊢ ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
i : ℕ
⊢ 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
hi

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 1 ≤ i
⊢ ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
⊢ n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
hi

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
⊢ ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
⊢ n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₂ i), e = 0

Tactic:
hi

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
⊢ ∀ ⦃Y : C⦄ (e : Ext Y S.X₂ i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
⊢ n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₃ i), e = 0

Tactic:
hi

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
⊢ ∀ ⦃Y : C⦄ (e : Ext Y S.X₃ i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i
i : ℕ
⊢ n < ↑i → HasInjectiveDimensionLT X i

Tactic:
hi

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i
i : ℕ
hi : n < ↑i
⊢ HasInjectiveDimensionLT X i
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i
i : ℕ
hi : n < ↑i
this : HasInjectiveDimensionLT Y i
⊢ HasInjectiveDimensionLT X i

Tactic:
exact h.hasInjectiveDimensionLT i

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
d : ℕ
hd : injectiveDimension X = ↑↑d
⊢ HasInjectiveDimensionLE X d

Tactic:
by simpa only [← injectiveDimension_le_iff] using! hd.le

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
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
x y : M
⊢ s.var (update m i (x + y)) = s.var (update m i x) + s.var (update m i y)

Tactic:
have := s.linearCombination_var_relation (.add m i x y)

Goal state after:
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
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
x y : M
this : (Finsupp.linearCombination R s.var) ((relations R ι M).relation (Rels.add m i x y)) = 0
⊢ s.var (update m i (x + y)) = s.var (update m i x) + s.var (update m i y)
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)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app (colimit (F ⋙ evaluation R X))

Tactic:
dsimp
    rw [ι_colimMap_assoc, Functor.whiskerLeft_app, restriction_app]
    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
    erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom)]
    rw [ModuleCat.restrictScalarsId'App_inv_naturality, map_id]
    dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
⊢ Closed F

Tactic:
by
    haveI : ∀ X : Type v₁, PreservesColimits (tensorLeft X) := by infer_instance
    letI : PreservesColimits (tensorLeft F) := ⟨by infer_instance⟩
    have := Presheaf.isLeftAdjoint_of_preservesColimits.{v₁} (tensorLeft F)
    exact Closed.mk _ (Adjunction.ofIsLeftAdjoint (tensorLeft F))

Goal state after: