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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ HasExt C

Tactic:
rw [hasExt_iff.{w}]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ
      (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
        ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
      n₀ n₁ h =
    (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
        hS.δ n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).inv.app S.X₁

Tactic:
rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _),
    assoc, assoc, assoc, Iso.inv_hom_id_app,
    ← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
      (homologyFunctor C (up ℤ) 0).homologySequenceδ
          (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
            ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
          n₀ n₁ h ≫
        (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ =
    HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
      hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁)
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ = 0 ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
d_fst_v _ _ _ _ h,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (-(↑(fst S.f)).v n₀ n₁ h ≫ S.X₁.d n₁ (n₁ + 1)) = 0 ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₁ : Mono (app' ((natAddLEFunctor h).map φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' ((natAddLEFunctor h).map φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
h₀ : Epi (app' ((natAddLEFunctor h).map φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
⊢ Mono (app' ((natAddLEFunctor h).map φ) 2 mono_of_epi_of_mono_of_mono'._proof_4)

Tactic:
exact mono_of_epi_of_mono_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
    (natAddLEFunctor_obj_exact h hR₂) h₀ h₁ h₃

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X : Cᵒᵖ
⊢ ((shiftFunctor Cᵒᵖ n).map
          ((NatIso.op (shiftFunctorCompIsoId C (-n) n ⋯) ≪≫
                  Functor.isoWhiskerRight (shiftFunctorOpIso C n (-n) ⋯).symm (shiftFunctor C n).op).hom.app
            X) ≫
        ((shiftFunctor C n).op.isoWhiskerLeft (shiftFunctorOpIso C n (-n) ⋯) ≪≫
                NatIso.op (shiftFunctorCompIsoId C n (-n) ⋯).symm).hom.app
          ((shiftFunctor Cᵒᵖ n).obj X)).unop =
    (𝟙 ((shiftFunctor Cᵒᵖ n).obj X)).unop

Tactic:
dsimp [shiftFunctorOpIso]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X : Cᵒᵖ
⊢ ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
        𝟙
          (Opposite.unop
            ((shiftFunctor Cᵒᵖ n).obj
              (Opposite.op ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))))))) ≫
      ((shiftFunctor Cᵒᵖ n).map
          (((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
            ((shiftFunctor C n).map (𝟙 ((shiftFunctor Cᵒᵖ n).obj X)).unop).op)).unop =
    𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))) →
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
rintro ⟨T', hT', ⟨e⟩⟩
    refine isomorphic_distinguished _ hT' _ ?_
    exact Iso.unop ((triangleOpEquivalence C).unitIso.app (Opposite.op T') ≪≫
      (triangleOpEquivalence C).inverse.mapIso e.symm)

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
inst✝ : HasDerivedCategory C
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (ConcreteCategory.hom
        ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯))
      x.hom =
    (x.comp hS.extClass h).hom

Tactic:
by
  rw [Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply,
    comp_hom, hS.extClass_hom, ShiftedHom.comp]
  rfl

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]
  rintro _ ⟨r, rfl⟩
  simp only [SetLike.mem_coe, LinearMap.mem_ker, π_relation]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b

