mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
⊢ IsIso ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv)

Tactic:
have : IsIso (K.pOpcycles (e.f i)) := K.isIso_pOpcycles _ _ rfl (by
      obtain ⟨hi₁, hi₂⟩ := hi
      apply IsZero.eq_of_src (K.isZero_X_of_isStrictlySupported e _
        (fun j hj ↦ hi₂ j (by simpa only [hj] using hi₁))))

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi : e.BoundaryGE i
this : IsIso (K.pOpcycles (e.f i))
⊢ IsIso ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv)
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case left.inl.inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
j₂ : ι₂
h : fromSum e₁ e₂ (Sum.inl i₁) = fromSum e₁ e₂ (Sum.inr j₂)
⊢ Sum.inl i₁ = Sum.inr j₂

Tactic:
exact (ac.disjoint _ _ h).elim

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

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

Tactic:
by
  apply LocalizerMorphism.id_homMap

Goal state after:
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:
by
  rw [hasExt_iff.{w}]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := ⋯
h : (singleFunctor C 0).FullyFaithful
e : (X ⟶ Y) ≃ Ext X Y 0 := ⋯
f : X ⟶ Y
⊢ (ShiftedHom.homEquiv 0 ⋯) (h.homEquiv f) = homEquiv (mk₀ f)

Tactic:
symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := ⋯
h : (singleFunctor C 0).FullyFaithful
e : (X ⟶ Y) ≃ Ext X Y 0 := ⋯
f : X ⟶ Y
⊢ homEquiv (mk₀ f) = (ShiftedHom.homEquiv 0 ⋯) (h.homEquiv f)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
α : ↑(AddCommGrpCat.of (Ext X X✝ n))
⊢ Ext.comp α ((Ext.mk₀ f).comp (Ext.mk₀ f') ⋯) ⋯ = (Ext.comp α (Ext.mk₀ f) ⋯).comp (Ext.mk₀ f') ⋯

Tactic:
symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
α : ↑(AddCommGrpCat.of (Ext X X✝ n))
⊢ (Ext.comp α (Ext.mk₀ f) ⋯).comp (Ext.mk₀ f') ⋯ = Ext.comp α ((Ext.mk₀ f).comp (Ext.mk₀ f') ⋯) ⋯
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : ↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁)
⊢ (Ext.mk₀ f.unop).comp (Ext.comp α (Ext.mk₀ g) ⋯) ⋯ = ((Ext.mk₀ f.unop).comp α ⋯).comp (Ext.mk₀ g) ⋯

Tactic:
symm

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : ↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁)
⊢ ((Ext.mk₀ f.unop).comp α ⋯).comp (Ext.mk₀ g) ⋯ = (Ext.mk₀ f.unop).comp (Ext.comp α (Ext.mk₀ g) ⋯) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
S : ShortComplex (CochainComplex C ℤ)
⊢ (mapHomologicalComplexIso S.f F).hom ≫ descShortComplex (S.map (F.mapHomologicalComplex (up ℤ))) =
    (F.mapHomologicalComplex (up ℤ)).map (descShortComplex S)

Tactic:
symm

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
S : ShortComplex (CochainComplex C ℤ)
⊢ (F.mapHomologicalComplex (up ℤ)).map (descShortComplex S) =
    (mapHomologicalComplexIso S.f F).hom ≫ descShortComplex (S.map (F.mapHomologicalComplex (up ℤ)))
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C (a + b)).obj X) ≫
      G.map ((Functor.CommShift.isoAdd e₁ f₁).hom.app X) ≫ (Functor.CommShift.isoAdd e₂ f₂).hom.app (F.obj X)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoAdd_hom_app,
    Functor.map_comp, assoc, unit_naturality_assoc]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    (shiftFunctorAdd C a b).hom.app X ≫
      adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        G.map (f₁.hom.app ((shiftFunctor C a).obj X)) ≫
          G.map ((shiftFunctor D b).map (e₁.hom.app X)) ≫
            G.map ((shiftFunctorAdd D a b).inv.app (F.obj X)) ≫
              G.map ((shiftFunctorAdd D a b).hom.app (F.obj X)) ≫
                f₂.hom.app ((shiftFunctor D a).obj (F.obj X)) ≫
                  (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫ (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X))
Module: Mathlib.CategoryTheory.Shift.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : F.CommShift A
inst✝⁶ : G.CommShift A
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
F' : D ⥤ E
G' : E ⥤ D
adj' : F' ⊣ G'
inst✝⁴ : HasShift E A
inst✝³ : F'.CommShift A
inst✝² : G'.CommShift A
inst✝¹ : adj.CommShift A
inst✝ : adj'.CommShift A
⊢ NatTrans.CommShift (adj.comp adj').unit A

Tactic:
by
    rw [comp_unit]
    infer_instance

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
τ : F ⟶ G
inst✝ : CommShift τ B
x✝ : A
⊢ (commShiftIso (PullbackShift.functor φ F) x✝).hom ≫
      whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift D φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natTrans φ τ) ≫
      (commShiftIso (PullbackShift.functor φ G) x✝).hom

Tactic:
by
    ext
    dsimp [PullbackShift.natTrans]
    simp only [commShiftPullback_iso_eq φ _ _ _ rfl, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, comp_app, whiskerRight_app, whiskerLeft_app,
      assoc]
    rw [← τ.naturality_assoc]
    simp [← NatTrans.shift_app_comm_assoc]

Goal state after:
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 ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ (shiftFunctor C a).obj B
⊢ (ConcreteCategory.hom ((preadditiveYoneda.obj B).shiftMap f a a' h)) z = ((ShiftedHom.opEquiv n).symm f).comp z ⋯

Tactic:
symm

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ (shiftFunctor C a).obj B
⊢ ((ShiftedHom.opEquiv n).symm f).comp z ⋯ = (ConcreteCategory.hom ((preadditiveYoneda.obj B).shiftMap f a a' h)) z
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
mem_ann : r ∈ Module.annihilator R ↑N
n : ℕ
⊢ AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯) = 0

Tactic:
by
  ext h
  have : r • 𝟙 N = 0 := by
    simp [← ModuleCat.lsmul_eq_smul_id, Module.mem_annihilator_iff_lsmul_eq_zero.mp mem_ann]
  have smul_eq : r • h = (Ext.mk₀ (r • 𝟙 N)).comp h (zero_add n) := by simp [Ext.mk₀_smul]
  simp [Ext.mk₀_smul, this, smul_eq]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : DivisionCommMonoid G
k l : ℕ
inst✝³ : CommMonoid R
inst✝² : CommMonoid S
inst✝¹ : FunLike F R S
inst✝ : MonoidHomClass F R S
σ : F
n : ℕ
ξ₁ ξ₂ : ↥(rootsOfUnity n R)
⊢ ↑⟨(Units.map ↑σ) ↑(ξ₁ * ξ₂), ⋯⟩ = ↑(⟨(Units.map ↑σ) ↑ξ₁, ⋯⟩ * ⟨(Units.map ↑σ) ↑ξ₂, ⋯⟩)

Tactic:
simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]

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
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ (↑g).det ≠ 0

Tactic:
rw [g.det_coe]

Goal state after:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
g : SpecialLinearGroup n R
⊢ 1 ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1

Tactic:
rwa [det_fin_two] at hm

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![a, -v; b, u].det = 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ a * u - -v * b = u * a + v * b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, a; -u, b].det = 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - a * -u = u * a + v * b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![a, b; -v, u].det = 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ a * u - b * -v = u * a + v * b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, -u; a, b].det = 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
i : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - -u * a = u * a + v * b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ * ∏ x with x ≠ i₀, D x = 1
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D

Tactic:
mul_eq_one_iff_eq_inv₀ (by grind),

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = (∏ x with x ≠ i₀, D x)⁻¹
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) = D
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
⊢ 0 - x * (ι Q) b * ((ι Q) a * y) = -(x * (ι Q) b * ((ι Q) a * y))

Tactic:
zero_sub

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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
y : CliffordAlgebra Q
⊢ -(x * (ι Q) b * ((ι Q) a * y)) = -(x * (ι Q) b * ((ι Q) a * y))
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ⊢ S⁻¹ = -S

Tactic:
decide

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
a : A 0
n : ℕ
⊢ (of A 0) (a ^ (n + 1)) = (of A 0) a ^ (n + 1)

Tactic:
by rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]

Goal state after:
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
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✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ ((toMatrix c₁ b₁) id)ᵀ * (toMatrix₂ b₁ b₂) B * (toMatrix c₂ b₂) id = (toMatrix₂ c₁ c₂) B

Tactic:
← LinearMap.toMatrix₂_compl₁₂,

Goal state after:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
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✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
c₁ : Basis n' R M₁
c₂ : Basis m' R M₂
B : M₁ →ₗ[R] M₂ →ₗ[R] R
⊢ (toMatrix₂ c₁ c₂) (B.compl₁₂ id id) = (toMatrix₂ c₁ c₂) B
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'
M : Matrix n m R
P : Matrix n n' R
Q : Matrix m m' R
⊢ (toMatrix₂ b₁' b₂') (((toLinearMap₂ b₁ b₂) M).compl₁₂ ((toLin b₁' b₁) P) ((toLin b₂' b₂) Q)) =
    (toMatrix₂ b₁' b₂') ((toLinearMap₂ b₁' b₂') (Pᵀ * M * Q))

Tactic:
by
      simp only [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, LinearMap.toMatrix₂_toLinearMap₂,
        toMatrix_toLin]

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✝¹ : AddCommMonoid P
inst✝ : Module R P
Q : QuadraticMap R N P
f : M →ₗ[R] N
B : BilinMap R N P
h : ∀ (x y : N), Q (x + y) = Q x + Q y + (B x) y
x y : M
⊢ Q (f x + f y) = Q (f x) + Q (f y) + ((LinearMap.compl₁₂ B f f) x) y

Tactic:
exact h (f x) (f y)

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 : M
⊢ (DirectSum.coeAlgHom (evenOdd Q)) (((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((ι Q) m)) = (ι Q) m

Tactic:
rw [lift_ι_apply, GradedAlgebra.ι_apply Q, DirectSum.coeAlgHom_of, Subtype.coe_mk]

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

Goal state before:
pp: α : Type u_1
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
a b : α
hab : a ≠ b
ha' : ↑n ≤ {b}ᶜ.encard
s : Set α
has : {a} ⊆ s
has' : s ⊆ {b}ᶜ
hs : s.encard = ↑n
this : s.Finite
⊢ a ∈ ⟨this.toFinset, ⋯⟩

Tactic:
simpa using has

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
f : Fin n ↪o I
⊢ (fun s ↦ (↑s).orderEmbOfFin ⋯) ((fun f ↦ ofFinEmb n I f.toEmbedding) f) = f

Tactic:
symm

Goal state after:
n : ℕ
I : Type u_1
inst✝ : LinearOrder I
f : Fin n ↪o I
⊢ f = (fun s ↦ (↑s).orderEmbOfFin ⋯) ((fun f ↦ ofFinEmb n I f.toEmbedding) f)
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
x : M
⊢ (ι R) x = 0 ↔ x = 0

Tactic:
← ι_inj R x 0,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ (ι R) x = (ι R) 0
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
⊢ r • 0 = 0

Tactic:
colimit_zero_eq _ (IsFiltered.nonempty.some : J),

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
⊢ r • M.mk F ⟨⋯.some, 0⟩ = M.mk F ⟨⋯.some, 0⟩
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasInjectiveDimensionLT X 0
⊢ ⊥ < ↑0

Tactic:
decide

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

Goal state before:
pp: case bot
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ⊥
⊢ ⊥ ≠ ⊤ ↔ ∃ n, HasInjectiveDimensionLE X n

Tactic:
simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]

Goal state after:
case bot
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : injectiveDimension X = ⊥
⊢ ∃ n, HasInjectiveDimensionLE X n
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
x✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
⊢ ∀ {X Y : J₂ × J₁} (f : X ⟶ Y),
    ((externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).obj x✝).map f ≫
        (β_ (x✝.1.obj ((Prod.swap J₂ J₁).obj Y).1) (x✝.2.obj ((Prod.swap J₂ J₁).obj Y).2)).hom =
      (β_ (x✝.1.obj ((Prod.swap J₂ J₁).obj X).1) (x✝.2.obj ((Prod.swap J₂ J₁).obj X).2)).hom ≫
        ((Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).obj x✝).map f

Tactic:
simp [whisker_exchange]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
x✝¹ : X✝ ⟶ Y✝
x✝ : J₂ × J₁
⊢ ((externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).map x✝¹ ≫
          (NatIso.ofComponents
              (fun x ↦ β_ (Y✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (Y✝.2.obj ((Prod.swap J₂ J₁).obj x).2)) ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents (fun x ↦ β_ (X✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (X✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
              ⋯).hom ≫
          (Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).map x✝¹).app
      x✝

Tactic:
simp [whisker_exchange]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ colim.obj (⊤_ C ⥤ Type u) ≅ ⊤_ Type u

Tactic:
symm

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ ⊤_ Type u ≅ colim.obj (⊤_ C ⥤ Type u)