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

Goal state before:
pp: ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ (K.restriction e).iCycles j ≫ (K.restriction e).d j k = 0 ≫ (K.restrictionXIso e hk').inv

Tactic:
iCycles_d,

Goal state after:
ι : 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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ 0 = 0 ≫ (K.restrictionXIso e hk').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : 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 : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryGE i
⊢ (truncGE'Map φ e).f i =
    (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ opcyclesMap φ (e.f i) ≫ (L.truncGE'XIsoOpcycles e ⋯ hi).inv

Tactic:
exact dif_pos hi

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
⊢ K.IsSupportedOutside e₁ ↔ K.IsSupported e₂

Tactic:
by
  constructor
  · intro h
    exact ⟨fun i hi => by
      obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
      exact h.exactAt i₁⟩
  · intro _
    exact ⟨fun i₁ => K.exactAt_of_isSupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ Q.map g =
    inv (Q.map (X.ιTruncLE b)) ≫
      Q.map (CochainComplex.truncLEMap g b) ≫ inv (Q.map (CochainComplex.truncLEMap s b)) ≫ Q.map (Y.ιTruncLE b ≫ s)

Tactic:
← CochainComplex.ιTruncLE_naturality s b,

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ Q.map g =
    inv (Q.map (X.ιTruncLE b)) ≫
      Q.map (CochainComplex.truncLEMap g b) ≫
        inv (Q.map (CochainComplex.truncLEMap s b)) ≫ Q.map (CochainComplex.truncLEMap s b ≫ Y'.ιTruncLE b)
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
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ ∑ x, (x✝ x).comp (mk₀ (c.ι x ≫ c.π i)) ⋯ = x✝ i

Tactic:
rw [Finset.sum_eq_single i _ (by simp), bicone_ι_π_self, comp_mk₀_id]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ ∀ b ∈ Finset.univ, b ≠ i → (x✝ b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
⊢ ∀ (a b : ℤ), -(a + b) = -a + -b

Tactic:
by intros; lia

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
f : Y ⟶ X
n a : ℤ
x : Opposite.op ((shiftFunctor C a).obj Z) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ Quiver.Hom.op ((opEquiv' n a a' h).symm (x ≫ (shiftFunctor Cᵒᵖ n).map f.op)) = (f ≫ (opEquiv' n a a' h).symm x).op

Tactic:
simp [opEquiv'_symm_apply, opEquiv_symm_apply]

Goal state after:
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
E : C ≌ D
A : Type u_3
inst✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : E.functor.CommShift A
this : E.inverse.CommShift A := E.commShiftInverse A
⊢ E.CommShift A

Tactic:
exact CommShift.mk' _ _ (E.toAdjunction.commShift_of_leftAdjoint A).commShift_unit

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

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

Tactic:
by
    let := HasDerivedCategory.standard C
    have := hasExt_of_hasDerivedCategory C
    rw [hasExt_iff_small_ext.{w}]
    intro X Y n
    induction n generalizing X Y with
    | zero =>
      rw [small_congr Ext.homEquiv₀]
      infer_instance
    | succ n hn =>
      let S := ShortComplex.mk _ _ (cokernel.condition (Injective.ι Y))
      have hS : S.ShortExact :=
        { exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel S.f) }
      have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) :=
        fun y₁ ↦ Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl
      exact small_of_surjective.{w} this

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

Goal state before:
pp: ι : Type u_1
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
inst✝ : DecidableEq ι
i j : ι
⊢ (e.repr (e j)) i = 1 i j

Tactic:
simp [Matrix.one_apply, Finsupp.single_apply, eq_comm]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ (e.repr (update v j x k)) i' = (e.repr x) i'

pp: case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (update v j x k)) i' = (e.repr (v k)) i'

Tactic:
· rw [h, update_self j x v]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (update v j x k)) i' = (e.repr (v k)) i'
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Finite κ
inst✝³ : Fintype ι
inst✝² : Fintype κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ c.toMatrix ⇑c' * (toMatrix b' c') f * b'.toMatrix ⇑b = (toMatrix b c) f

Tactic:
cases nonempty_fintype κ

Goal state after:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Finite κ
inst✝³ : Fintype ι
inst✝² : Fintype κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
val✝ : Fintype κ
⊢ c.toMatrix ⇑c' * (toMatrix b' c') f * b'.toMatrix ⇑b = (toMatrix b c) f
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)

Tactic:
cases nonempty_fintype κ

Goal state after:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
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
b : F
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F) ↔ b = 0

Tactic:
refine ⟨fun h ↦ ?_, fun hb ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
h : transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)
⊢ b = 0

case refine_2
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
hb : b = 0
⊢ transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha)⁻¹ = diag2 a⁻¹ ⋯