Tactic:
exact dvd_add (dvd_mul_of_dvd_right (gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (gcd_dvd_right _ _) _)

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

Goal state before:
pp: R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑(ζ ^ (m % ↑(orderOf ζ)).toNat) = ↑↑ζ ^ m_1

Tactic:
rootsOfUnity.coe_pow

Goal state after:
R : Type u_4
F : Type u_6
k : ℕ
inst✝⁴ : NeZero k
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F R R
inst✝ : MonoidHomClass F R R
σ : F
ζ : ↥(rootsOfUnity k R)
m : ℤ
hm : ∀ (g : ↥(rootsOfUnity k R)), (restrictRootsOfUnity σ k) g = g ^ m
⊢ ∃ m_1, ↑↑ζ ^ (m % ↑(orderOf ζ)).toNat = ↑↑ζ ^ m_1
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
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ det ((map f) g) = (Units.map ↑f) (det g)

Tactic:
by
  ext
  simp only [map,
    Matrix.GeneralLinearGroup.val_det_apply, Units.coe_map, MonoidHom.coe_coe]
  exact Eq.symm (RingHom.map_det f g.1)

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

Goal state before:
pp: n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
t : A
h : t ≠ 0
this : (α : Type u_1) → [Finite α] → Fintype α
⊢ ((∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → w = 0) ↔
    M.Nondegenerate

Tactic:
nondegenerate_def

Goal state after:
n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
t : A
h : t ≠ 0
this : (α : Type u_1) → [Finite α] → Fintype α
⊢ ((∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → v = 0) ∧
      ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → w = 0) ↔
    (∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ M *ᵥ w = 0) → w = 0
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 ℳ
inst✝ : (i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)
r : M
⊢ ∑ x ∈ DFinsupp.support ((decompose ℳ) r), ↑(((decompose ℳ) r) x) =
    ∑ x ∈ DFinsupp.support ((decompose ℳ) r), (decompose ℳ).symm ((of (fun i ↦ ↥(ℳ i)) x) (((decompose ℳ) r) x))

Tactic:
decompose_symm_of

Goal state after:
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 ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p q : P
hp : SetLike.IsHomogeneous ℳ p
hq : SetLike.IsHomogeneous ℳ q
hpq : ∀ (i : ι), ∀ m ∈ ℳ i, m ∈ p ↔ m ∈ q
⊢ p = q

Tactic:
by
  refine SetLike.ext fun m ↦ ?_
  rw [AddSubmonoidClass.IsHomogeneous.mem_iff ℳ p hp,
    AddSubmonoidClass.IsHomogeneous.mem_iff ℳ q hq]
  exact forall_congr' fun i ↦ hpq i _ (decompose ℳ _ i).2

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
n : Type u_11
m : Type u_12
n' : Type u_13
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 n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
⊢ M * (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁' b₂) (B ∘ₗ (toLin b₁' b₁) Mᵀ)

Tactic:
by
  rw [LinearMap.toMatrix₂_comp b₁, toMatrix_toLin, transpose_transpose]

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✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : (coeAlgHom 𝒜).comp decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : ↥(𝒜 i)), decompose ↑x = (of (fun i ↦ ↥(𝒜 i)) i) x
⊢ Function.RightInverse ⇑(DirectSum.coeAddMonoidHom 𝒜) ⇑decompose

Tactic:
suffices decompose.comp (DirectSum.coeAlgHom 𝒜) = AlgHom.id _ _ from AlgHom.congr_fun this

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : SetLike.GradedMonoid 𝒜
decompose : A →ₐ[R] ⨁ (i : ι), ↥(𝒜 i)
right_inv : (coeAlgHom 𝒜).comp decompose = AlgHom.id R A
left_inv : ∀ (i : ι) (x : ↥(𝒜 i)), decompose ↑x = (of (fun i ↦ ↥(𝒜 i)) i) x
⊢ decompose.comp (coeAlgHom 𝒜) = AlgHom.id R (⨁ (i : ι), ↥(𝒜 i))
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 y : A), ↑(((decompose 𝒜) (x * y)) 0) = ↑(((decompose 𝒜) x) 0) * ↑(((decompose 𝒜) y) 0)

Tactic:
refine DirectSum.Decomposition.inductionOn 𝒜 (fun x => ?_) ?_ ?_
    · simp only [zero_mul, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
    · rintro i ⟨c, hc⟩
      refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_
      · simp only [mul_zero, decompose_zero, zero_apply, ZeroMemClass.coe_zero]
      · rintro j ⟨c', hc'⟩
        simp only
        by_cases h : i + j = 0
        · rw [decompose_of_mem_same 𝒜
              (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'),
            decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero.mp h).1 ▸ hc),
            decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero.mp h).2 ▸ hc')]
        · rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h]
          rcases show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero, not_and_or] at h with h' | h'
          · simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul]
          · simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]
      · intro _ _ hd he
        simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he]
    · rintro _ _ ha hb _
      simp only [add_mul, decompose_add, add_apply, AddMemClass.coe_add, ha, hb]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
N' : Type u_8
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : N →ₗ[R] N'
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((f.compQuadraticMap' Q).polarBilin x✝¹) x✝ = ((compr₂ Q.polarBilin f) x✝¹) x✝

Tactic:
rw [polarBilin_apply_apply, compr₂_apply, polarBilin_apply_apply,
    LinearMap.compQuadraticMap_polar]

Goal state after:
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
n : ZMod 2
⊢ Submodule.map involute.toLinearMap (evenOdd Q n) = evenOdd Q n

Tactic:
evenOdd_map_involute

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
n : ZMod 2
⊢ evenOdd Q n = evenOdd Q n
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : IsOrderedAddMonoid ι
inst✝⁴ : DecidableEq ι
inst✝³ : Semiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
r r' : ⨁ (i : ι), ↥(A i)
m n : ι
hr : ∀ i < m, r i = 0
hr' : ∀ i < n, r' i = 0
k : ι
hk : k < m + n
⊢ (r * r') k = 0

Tactic:
classical
  rw [Subtype.ext_iff, ZeroMemClass.coe_zero, coe_mul_apply]
  apply Finset.sum_eq_zero fun x hx ↦ ?_
  obtain (hx | hx) : x.1 < m ∨ x.2 < n := by
    by_contra! ⟨hm, hn⟩
    obtain rfl : x.1 + x.2 = k := by simp_all
    apply lt_irrefl (m + n) <| lt_of_le_of_lt (by gcongr) hk
  all_goals simp [hr, hr', hx]

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

Goal state before:
pp: case e_fst.add
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
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m : M
x y : CliffordAlgebra Q
hx : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1 = x
hy : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) y).1 = y
⊢ (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1 + (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) y).1 = x + y

Tactic:
hx,

Goal state after:
case e_fst.add
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
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m : M
x y : CliffordAlgebra Q
hx : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1 = x
hy : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) y).1 = y
⊢ x + (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) y).1 = x + y
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: case inl.inl
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : (Nat.card α).choose n = 0
⊢ False

Tactic:
rw [Nat.choose_eq_zero_iff] at h
      exact (lt_self_iff_false n).mp (lt_trans h2 h)

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
n : ℕ
f g : M.exteriorPower n ⟶ N
h : mk.postcomp f = mk.postcomp g
⊢ Hom.hom f = Hom.hom g

Tactic:
exact exteriorPower.linearMap_ext h

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ y✝ : CliffordAlgebra 0
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
hy :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) y✝ = g ((liftAlternating f) y✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ + (liftAlternating fun i ↦ g.compAlternatingMap (f i)) y✝ =
    g ((liftAlternating f) x✝) + g ((liftAlternating f) y✝)

Tactic:
hx,

Goal state after:
case add
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ y✝ : CliffordAlgebra 0
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
hy :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) y✝ = g ((liftAlternating f) y✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ g ((liftAlternating f) x✝) + (liftAlternating fun i ↦ g.compAlternatingMap (f i)) y✝ =
    g ((liftAlternating f) x✝) + g ((liftAlternating f) y✝)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ : CliffordAlgebra 0
hx : (liftAlternating (ιMulti R)) x✝ = x✝
hy : (liftAlternating (ιMulti R)) y✝ = y✝
⊢ (liftAlternating (ιMulti R)) x✝ + (liftAlternating (ιMulti R)) y✝ = x✝ + y✝

Tactic:
hx,

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ : CliffordAlgebra 0
hx : (liftAlternating (ιMulti R)) x✝ = x✝
hy : (liftAlternating (ιMulti R)) y✝ = y✝
⊢ x✝ + (liftAlternating (ιMulti R)) y✝ = x✝ + y✝
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 : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
⊢ (map f).toLinearMap.compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

Tactic:
ext m
  exact map_apply_ιMulti _ _

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
⊢ HasInjectiveDimensionLT X n

Tactic:
have : injectiveDimension X ∈ _ := csInf_mem ⟨⊤, by simp⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
this : injectiveDimension X ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}
⊢ HasInjectiveDimensionLT X n
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 = ↑⊤
this : ∃ n, HasInjectiveDimensionLE X n
⊢ False

Tactic:
obtain ⟨n, hn⟩ := this

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
x : M₀
hx : g x = a • m
⊢ mk (g x) (⟨a, aS⟩ * s) = mk m s

Tactic:
hx,

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
x : M₀
hx : g x = a • m
⊢ mk (a • m) (⟨a, aS⟩ * s) = mk m s
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : IsFilteredOrEmpty C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ s ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f)) = s' ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f))

Tactic:
simp [reassoc_of% (IsFiltered.coeq_condition s s')]

Goal state after: