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 Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
              (shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y) ≫ g).unop ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
erw [← NatTrans.naturality]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
              (shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          (((shiftFunctor Cᵒᵖ a ⋙ (shiftFunctor C a).op).map g ≫
                (opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : Cᵒᵖ
x : unop A ⟶ (shiftFunctor C n₀).obj T.obj₃
⊢ (ConcreteCategory.hom ((preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h)) x =
    x ≫ (shiftFunctor C n₀).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n₀ n₁ ⋯).inv.app T.obj₁

Tactic:
by
  apply Category.assoc

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

Goal state before:
pp: C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝⁹ : AddMonoid A
inst✝⁸ : AddMonoid B
inst✝⁷ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
D : Type u_4
inst✝⁶ : Category.{v_2, u_4} D
inst✝⁵ : HasShift D B
F : C ⥤ D
inst✝⁴ : F.CommShift B
G✝ : C ⥤ D
inst✝³ : G✝.CommShift B
E : Type u_5
inst✝² : Category.{v_3, u_5} E
inst✝¹ : HasShift E B
G : D ⥤ E
inst✝ : G.CommShift B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ G.map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      G.map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app (F.obj x✝) ≫ (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj (F.obj x✝)) =
    G.map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      G.map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        G.map ((pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj x✝)) ≫
          G.map ((pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).hom.app (F.obj x✝)) ≫
            (commShiftIso G (φ x✝¹)).hom.app (F.obj x✝) ≫
              (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj (F.obj x✝))

Tactic:
slice_rhs 3 4 => rw [← G.map_comp, Iso.inv_hom_id_app]

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
E : Type u_5
inst✝² : Category.{v_3, u_5} E
inst✝¹ : HasShift E B
G : D ⥤ E
inst✝ : G.CommShift B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ G.map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      G.map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app (F.obj x✝) ≫ (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj (F.obj x✝)) =
    G.map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      G.map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        (G.map (𝟙 ((shiftFunctor D (φ x✝¹)).obj (F.obj x✝))) ≫ (commShiftIso G (φ x✝¹)).hom.app (F.obj x✝)) ≫
          (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj (F.obj x✝))
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
L M N : C
f : M ⟶ N
hf : Mono f
⊢ Function.Injective ⇑((mk₀ f).postcomp L ⋯)

Tactic:
rw [← AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
f : M ⟶ N
hf : Mono f
⊢ ∀ x ∈ ((mk₀ f).postcomp L ⋯).ker, x = 0
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
π : (relations.G →₀ A) →ₗ[A] M
hπ : π ∘ₗ relations.map = 0
⊢ (ofπ' π hπ).π = π

Tactic:
simp [ofπ']

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
h : solution.IsPresentationCore
e : relations.Quotient ≃ₗ[A] M := LinearEquiv.ofLinearMap solution.fromQuotient (h.down.desc (ofQuotient relations)) ⋯ ⋯
⊢ Function.Bijective ⇑solution.fromQuotient

Tactic:
exact e.bijective

Goal state after:
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₁
⊢ { X₁ := AddCommGrpCat.of (Ext S.X₂ Y n₀), X₂ := AddCommGrpCat.of (Ext S.X₁ Y n₀),
      X₃ := AddCommGrpCat.of (Ext S.X₃ Y n₁), f := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp Y h), zero := ⋯ }.Exact

Tactic:
by
  let := HasDerivedCategory.standard C
  have := (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequence_exact₃ _
    (op_distinguished _ hS.singleTriangle_distinguished) n₀ n₁ (by lia)
  rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
  apply Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv)
    (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv) (H := this)
  · ext; apply singleFunctor_map_comp_hom (C := C)
  · ext; dsimp; apply preadditiveYoneda_homologySequenceδ_singleTriangle_apply

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

Goal state before:
pp: ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
⊢ b.toMatrix (x • w) = (Algebra.leftMulMatrix b) x * b.toMatrix w

Tactic:
by
  ext
  rw [Basis.toMatrix_apply, Pi.smul_apply, smul_eq_mul, ← Algebra.leftMulMatrix_mulVec_repr]
  rfl

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, (∑ i, w i • A i x) • v x = 0
hv : w ᵥ* A = 0
w' : ι → R
⊢ w ⬝ᵥ A *ᵥ w' = 0

Tactic:
simpa [Matrix.dotProduct_mulVec] using congr_arg (fun x ↦ dotProduct x w') hv

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

Goal state before:
pp: ι : 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
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
ι : 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
inst✝² : Finite ι
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
v : Basis ι' R M
i : ι'
val✝ : Fintype ι
⊢ ((toLin v e) (e.toMatrix ⇑v)) (v i) = LinearMap.id (v i)
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : 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
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : Fintype ι
e : Basis ι R M
⊢ RightInverse (fun m j ↦ ∑ i, m i j • e i) e.toMatrix

Tactic:
intro m
    ext k l
    simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply,
      LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case intro
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
val✝ : Fintype R
⊢ IsField R

Tactic:
exact @Field.toIsField R (@Fintype.fieldOfDomain R _ _ (Classical.decEq R) _)

Goal state after:
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
L M N : C
g : M ⟶ N
hg : Epi g
⊢ Function.Injective ⇑((mk₀ g).precomp L ⋯)

Tactic:
rw [← AddMonoidHom.ker_eq_bot_iff, AddSubgroup.eq_bot_iff_forall]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
⊢ ∀ x ∈ ((mk₀ g).precomp L ⋯).ker, x = 0
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:
by
  rw [mul_ι_mul_ι_mul_comm, h.polar_eq_zero, map_zero, zero_mul, zero_sub]

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
⊢ ((mk₂'ₛₗ σ₁ σ₂ (fun v w ↦ ∑ i, ∑ j, σ₂ (w j) •> σ₁ (v i) •> f i j) ⋯ ⋯ ⋯ ⋯) (Pi.single i 1)) (Pi.single j 1) = f i j

Tactic:
mk₂'ₛₗ_apply

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
⊢ ∑ 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.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₂
⊢ ((mk₂'ₛₗ σ₁ σ₂ (fun v w ↦ ∑ i, ∑ j, σ₂ (w j) •> σ₁ (v i) •> M i j) ⋯ ⋯ ⋯ ⋯) x) y =
    ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j

Tactic:
mk₂'ₛₗ_apply

Goal state after:
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₂
⊢ ∑ i, ∑ j, σ₂ (y j) •> σ₁ (x i) •> M i j = ∑ i, ∑ j, σ₁ (x i) •> σ₂ (y j) •> M i j
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
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ (B x) y = ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)

Tactic:
← b₁.sum_repr x,

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
n : Type u_11
m : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
σ₁ σ₂ : R →+* R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R
x : M₁
y : M₂
⊢ (B (∑ i, (b₁.repr x) i •> b₁ i)) y = ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ (toMatrix₂ b₁ b₂) B *ᵥ ⇑σ₂ ∘ ⇑(b₂.repr y)
Module: Mathlib.Algebra.DirectSum.Decomposition

Goal state before:
pp: ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ (decompose ℳ) ↑x = (of (fun i ↦ ↥(ℳ i)) i) x

Tactic:
← decompose_symm_of _,

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
i : ι
x : ↥(ℳ i)
⊢ (decompose ℳ) ((decompose ℳ).symm ((of (fun i ↦ ↥(ℳ i)) i) x)) = (of (fun i ↦ ↥(ℳ i)) i) x
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 j : ι} (ai : A i) (aj : A j),
    ((↑F).comp (of A (i + j))) (GradedMonoid.GMul.mul ai aj) = ((↑F).comp (of A i)) ai * ((↑F).comp (of A j)) aj

Tactic:
by
      intro i j ai aj
      simp only [AddMonoidHom.comp_apply, AddMonoidHom.coe_coe]
      rw [← F.map_mul (of A i ai), of_mul_of ai]

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
inst✝⁵ : Monoid S
inst✝⁴ : Monoid T
inst✝³ : DistribMulAction S N
inst✝² : DistribMulAction T N
inst✝¹ : SMulCommClass S R N
inst✝ : SMulCommClass T R N
a : S
Q : QuadraticMap R M N
b : R
x : M
⊢ (a • ⇑Q) (b • x) = (b * b) • (a • ⇑Q) x

Tactic:
rw [Pi.smul_apply, Q.map_smul, Pi.smul_apply, smul_comm]

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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
m : M
⊢ (⟨⅟2, ⋯⟩ • 1 * 2) m = 1 m

Tactic:
dsimp [Submonoid.smul_def]

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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
m : M
⊢ ⅟2 • 2 • m = m
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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
m : M
⊢ (2 * ⟨⅟2, ⋯⟩ • 1) m = 1 m

Tactic:
dsimp [Submonoid.smul_def]

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✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Invertible 2
m : M
⊢ 2 • ⅟2 • m = m
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a : ↥(𝒜 i)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) i) a * (decompose 𝒜) b) n) = if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0

Tactic:
coe_of_mul_apply

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
a : ↥(𝒜 i)
⊢ (if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0) = if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case neg
ι : 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support r'
⊢ 0 = ↑r * ↑(r' j)

Tactic:
DFinsupp.notMem_support_iff.mp h,

Goal state after:
case neg
ι : 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
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
j n : ι
H : ∀ (x : ι), i + x = n ↔ x = j
h : j ∉ DFinsupp.support r'
⊢ 0 = ↑r * ↑0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case neg
ι : 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∉ DFinsupp.support r
⊢ 0 = ↑(r j) * ↑r'

Tactic:
DFinsupp.notMem_support_iff.mp h,

Goal state after:
case neg
ι : 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
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
j n : ι
H : ∀ (x : ι), x + i = n ↔ x = j
h : j ∉ DFinsupp.support r
⊢ 0 = ↑0 * ↑r'
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] CliffordAlgebra Q × N →ₗ[R] N
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)

Tactic:
have v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
  have l := v_mul.compl₂ (LinearMap.fst _ _ N)
  exact
    { toFun := fun m => (l m).prod (f m)
      map_add' := fun v₂ v₂ =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_add _ _) x) (LinearMap.congr_fun (f.map_add _ _) x)
      map_smul' := fun c v =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_smul _ _) x)
            (LinearMap.congr_fun (f.map_smul _ _) x) }

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

Goal state before:
pp: case mem.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x✝ : CliffordAlgebra Q
i✝ : ℕ
x y : CliffordAlgebra Q
i : ℕ
hx : x ∈ (ι Q).range ^ i
hy : y ∈ (ι Q).range ^ i
ihx : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x, ⋯⟩
ihy : ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) y = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨y, ⋯⟩
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) (x + y) = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑i) ⟨x + y, ⋯⟩

Tactic:
| add x y i hx hy ihx ihy =>

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

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
⊢ Nontrivial ↑(powersetCard α n)

Tactic:
rw [Set.nontrivial_coe_sort, ← Set.one_lt_ncard_iff_nontrivial, ← Nat.card_coe_set_eq,
      powersetCard.card]

Goal state after:
case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
⊢ 1 < (Nat.card α).choose n
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case refine_2
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r

Tactic:
· rintro ⟨rfl, rfl⟩
    rw [map_zero, map_zero]

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

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

Tactic:
rw [← hv, ι_leftInverse]

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
inst✝ : HasInjectiveDimensionLT X 0
⊢ IsZero X

Tactic:
by
  let := HasExt.standard C
  rw [IsZero.iff_id_eq_zero]
  apply Ext.homEquiv₀.symm.injective
  simpa only [Ext.homEquiv₀_symm_apply, Ext.mk₀_zero]
    using Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT _ 0 (by rfl)

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 Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : n ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i}
⊢ n ∈ insert ⊤ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}

Tactic:
simp only [Set.mem_ofPred_eq, not_top_lt, IsEmpty.forall_iff, implies_true,
      Set.insert_eq_of_mem] at hn ⊢

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 : ℕ), n < ↑i → HasInjectiveDimensionLT X i