Tactic:
apply inv_eq_of_mul_eq_one_right
  exact diag2_mul_inv a ha

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_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Subalgebra.map ((lift Q) ⟨f, cond⟩) ⊤ = Algebra.adjoin R (Set.range ⇑f)

Tactic:
← adjoin_range_ι,

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_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
⊢ Subalgebra.map ((lift Q) ⟨f, cond⟩) (Algebra.adjoin R (Set.range ⇑(ι Q))) = Algebra.adjoin R (Set.range ⇑f)
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
Q : QuadraticMap R M N
x y : M
⊢ polar (⇑Q) (-x) y = -polar (⇑Q) x y

Tactic:
rw [← neg_one_smul R x, polar_smul_left, neg_one_smul]

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 ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive ↑m
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
⊢ ∀ (m : M), motive m

Tactic:
let ℳ' : ι → AddSubmonoid M := fun i ↦
    (⟨⟨ℳ i, fun x y ↦ AddMemClass.add_mem x y⟩, (ZeroMemClass.zero_mem _)⟩ : AddSubmonoid M)

Goal state after:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
motive : M → Prop
zero : motive 0
homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), motive ↑m
add : ∀ (m m' : M), motive m → motive m' → motive (m + m')
ℳ' : ι → AddSubmonoid M := fun i ↦ { carrier := ↑(ℳ i), add_mem' := ⋯, zero_mem' := ⋯ }
⊢ ∀ (m : M), motive m
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 0
⊢ ↑(((decompose 𝒜) (a * b)) j) = a * ↑(((decompose 𝒜) b) j)

Tactic:
lift a to 𝒜 0 using a_mem
  rw [decompose_mul, decompose_coe, coe_of_mul_apply_of_mem_zero]

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✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S R N
Q : QuadraticMap R M N
a : S
x : M
⊢ Q (a • x) = (a * a) • Q x

Tactic:
by
    simp [map_smul_of_tower]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Q x = 0
hx : ¬x = 0
⊢ 0 < 0

Tactic:
have := hQ _ hx

Goal state after:
M : Type u_4
N : Type u_5
R₂ : Type u
inst✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R₂ M
inst✝² : PartialOrder N
inst✝¹ : AddCommMonoid N
inst✝ : Module R₂ N
Q : QuadraticMap R₂ M N
hQ : Q.PosDef
x : M
hQx : Q x = 0
hx : ¬x = 0
this : 0 < Q x
⊢ 0 < 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✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ↥(A 0)
r' : ⨁ (i : ι), ↥(A i)
j _x : ι
⊢ 0 + _x = j ↔ _x = j

Tactic:
by rw [zero_add]

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

Goal state before:
pp: case mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ i
⊢ P x

Tactic:
| mem i x hx =>

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
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 f hf n) ((ι Q) m * x) = (f m) (x, (foldr' Q f hf n) x)

Tactic:
dsimp [foldr']

Goal state after:
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)) ((ι Q) m * x)).2 = (f m) (x, (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) x).2)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
i : { n // ↑n = i' }
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range ^ ↑i
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) x = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨x, ⋯⟩

Tactic:
| mem i x hx =>

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

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

Tactic:
← Set.powersetCard.coe_coe,

Goal state after:
α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ (↑↑s).Nonempty ↔ 1 ≤ n
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ #(Finset.map f ↑s) = n

Tactic:
card_map,

Goal state after:
α : Type u_1
n : ℕ
β : Type u_2
f : α ↪ β
s : ↑(powersetCard α n)
⊢ #↑s = n
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
⊢ basisRepr Q v = weightedSumSquares R fun i ↦ Q (v i)

Tactic:
by
  ext w
  rw [basisRepr_apply, ← @associated_eq_self_apply R, map_sum, weightedSumSquares_apply]
  refine sum_congr rfl fun j hj => ?_
  rw [← @associated_eq_self_apply R, LinearMap.map_sum₂, sum_eq_single_of_mem j hj]
  · rw [map_smul, LinearMap.map_smul₂, smul_eq_mul, associated_apply, smul_eq_mul,
      smul_eq_mul, Module.End.smul_def, half_moduleEnd_apply_eq_half_smul]
    ring_nf
  · intro i _ hij
    rw [map_smul, LinearMap.map_smul₂, hv₂ hij]
    module

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

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n.succ → M
⊢ (ιMulti R n.succ) v = (ι R) (v 0) * (ιMulti R n) (Matrix.vecTail v)

Tactic:
by
  simp [ιMulti, Matrix.vecTail]

Goal state after:
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
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫ coconeMorphism F x✝ = coconeMorphism F x✝¹ ≫ ((Functor.const J).obj (colimit F)).map f

Tactic:
by
        ext
        simpa using! (Types.TypeMax.colimitCocone
          (F ⋙ forget (ModuleCat R))).ι.naturality_apply f _

Goal state after:
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
⊢ Submodule.map (⋀[R]^n M).subtype (Submodule.span R (range ⇑(ιMulti R n))) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
LinearMap.map_span,

Goal state after:
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Submodule.span R (⇑(⋀[R]^n M).subtype '' range ⇑(ιMulti R n)) = Submodule.map (⋀[R]^n M).subtype ⊤
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
hv : Submodule.span R (range v) = ⊤
⊢ Submodule.map (⋀[R]^n M).subtype (Submodule.span R (range (ιMulti_family R n v))) = Submodule.map (⋀[R]^n M).subtype ⊤

Tactic:
LinearMap.map_span,

Goal state after:
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
hv : Submodule.span R (range v) = ⊤
⊢ Submodule.span R (⇑(⋀[R]^n M).subtype '' range (ιMulti_family R n v)) = Submodule.map (⋀[R]^n M).subtype ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (Hom.hom ((extendRestrictScalarsAdj f).counit.app M₁ ⊗ₘ (extendRestrictScalarsAdj f).counit.app M₂))
      ((Hom.hom (δ (extendScalars f) ((restrictScalars f).obj M₁) ((restrictScalars f).obj M₂)))
        (1 ⊗ₜ[R] (m₁ ⊗ₜ[R] m₂))) =
    m₁ ⊗ₜ[S] m₂

Tactic:
extendScalars_δ_tmul,

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (Hom.hom ((extendRestrictScalarsAdj f).counit.app M₁ ⊗ₘ (extendRestrictScalarsAdj f).counit.app M₂))
      (1 ⊗ₜ[R] m₁ ⊗ₜ[S] (1 ⊗ₜ[R] m₂)) =
    m₁ ⊗ₜ[S] m₂
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u_1
inst✝¹ : Category.{v_1, u_1} E
inst✝ : MonoidalCategory E
e : C ≌ D
X Y : D ⥤ E
x✝ : C
⊢ (Functor.LaxMonoidal.μ e.congrLeft.inverse X Y).app x✝ =
    (e.congrLeft.toAdjunction.unit.app (e.congrLeft.inverse.obj X ⊗ e.congrLeft.inverse.obj Y) ≫
          e.congrLeft.inverse.map
            (Functor.OplaxMonoidal.δ e.congrLeft.functor (e.congrLeft.inverse.obj X) (e.congrLeft.inverse.obj Y) ≫
              (e.congrLeft.toAdjunction.counit.app X ⊗ₘ e.congrLeft.toAdjunction.counit.app Y))).app
      x✝

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_fst
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y)) ≫
      fst (H.obj (F.obj Y)) (H.obj (G.obj Y)) =
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))) ≫
      fst (H.obj (F.obj Y)) (H.obj (G.obj Y))

Tactic:
simp [← Functor.map_comp]

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

Goal state before:
pp: case h_snd
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ (H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y)) ≫
      snd (H.obj (F.obj Y)) (H.obj (G.obj Y)) =
    (CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))) ≫
      snd (H.obj (F.obj Y)) (H.obj (G.obj Y))

Tactic:
simp [← Functor.map_comp]

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
X✝ Y✝ : (J₁ ⥤ C) × (J₁ ⥤ C)
x✝ : X✝ ⟶ Y✝
⊢ (externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).map x✝ ≫
      (NatIso.ofComponents
          (fun x ↦
            Iso.refl
              (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj Y✝).obj x))
          ⋯).hom =
    (NatIso.ofComponents
          (fun x ↦
            Iso.refl
              (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj X✝).obj x))
          ⋯).hom ≫
      (tensor (J₁ ⥤ C)).map x✝

Tactic:
by ext; simp [tensorHom_def]

Goal state after: