mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
a b : A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorAdd C a b).inv.app (Opposite.unop x✝))).op ≫
      ((commShiftIso F b).inv.app ((shiftFunctor C a).obj (Opposite.unop x✝))).op ≫
        ((shiftFunctor D b).map ((commShiftIso F a).inv.app (Opposite.unop x✝))).op ≫
          ((shiftFunctorAdd D a b).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorAdd (OppositeShift C A) a b).hom.app x✝) ≫
      ((commShiftIso F b).inv.app (Opposite.unop ((shiftFunctor (OppositeShift C A) a).obj x✝))).op ≫
        (shiftFunctor (OppositeShift D A) b).map ((commShiftIso F a).inv.app (Opposite.unop x✝)).op ≫
          (shiftFunctorAdd (OppositeShift D A) a b).inv.app ((OppositeShift.functor A F).obj x✝)

Tactic:
oppositeShiftFunctorAdd_inv_app,

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
a b : A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorAdd C a b).inv.app (Opposite.unop x✝))).op ≫
      ((commShiftIso F b).inv.app ((shiftFunctor C a).obj (Opposite.unop x✝))).op ≫
        ((shiftFunctor D b).map ((commShiftIso F a).inv.app (Opposite.unop x✝))).op ≫
          ((shiftFunctorAdd D a b).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorAdd (OppositeShift C A) a b).hom.app x✝) ≫
      ((commShiftIso F b).inv.app (Opposite.unop ((shiftFunctor (OppositeShift C A) a).obj x✝))).op ≫
        (shiftFunctor (OppositeShift D A) b).map ((commShiftIso F a).inv.app (Opposite.unop x✝)).op ≫
          ((shiftFunctorAdd D a b).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op
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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((Functor.commShiftIso F (-a)).inv.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((Functor.commShiftIso F (-a)).hom.app ((shiftFunctor C a).obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
              G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
                G.map ((shiftFunctor D a).map (adj.counit.app Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
slice_lhs 3 4 => rw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app]

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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
a : A
inst✝ : F.CommShift A
Y : D
h : -a + a = 0
⊢ adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        ((G.map ((shiftFunctor D a).map (𝟙 ((F ⋙ shiftFunctor D (-a)).obj ((shiftFunctor C a).obj (G.obj Y))))) ≫
              G.map
                ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y))))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y))))) ≫
          G.map ((shiftFunctor D a).map (adj.counit.app Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map ((shiftFunctorCompIsoId D (-a) a h).inv.app (F.obj ((shiftFunctor C a).obj (G.obj Y)))) ≫
        G.map ((shiftFunctor D a).map ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj Y)))) ≫
          G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj Y)))) ≫
            G.map ((shiftFunctor D a).map (adj.counit.app Y))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: 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 ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Tactic:
simp only [mem_distinguishedTriangles_iff, Pretriangulated.rotate_distinguished_triangle
    ((triangleOpEquivalence C).inverse.obj (T.rotate)).unop]
  exact distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm

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

Goal state before:
pp: 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
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ distinguishedTriangles C

Tactic:
by
  obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle₁ f.unop
  refine ⟨_, g.op, (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
    (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op, ?_⟩
  simp only [mem_distinguishedTriangles_iff]
  refine Pretriangulated.isomorphic_distinguished _ H _ ?_
  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
    (Quiver.Hom.op_inj (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))

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₀ n₁ : ℕ
h : n₀ + 1 = n₁
x : ↑(AddCommGrpCat.of (Ext X S.X₃ n₀))
⊢ (comp x hS.extClass h).comp (mk₀ S.f) ⋯ = 0

Tactic:
simp only [comp_assoc_of_third_deg_zero, ShortComplex.ShortExact.extClass_comp,
          comp_zero]

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

Goal state before:
pp: case comm₂₃
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
S : ShortComplex C
hS : S.ShortExact
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
this✝ : HasDerivedCategory C := ⋯
this :
  Function.Exact
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₂,
            f :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            g := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).map hS.singleTriangle.mor₁,
            zero := ⋯ }.f)
    ⇑(ConcreteCategory.hom
        { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
            X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
            X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₂,
            f :=
              (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁ ⋯,
            g := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).map hS.singleTriangle.mor₁,
            zero := ⋯ }.g)
⊢ (ConcreteCategory.hom
          { X₁ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₀).obj hS.singleTriangle.obj₃,
              X₂ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₁,
              X₃ := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).obj hS.singleTriangle.obj₂,
              f :=
                (preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequenceδ hS.singleTriangle ↑n₀ ↑n₁
                  ⋯,
              g := ((preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).shift ↑n₁).map hS.singleTriangle.mor₁,
              zero := ⋯ }.g).comp
      ↑homAddEquiv =
    (↑homAddEquiv).comp
      (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 h),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.g)

Tactic:
· ext x; apply hom_comp_singleFunctor_map_shift (C := C)

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

Goal state before:
pp: case mpr
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ (B (z • x)) y = 0

Tactic:
rw [map_smulₛₗ₂, smul_eq_zero]

Goal state after:
case mpr
K : Type u_7
V : Type u_9
V₂ : Type u_11
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J : K →+* K
B : V →ₗ[K] V →ₛₗ[J] V₂
x y : V
h : (B x) y = 0
z : K
⊢ (RingHom.id K) z = 0 ∨ (B x) y = 0
Module: Mathlib.LinearAlgebra.Basis.Bilinear

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst✝⁶ : CommSemiring Rₗ
inst✝⁵ : AddCommMonoid Mₗ
inst✝⁴ : AddCommMonoid Nₗ
inst✝³ : AddCommMonoid Pₗ
inst✝² : Module Rₗ Mₗ
inst✝¹ : Module Rₗ Nₗ
inst✝ : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ ((b₁'.repr x).sum fun i xi ↦ (b₂'.repr y).sum fun j yj ↦ xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y

Tactic:
by
  conv_rhs => rw [← b₁'.linearCombination_repr x, ← b₂'.linearCombination_repr y]
  simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smul₂, map_smul]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q : QuadraticMap R M N
f : M₁ ≃ₗ[R] M
m✝ : M
⊢ (Q.comp ↑f) ((↑f.symm).toFun m✝) = Q m✝

Tactic:
simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe,
        f.apply_symm_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ id x = x

Tactic:
id_eq

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
f : Q₁ →qᵢ Q₂
g : Q₂ →qᵢ Q₁
x : CliffordAlgebra Q₁
h : g.comp f = QuadraticMap.Isometry.id Q₁
⊢ x = x
Module: Mathlib.Algebra.GradedMonoid

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

Tactic:
rw [Finset.prod_insert hF2, Finset.sum_insert hF2]
    apply SetLike.mul_mem_graded (by grind)
    grind

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

Goal state before:
pp: F : Type u_1
inst✝ : Field F
P : SL(2, F) → Prop
htransvec : ∀ (i j : Fin 2) (h : i ≠ j) (c : F), P (SpecialLinearGroup.transvection h c)
hmul : ∀ (A B : SL(2, F)), P A → P B → P (A * B)
A : SL(2, F)
c : F
hc : c ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 0
⊢ diag2n hij c hc = diag2 c⁻¹ ⋯

Tactic:
ext; simp [diag2n_coe, diagonal_apply]; grind

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

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' =
    ∑ ij ∈ DFinsupp.support a ×ˢ DFinsupp.support a', (of A (ij.1 + ij.2)) (GradedMonoid.GMul.mul (a ij.1) (a' ij.2))

Tactic:
simp only [mul_eq_dfinsuppSum, DFinsupp.sum, Finset.sum_product]

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
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
s : Finset ι
f : ι → M
⊢ Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)

Tactic:
induction s using Finset.cons_induction with

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
ι : Type u_8
Q : QuadraticMap R M N
s : Finset ι
f : ι → M
⊢ Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
⊢ (B y) x + (B x) y = 0 ↔ (B x) y = 0

Tactic:
← h.eq,

Goal state after:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
⊢ (RingHom.id R) ((B x) y) + (B x) y = 0 ↔ (B x) y = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑((r * (of (fun i ↦ ↥(A i)) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0

Tactic:
split_ifs with h
  exacts [coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]

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

Goal state before:
pp: ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ (i + j)

Tactic:
rw [pow_add]

Goal state after:
ι : Type u_1
σ : Type u_2
S : Type u_3
R : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommSemiring S
inst✝¹ : Semiring R
inst✝ : Algebra S R
p✝ : Submodule S R
i j : ℕ
p q : R
hp : p ∈ p✝ ^ i
hq : q ∈ p✝ ^ j
⊢ p * q ∈ p✝ ^ i * p✝ ^ j
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case e_fst
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 : CliffordAlgebra Q
⊢ (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).1 = x

Tactic:
induction x using CliffordAlgebra.left_induction with

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ (↑s).Nonempty ↔ 1 ≤ n

Tactic:
← one_le_card,

Goal state after:
α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ 1 ≤ #↑s ↔ 1 ≤ n
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 : R
⊢ algebraMapInv ((algebraMap R (ExteriorAlgebra R M)) x) = x

Tactic:
by
  simp [algebraMapInv]

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

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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
r : R
⊢ (liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0

Tactic:
rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]

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

Goal state before:
pp: case ι_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : CliffordAlgebra 0
m✝ : M
hx : (liftAlternating (ιMulti R)) x✝ = x✝
⊢ (liftAlternating fun i ↦ (LinearMap.mulLeft R ((ι R) m✝)).compAlternatingMap (ιMulti R i)) x✝ =
    (CliffordAlgebra.ι 0) m✝ * x✝

Tactic:
liftAlternating_comp,

Goal state after:
case ι_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : CliffordAlgebra 0
m✝ : M
hx : (liftAlternating (ιMulti R)) x✝ = x✝
⊢ (LinearMap.mulLeft R ((ι R) m✝) ∘ₗ liftAlternating (ιMulti R)) x✝ = (CliffordAlgebra.ι 0) m✝ * x✝
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
(Classical.indefiniteDescription (fun z => f z = _) _).2

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ ↑(x + y) = ↑x + ↑y
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c • (ConcreteCategory.hom f) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)

Tactic:
(Classical.indefiniteDescription (fun z => f z = _) _).2

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ ↑(c • x) = (RingHom.id R) c • ↑x
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 : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ id x✝ = x✝

Tactic:
id_eq

Goal state after:
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 : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x✝ : ↥(⋀[R]^n M)
⊢ x✝ = x✝
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
⊢ (map n (span R (range v)).subtype).range = span R (range (ιMulti_family R n v))

Tactic:
by
  have ⟨f, hf⟩ : ∃ f : I → Submodule.span R (Set.range v), Submodule.subtype _ ∘ f = v :=
    ⟨fun i ↦ ⟨v i, Submodule.subset_span (Set.mem_range_self i)⟩, rfl⟩
  have htop : Submodule.span R (Set.range f) = ⊤ := by
    apply SetLike.coe_injective
    apply Set.image_injective.mpr (Submodule.span R (Set.range v)).injective_subtype
    rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
  rw [LinearMap.range_eq_map (M := ⋀[R]^n _), ← ιMulti_family_span_of_span _ htop,
    Submodule.map_span, ← Set.range_comp, map_comp_ιMulti_family, hf]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
I B : C
t : IsInitial I
inst✝ : MonoidalClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
⊢ g = h

Tactic:
have := strict_initial t g

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
I B : C
t : IsInitial I
inst✝ : MonoidalClosed C
Z✝ : C
g h : Z✝ ⟶ I
x✝ : g ≫ t.to B = h ≫ t.to B
this : IsIso g
⊢ g = h
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✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ IsFiltered (StructuredArrow (op d) F.op)

Tactic:
apply isFiltered_structuredArrow_of_isFiltered_of_exists

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∃ c, Nonempty (op d ⟶ F.op.obj c)

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∀ {c : Cᵒᵖ} (s s' : op d ⟶ F.op.obj c), ∃ c' t, s ≫ F.op.map t = s' ≫ F.op.map t
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFilteredOrEmpty J
⊢ FinallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

Tactic:
by
  refine ⟨fun _ => FinallySmall.exists_small_weakly_terminal_set _, fun h => ?_⟩
  rcases h with ⟨s, hs, hs'⟩
  exact finallySmall_of_small_weakly_terminal_set s hs'

Goal state after: