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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
⊢ ∃ f', inv (Q.map s) ≫ Q.map g = Q.map f'

Tactic:
have ⟨φ, hφ⟩ := (CochainComplex.singleFunctor C n).map_surjective (e.inv ≫ s)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
φ : A₀ ⟶ A
hφ : (CochainComplex.singleFunctor C n).map φ = e.inv ≫ s
⊢ ∃ f', inv (Q.map s) ≫ Q.map g = Q.map f'
Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
φ : A₀ ⟶ A
hφ : (CochainComplex.singleFunctor C n).map φ = e.inv ≫ s
this✝¹ : IsIso ((singleFunctor C n).map φ)
this✝ : IsIso φ
this : IsIso (e.inv ≫ s)
⊢ ∃ f', inv (Q.map s) ≫ Q.map g = Q.map f'

Tactic:
have : IsIso s := IsIso.of_isIso_comp_left e.inv s

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
φ : A₀ ⟶ A
hφ : (CochainComplex.singleFunctor C n).map φ = e.inv ≫ s
this✝² : IsIso ((singleFunctor C n).map φ)
this✝¹ : IsIso φ
this✝ : IsIso (e.inv ≫ s)
this : IsIso s
⊢ ∃ f', inv (Q.map s) ≫ Q.map g = Q.map f'
Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
φ : A₀ ⟶ A
hφ : (CochainComplex.singleFunctor C n).map φ = e.inv ≫ s
this✝² : IsIso ((singleFunctor C n).map φ)
this✝¹ : IsIso φ
this✝ : IsIso (e.inv ≫ s)
this : IsIso s
⊢ ∃ f', inv (Q.map s) ≫ Q.map g = Q.map f'

Tactic:
exact ⟨inv s ≫ g, by simp⟩

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (equiv W L) (f.shift n a' h) =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((equiv W L) f) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)

Tactic:
dsimp [equiv]
  erw [equiv_shift']
  simp only [Functor.comp_obj, assoc, Iso.inv_hom_id_app, comp_id, Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono (homologyMap φ.τ₁ j)

Tactic:
by
    have := h₃ j hij
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this : Mono (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
⊢ Epi (homologyMap φ.τ₁ j)

Tactic:
by
    have := h₃ j hij
    infer_instance

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ r • G.map e.inv ≫ G.map e.hom = r • 𝟙 (G.obj X)

Tactic:
← G.map_comp,

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ r • G.map (e.inv ≫ e.hom) = r • 𝟙 (G.obj X)
Module: Mathlib.Algebra.CharP.Reduced

Goal state before:
pp: case e'_1.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p k) 1 = 1

Tactic:
apply map_one

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

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Finite ι
⊢ (Pi.basisFun R ι).toMatrix = transpose

Tactic:
ext M i j

Goal state after:
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Finite ι
M : ι → ι → R
i j : ι
⊢ (Pi.basisFun R ι).toMatrix M i j = Mᵀ i j
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommMonoid R
inst✝ : NeZero k
x : R
x✝ : x ∈ val '' ↑(rootsOfUnity k R)
y : Rˣ
hy1 : y ∈ ↑(rootsOfUnity k R)
hy2 : ↑y = x
⊢ x ∈ {z | z ^ k = 1}

Tactic:
by rw [← hy2]; exact (mem_rootsOfUnity' k y).mp hy1

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

Goal state before:
pp: case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b, 0 < v b
⊢ ∃ b, 0 < (-1 • v) b

Tactic:
simp_rw [not_exists, not_lt] at h_sup

Goal state after:
case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ ∃ b, 0 < (-1 • v) b
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (i : n), 0 < ∑ j, A i j
⊢ ∀ (j : n), 0 < ∑ i, Aᵀ i j

Tactic:
simp_rw [Matrix.transpose_apply]
    exact h2

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

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
hn : IsEmpty n
⊢ ↥(center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)

Tactic:
rw [center_eq_bot_of_subsingleton, Fintype.card_eq_zero, max_eq_right_of_lt zero_lt_one,
      rootsOfUnity_one]

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
hn : IsEmpty n
⊢ ↥⊥ ≃* ↥⊥
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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
y : CliffordAlgebra Q
⊢ x * (ι Q) a * ((ι Q) b * y) = -(x * (ι Q) b * ((ι Q) a * y))

Tactic:
rw [mul_ι_mul_ι_mul_comm, h.polar_eq_zero, map_zero, zero_mul, zero_sub]

Goal state after:
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ (head :: tail).dProd fι fA = (map fA (head :: tail)).prod

Tactic:
List.dProd_cons,

Goal state after:
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA) = (map fA (head :: tail)).prod
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
⊢ ↑((head :: tail).dProd fι fA) = (List.map (fun a ↦ ↑(fA a)) (head :: tail)).prod

Tactic:
List.dProd_cons,

Goal state after:
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → ↥(A (fι a))
l : List α
head : α
tail : List α
⊢ ↑(GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) = (List.map (fun a ↦ ↑(fA a)) (head :: tail)).prod
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_2
R : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : CommMonoid R
inst✝¹ : AddCommMonoid ι
A : ι → S
inst✝ : GradedMonoid A
κ : Type u_5
i : κ → ι
g : κ → R
F : Finset κ
hF : ∀ k ∈ F, g k ∈ A (i k)
⊢ ∏ k ∈ F, g k ∈ A (∑ k ∈ F, i k)

Tactic:
by
  classical
  induction F using Finset.induction_on
  · simp [GradedOne.one_mem]
  · case insert j F' hF2 h3 =>
    rw [Finset.prod_insert hF2, Finset.sum_insert hF2]
    apply SetLike.mul_mem_graded (by grind)
    grind

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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A) One.one) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
simp only [One.one]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A) ((of A 0) GradedMonoid.GOne.one)) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A).flip One.one) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)

Tactic:
simp only [One.one]

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ((mulHom A).flip ((of A 0) GradedMonoid.GOne.one)) ((of A i) xi) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) xi)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f g : M → N
x y : M
⊢ polar (f + g) x y = polar f x y + polar g x y

Tactic:
simp only [polar, Pi.add_apply]

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f g : M → N
x y : M
⊢ f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix m m' R
⊢ (toMatrix₂ b₁ b₂) B * M = (toMatrix₂ b₁ b₂) B * (toMatrix b₂' b₂) ((toLin b₂' b₂) M)

Tactic:
toMatrix_toLin

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix m m' R
⊢ (toMatrix₂ b₁ b₂) B * M = (toMatrix₂ b₁ b₂) B * M
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
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm)
      (Submodule.map ((lift Q) ⟨↑(MulOpposite.opLinearEquiv R) ∘ₗ ι Q, ⋯⟩).toLinearMap (ι Q).range) =
    (ι Q).range

Tactic:
ι_range_map_lift,

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
⊢ Submodule.map (↑(MulOpposite.opLinearEquiv R).symm) (↑(MulOpposite.opLinearEquiv R) ∘ₗ ι Q).range = (ι Q).range
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
i' : ZMod 2
x' : CliffordAlgebra Q
hx' : x' ∈ evenOdd Q i'
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x' = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x', hx'⟩

Tactic:
induction hx' using Submodule.iSup_induction' with
  | mem i x hx =>
    obtain ⟨i, rfl⟩ := i
    dsimp only [Subtype.coe_mk] at hx
    induction hx using Submodule.pow_induction_on_left' with
    | algebraMap r =>
      rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
    | add x y i hx hy ihx ihy =>
      rw [map_add, ihx, ihy, ← map_add]
      rfl
    | mem_mul m hm i x hx ih =>
      obtain ⟨_, rfl⟩ := hm
      rw [map_mul, ih, lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.of_mul_of]
      refine DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext ?_ ?_) <;>
        dsimp only [GradedMonoid.mk, Subtype.coe_mk]
      · rw [Nat.succ_eq_add_one, add_comm, Nat.cast_add, Nat.cast_one]
      rfl
  | zero =>
    rw [map_zero]
    apply Eq.symm
    apply DFinsupp.single_eq_zero.mpr; rfl
  | add x y hx hy ihx ihy =>
    rw [map_add, ihx, ihy, ← map_add]; rfl

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
⊢ M →ₗ[R] ⨁ (i : ZMod 2), ↥(evenOdd Q i)

Tactic:
apply GradedAlgebra.ι Q

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

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

Tactic:
rw [← add_mul, ι_add_mul_swap, zero_mul]

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 : ι
r : R
x : M
this :
  (Finsupp.linearCombination R s.var) (Finsupp.single (update m i (r • x)) 1 - r • Finsupp.single (update m i x) 1) = 0
⊢ s.var (update m i (r • x)) = r • s.var (update m i x)

Tactic:
Finsupp.smul_single,

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 : ι
r : R
x : M
this :
  (Finsupp.linearCombination R s.var) (Finsupp.single (update m i (r • x)) 1 - Finsupp.single (update m i x) (r • 1)) =
    0
⊢ s.var (update m i (r • x)) = r • s.var (update m i x)
Module: Mathlib.Algebra.Category.ModuleCat.Localization

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Submonoid R
M₁ M₂ M₃ : ModuleCat R
f₁ : M₁ ⟶ M₂
f₂ : M₂ ⟶ M₃
h₁ : IsLocalizedModule S (Hom.hom f₁)
h₂ : IsLocalizedModule S (Hom.hom (f₁ ≫ f₂))
⊢ IsIso f₂

Tactic:
by
  have : Function.Bijective f₂.hom := by
    rw [← IsLocalizedModule.linearEquiv_of_isLocalizedModule_comp S f₁.hom f₂.hom]
    exact (IsLocalizedModule.linearEquiv ..).bijective
  simpa [ConcreteCategory.isIso_iff_bijective]

Goal state after:
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
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ (c.ι.app j).app X ≫ m.app X = (s.ι.app j).app X

Tactic:
rw [← hm]

Goal state after:
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
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ (c.ι.app j).app X ≫ m.app X = (c.ι.app j ≫ m).app X
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 Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ (F.obj j).map (f ≫ g) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv

Tactic:
map_comp,

Goal state after:
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 Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ ((F.obj j).map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((F.obj j).map g) ≫
          (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (f ≫ g))) ⋯).inv.app
            ((F.obj j).obj Z)) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))).map (colimit.ι (F ⋙ evaluation R Z) j) =
    (F.whiskerLeft (restriction R f)).app j ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
          ((F.whiskerLeft (restriction R g)).app j ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫
        (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
            (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ M.ιFreeYonedaCoproduct m ≫ M.fromFreeYonedaCoproduct = m.fromFreeYoneda

Tactic:
apply Sigma.ι_desc

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W : C
g : W ⟶ Y
⊢ (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g

Tactic:
· rintro ⟨W, h, k, hk, comm⟩
    have := R.hasPullback f hk
    exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩

Goal state after: