mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ (homEquiv W L₁ L₂) (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj X)

Tactic:
homEquiv_id

Goal state after:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ 𝟙 (L₂.obj X) = 𝟙 (L₂.obj X)
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
← hasSmallLocalizedHom_iff W

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
⊢ HasSmallLocalizedHom W X Y
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : CochainComplex C ℤ
inst✝ : ∀ (i : ℤ), HasHomology K i
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (HomologicalComplex.truncGE K (embeddingUpIntGE n₁)).Acyclic ↔ K.IsLE n₀

Tactic:
rw [acyclic_truncGE_iff_isSupportedOutside,
    (Embedding.embeddingUpInt_areComplementary n₀ n₁ h).isSupportedOutside₂_iff]

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
X : C
S : ShortComplex C
hS : S.ShortExact
n₁ : ℕ
x₁ : Ext X S.X₁ n₁
hx₁ : x₁.comp (mk₀ S.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
this :
  { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
      X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₀),
      g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.Exact
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = x₁

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₁ : ℕ
x₁ : Ext X S.X₁ n₁
hx₁ : x₁.comp (mk₀ S.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
            X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₀),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
                X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₀),
                g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
                  X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₀),
                  g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = 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
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this :
  { X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n), X₃ := AddCommGrpCat.of (Ext X S.X₃ n),
      f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
      zero := ⋯ }.Exact
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = x₂

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
x₂ : Ext X S.X₂ n
hx₂ : x₂.comp (mk₀ S.g) ⋯ = 0
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n),
            X₃ := AddCommGrpCat.of (Ext X S.X₃ n), f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n),
                X₃ := AddCommGrpCat.of (Ext X S.X₃ n), f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯),
                g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext X S.X₁ n), X₂ := AddCommGrpCat.of (Ext X S.X₂ n),
                  X₃ := AddCommGrpCat.of (Ext X S.X₃ n), f := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯),
                  g := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₁, x₁.comp (mk₀ S.f) ⋯ = 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
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
this :
  { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
      X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₁), zero := ⋯ }.Exact
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ : ℕ
x₃ : Ext X S.X₃ n₀
n₁ : ℕ
hn₁ : n₀ + 1 = n₁
hx₃ : x₃.comp hS.extClass hn₁ = 0
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
            X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
            g := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₁), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
                X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
                g := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₁), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext X S.X₂ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₃ n₀),
                  X₃ := AddCommGrpCat.of (Ext X S.X₁ n₁), f := AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X ⋯),
                  g := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₁), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₂, x₂.comp (mk₀ S.g) ⋯ = x₃
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f / (algebraMap R[X] K) g =
    (algebraMap R[X] K) (f /ₘ g) + (algebraMap R[X] K) (f %ₘ g) / (algebraMap R[X] K) g

Tactic:
field_simp

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : g.Monic
hg' : (algebraMap R[X] K) g ≠ 0
⊢ (algebraMap R[X] K) f = (algebraMap R[X] K) g * (algebraMap R[X] K) (f /ₘ g) + (algebraMap R[X] K) (f %ₘ g)
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₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  { 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 hn₁), zero := ⋯ }.Exact
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = x₁

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₀ : ℕ
x₁ : Ext S.X₁ Y n₀
n₁ : ℕ
hn₁ : 1 + n₀ = n₁
hx₁ : hS.extClass.comp x₁ hn₁ = 0
this :
  ∀
    (x₂ :
      ↑{ 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 hn₁), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { 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 hn₁), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { 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 hn₁), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₂, (mk₀ S.f).comp x₂ ⋯ = 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
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this :
  { 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.g).precomp Y ⋯), g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯),
      zero := ⋯ }.Exact
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this :
  ∀
    (x₂ :
      ↑{ 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.g).precomp Y ⋯),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { 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.g).precomp Y ⋯),
                g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { 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.g).precomp Y ⋯),
                  g := AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = 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
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  { 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 (hS.extClass.precomp Y hn₀),
      g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.Exact
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n₁ : ℕ
x₃ : Ext S.X₃ Y n₁
hx₃ : (mk₀ S.g).comp x₃ ⋯ = 0
n₀ : ℕ
hn₀ : 1 + n₀ = n₁
this :
  ∀
    (x₂ :
      ↑{ 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 (hS.extClass.precomp Y hn₀),
            g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { 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 (hS.extClass.precomp Y hn₀),
                g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { 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 (hS.extClass.precomp Y hn₀),
                  g := AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₁, hS.extClass.comp x₁ hn₀ = x₃
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 1 0 * ↑A 0 1 = 1

Tactic:
simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: case refine_1
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ ↑A 1 1 * ↑A 0 0 + -↑A 0 1 * ↑A 1 0 = 1

Tactic:
simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
j : Fin 2
⊢ -↑A 1 0 * ↑A 0 1 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
simp_rw [det_coe A ▸ det_fin_two A.1]
    ring

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
⊢ transvection hij 0 = 1

Tactic:
ext; simp [transvection_coe]

Goal state after:
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
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ f = g

Tactic:
apply (lift Q).symm.injective

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
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ (lift Q).symm f = (lift Q).symm g
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
⊢ P M

Tactic:
obtain ⟨i₀, j₀, hij₀⟩ := exists_pair_ne ι

Goal state after:
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
⊢ P M
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : AddMonoid ι
l : List α
fι : α → ι
head : α
tail : List α
⊢ (head :: tail).dProdIndex fι = (map fι (head :: tail)).sum

Tactic:
simp [List.dProdIndex_eq_map_sum tail fι]

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

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
⊢ r • x =
    { toFun := ⇑((of A 0).comp GAlgebra.toFun), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
change DistribSMul.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x
    apply DFunLike.congr_fun _ x
    ext i xi : 2
    dsimp only [AddMonoidHom.comp_apply, DistribSMul.toAddMonoidHom_apply,
      AddMonoidHom.mul_apply]
    rw [DirectSum.of_mul_of, ← of_smul]
    apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.smul_def r ⟨i, xi⟩)

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
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₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
i' : n
j' : m
⊢ (b₁.repr (l (b₁' i))) i' •> (b₂.repr (r (b₂' j))) j' •> (B (b₁ i')) (b₂ j') =
    (b₁.repr (l (b₁' i))) i' * (B (b₁ i')) (b₂ j') * (b₂.repr (r (b₂' j))) j'

Tactic:
simp only [smul_eq_mul, mul_assoc, mul_comm,
        mul_left_comm]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
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 𝒜
x✝¹ x✝ : A
⊢ ↑(((decompose 𝒜) x✝¹) 0 + ((decompose 𝒜) x✝) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)

Tactic:
AddMemClass.coe_add

Goal state after:
ι : Type u_1
R : Type u_2
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 𝒜
x✝¹ x✝ : A
⊢ ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0) = ↑(((decompose 𝒜) x✝¹) 0) + ↑(((decompose 𝒜) x✝) 0)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ 2 • ⅟2 (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝

Tactic:
← LinearMap.smul_apply,

Goal state after:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ (2 • ⅟2) (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: n : ℕ
β : Type u_2
⊢ Surjective (ofFinEmb n β)

Tactic:
intro ⟨s, hs⟩
  obtain ⟨f : Fin n ↪ β, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])
  exact ⟨f, Subtype.ext hf⟩

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

Goal state before:
pp: α : Type u_1
n m : ℕ
s : ↑(powersetCard α m)
t : ↑(powersetCard α n)
hst : Disjoint ↑s ↑t
⊢ (↑s).disjUnion (↑t) hst ∈ powersetCard α (m + n)

Tactic:
by rw [mem_iff, Finset.card_disjUnion, card_eq s, card_eq t]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ Nat.card ↑(powersetCard α n) = 0 ↔ Nat.card α < n

Tactic:
powersetCard.card,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ (Nat.card α).choose n = 0 ↔ Nat.card α < n
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ 1 < Nat.card ↑(powersetCard α n) ↔ 0 < n ∧ n < Nat.card α

Tactic:
powersetCard.card,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ 1 < (Nat.card α).choose n ↔ 0 < n ∧ n < Nat.card α
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
⊢ x = 0 ∧ r = 0

Tactic:
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := toTrivSqZeroExt_ι _

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 ((ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0
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 : ℕ
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:
· replace hn :=
        congr_arg (ι R (f 0) * ·) <| hn (fun i => f <| Fin.succ i) (i.pred h)
      rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn
      refine (eq_zero_iff_eq_zero_of_add_eq_zero ?_).mp hn
      rw [← add_mul, ι_add_mul_swap, zero_mul]

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

Goal state before:
pp: case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ↑⊤
n : ℕ
hn : injectiveDimension X ≤ ↑n
⊢ False

Tactic:
hd,

Goal state after:
case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ↑⊤
n : ℕ
hn : ↑⊤ ≤ ↑n
⊢ False
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
F : ↥(⋀[R]^n M) →ₗ[R] N
m : Fin n → M
⊢ (alternatingMapLinearEquiv.symm F) m = (F.compAlternatingMap (ιMulti R n)) m

Tactic:
obtain ⟨f, rfl⟩ := alternatingMapLinearEquiv.surjective F
  simp only [LinearEquiv.symm_apply_apply, alternatingMapLinearEquiv_comp_ιMulti]

Goal state after: