mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
i₁ : ι₁
h₁ : c.Rel (e₁.f i₁) (c.next (e₁.f i₁))
h₂ : ∀ (k : ι₁), ¬c.Rel (e₁.f i₁) (e₁.f k)
i₂ : ι₂
hi₂ : c.next (e₁.f i₁) = e₂.f i₂
⊢ ac.Boundary i₁ i₂

Tactic:
by simpa only [hi₂] using! h₁

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n → ∀ i < n, ExactAt K i

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ i < n, ExactAt K i) → K.IsGE n

Tactic:
· intro _ i hi
    exact K.exactAt_of_isGE n i hi

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ i < n, ExactAt K i) → K.IsGE n
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsLE n
⊢ L.IsLE n

Tactic:
by
  apply isSupported_of_iso e

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsGE n
⊢ L.IsGE n

Tactic:
by
  apply isSupported_of_iso e

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

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f

Tactic:
let G := Φ.localizedFunctor L₁ L₂

Goal state after:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁸ : Category.{v_2, u_2} C₁
inst✝⁷ : Category.{v_3, u_3} C₂
inst✝⁶ : Category.{v_4, u_4} C₃
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
L₃ : C₃ ⥤ D₃
inst✝ : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂
⊢ Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
n : ℤ
inst✝ : X.IsStrictlyLE n
⊢ ∃ X', ∃ (_ : X'.IsStrictlyLE n), ∃ s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
obtain ⟨X', s, hs, g, rfl⟩ := right_fac f
  have : IsIso (Q.map (CochainComplex.truncLEMap s n)) := by
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncLEMap_iff]
    rw [isIso_Q_map_iff_quasiIso] at hs
    infer_instance
  refine ⟨X'.truncLE n, inferInstance, CochainComplex.truncLEMap s n ≫ X.ιTruncLE n, ?_,
      CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n, ?_⟩
  · rw [Q.map_comp]
    infer_instance
  · simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ ∀ {P : C} (g : P ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4),
    g ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0 → g = 0

Tactic:
intro A

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
⊢ ∀ (g : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4),
    g ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0 → g = 0
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ ∀ ⦃A : C⦄ (y : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
    ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11

Tactic:
intro A

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
⊢ ∀ (y : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11),
    ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11
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 : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ (adj.homEquiv (G.obj ((shiftFunctor D a).obj Y)) ((shiftFunctor D a).obj Y))
      (adj.counit.app ((shiftFunctor D a).obj Y)) =
    (adj.homEquiv (G.obj ((shiftFunctor D a).obj Y)) ((shiftFunctor D a).obj Y))
      (F.map (e₂.hom.app Y) ≫ e₁.hom.app (G.obj Y) ≫ (shiftFunctor D a).map (adj.counit.app Y))

Tactic:
rw [adj.homEquiv_unit, adj.homEquiv_unit, G.map_comp, adj.unit_naturality_assoc, ← eq]

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 : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ adj.unit.app (G.obj ((shiftFunctor D a).obj Y)) ≫ G.map (adj.counit.app ((shiftFunctor D a).obj Y)) =
    e₂.hom.app Y ≫
      ((shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y))) ≫
        G.map (e₁.hom.app (G.obj Y) ≫ (shiftFunctor D a).map (adj.counit.app 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
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:
by
  symm
  ext n
  simp [mapHomologicalComplexIso, descShortComplex, mapHomologicalComplexXIso,
    mapHomologicalComplexXIso'_hom, Functor.mapHomologicalComplex_map_f,
    desc_f _ _ _ _ n (n + 1) rfl]

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 ℤ
X : Cᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫
      (𝟙 ((shiftFunctor C 0).obj (Opposite.unop X))).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
op_id,

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      (𝟙 ((shiftFunctor C b₃).obj (Opposite.unop X))).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
op_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      𝟙 (Opposite.op ((shiftFunctor C b₃).obj (Opposite.unop X))) ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app 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
inst✝ : adj.CommShift A
a : A
X : C
⊢ adj.unit.app ((shiftFunctor C a).obj X) ≫ (Functor.commShiftIso (F ⋙ G) a).hom.app X =
    (shiftFunctor C a).map (adj.unit.app X)

Tactic:
by
  simpa using (NatTrans.shift_app_comm adj.unit a X).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 : Cᵒᵖ
⊢ contractibleTriangle X ∈ distinguishedTriangles C

Tactic:
rw [mem_distinguishedTriangles_iff']
  exact ⟨_, inv_rot_of_distTriang _ (Pretriangulated.contractible_distinguished X.unop),
    ⟨contractibleTriangleIso X⟩⟩

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
⊢ Function.Injective ⇑solution.fromQuotient ↔ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
by
  constructor
  · intro h
    rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]
  · intro h
    rw [← LinearMap.ker_eq_bot, eq_bot_iff]
    intro x hx
    obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x
    replace hx : x ∈ LinearMap.ker solution.π := by
      simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx
    rw [h, ← range_map] at hx
    obtain ⟨x, rfl⟩ := hx
    simp only [toQuotient_map_apply, Submodule.zero_mem]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst✝ : Fintype ι'
b'' : ι'' → M
this✝¹ : DecidableEq ι
this✝ : DecidableEq ι'
this : DecidableEq ι''
i : ι
j : ι''
⊢ (b.toMatrix ⇑b' * b'.toMatrix b'') i j = b.toMatrix b'' i j

Tactic:
simp only [Matrix.mul_apply, toMatrix_apply, sum_repr_mul_repr]

Goal state after:
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 ((Finsupp.linearCombination Rₗ ⇑b₁') (b₁'.repr x))) y

Tactic:
← b₂'.linearCombination_repr y

Goal state after:
ι₁ : 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 ((Finsupp.linearCombination Rₗ ⇑b₁') (b₁'.repr x))) ((Finsupp.linearCombination Rₗ ⇑b₂') (b₂'.repr y))
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b ∈ Finset.univ, 0 < v b
⊢ ∃ b ∈ Finset.univ, 0 < (-1 • v) b

Tactic:
Finset.mem_univ,

Goal state after:
case inr.inr.refine_2
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : CommRing S]
    [inst_3 : LinearOrder S] [IsStrictOrderedRing S] {A : Matrix n n S},
    (Pairwise fun i j ↦ A i j < 0) →
      ∀ (h : Nonempty n), A.det = 0 → ∀ (v : n → S), v ≠ 0 → v ᵥ* A = 0 → 0 < Finset.univ.sup' ⋯ v → ∃ j, ∑ i, A i j ≤ 0
i : n
hi : v i ≠ 0 i
h_sup : ¬∃ b, True ∧ 0 < v b
⊢ ∃ b, True ∧ 0 < (-1 • v) b
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case neg
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
pf✝ : Nonempty n
⊢ ↑↑A = (scalar n) ↑↑(rootsOfUnity.mkOfPowEq (↑↑A (Classical.arbitrary n) (Classical.arbitrary n)) ⋯)

Tactic:
rootsOfUnity.val_mkOfPowEq_coe,

Goal state after:
case neg
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : ↥(center (SpecialLinearGroup n R))
h : ¬IsEmpty n
pf✝ : Nonempty n
⊢ ↑↑A = (scalar n) (↑↑A (Classical.arbitrary n) (Classical.arbitrary n))
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
⊢ Algebra.adjoin R (Set.range ⇑(ι Q)) = ⊤

Tactic:
refine top_unique fun x hx => ?_

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
hx : x ∈ ⊤
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι Q))
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case zero
⊢ ↑(T ^ 0) = !![1, 0; 0, 1]

Tactic:
zpow_zero,

Goal state after:
case zero
⊢ ↑1 = !![1, 0; 0, 1]
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A (n • i + i)) (GradedMonoid.GMul.mul (GradedMonoid.GMonoid.gnpow n a) a) =
    (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)

Tactic:
exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm

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
h : IsUnit 2
Q₁ Q₂ : QuadraticMap R M N
h₁₂ : Q₁.polarBilin = Q₂.polarBilin
⊢ Q₁.polarBilin.toQuadraticMap = Q₂.polarBilin.toQuadraticMap

Tactic:
exact congrArg toQuadraticMap h₁₂

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 x) y + (B x) y = 0 ↔ (B x) y = 0

Tactic:
add_self_eq_zero

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 := ⋯ }
⊢ (B x) y = 0 ↔ (B x) y = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = 0

Tactic:
by
  rw [← hx x]
  exact (associated_eq_self_apply _ _ x).symm

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

Goal state before:
pp: case succ.inl
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm 0
b : Basis (Fin (finrank K V)) K V := finBasis K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v

Tactic:
rw [hd] at b

Goal state after:
case succ.inl
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm 0
b : Basis (Fin (d + 1)) K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case inl
ι : 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
x : ι × ι
hx✝ : x ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = k}
hx : x.1 < m
⊢ ↑(r x.1) * ↑(r' x.2) = 0

Tactic:
simp [hr, hr', hx]

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

Goal state before:
pp: case inr
ι : 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
x : ι × ι
hx✝ : x ∈ {ij ∈ DFinsupp.support r ×ˢ DFinsupp.support r' | ij.1 + ij.2 = k}
hx : x.2 < n
⊢ ↑(r x.1) * ↑(r' x.2) = 0

Tactic:
simp [hr, hr', hx]

Goal state after:
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✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ (∏ x ∈ s, x) n = 0

Tactic:
simpa using listProd_apply_eq_zero (l := s.toList) (by simpa using hs) (by simpa)

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

Goal state before:
pp: α : Type u_1
n : ℕ
s t : ↑(powersetCard α n)
⊢ s = t ↔ ∀ a ∈ s, a ∈ t

Tactic:
eq_iff_subset

Goal state after:
α : Type u_1
n : ℕ
s t : ↑(powersetCard α n)
⊢ ↑s ⊆ ↑t ↔ ∀ a ∈ s, a ∈ t
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
⊢ alternatingMapLinearEquiv.symm (map n f) = (ιMulti R n).compLinearMap f

Tactic:
simp only [map, LinearEquiv.symm_apply_apply]

Goal state after: