mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S R' S' : Type u
x✝¹⁰ : CommRing R
x✝⁹ : CommRing S
x✝⁸ : CommRing R'
x✝⁷ : CommRing S'
x✝⁶ : Algebra R S
x✝⁵ : Algebra R R'
x✝⁴ : Algebra R S'
x✝³ : Algebra S S'
x✝² : Algebra R' S'
x✝¹ : IsScalarTower R S S'
x✝ : IsScalarTower R R' S'
hsq :
  IsPushout (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R R'))
    (CommRingCat.ofHom (algebraMap S S')) (CommRingCat.ofHom (algebraMap R' S'))
hRS : P (algebraMap R S)
⊢ P (algebraMap R' S')

Tactic:
exact h.1 (f := CommRingCat.ofHom (algebraMap R S)) hsq.flip hRS

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero Z
⊢ P Z

Tactic:
obtain ⟨Z₀, hZ₀, h₀⟩ := P.exists_prop_of_containsZero

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero Z
Z₀ : C
hZ₀ : IsZero Z₀
h₀ : P Z₀
⊢ P Z
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

Tactic:
by
  intro X₁ X₂ f hf
  have h := initialIsInitial (C := Discrete (PUnit.{w + 1}))
  let c₁ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₁)) h
  let c₂ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₂)) h
  have hc₁ : IsColimit c₁ := colimitOfDiagramInitial h _
  have hc₂ : IsColimit c₂ := colimitOfDiagramInitial h _
  have : hc₁.desc (Cocone.mk _ (Discrete.natTrans (fun _ ↦ by exact f) ≫ c₂.ι)) = f :=
    hc₁.hom_ext (fun x ↦ by
      obtain rfl : x = ⊥_ _ := by ext
      rw [IsColimit.fac]
      simp [c₁, c₂])
  rw [← this]
  exact ⟨_, _, _, _, _, hc₂, _, fun _ ↦ hf⟩

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
h : P.diagonal g
⊢ P.diagonal (pullback.fst f g)

Tactic:
rw [diagonal_iff, diagonal_pullback_fst, P.cancel_left_of_respectsIso,
        P.cancel_right_of_respectsIso]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.RespectsIso
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst✝ : HasPullback f g
h : P.diagonal g
⊢ P (Over.Hom.left ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)))
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : ↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left })))
⊢ (Hom.hom ((unop S).binaryCofan (unop T)).inl.op.unop) x =
    (Hom.hom (S ◁ (terminalOpOfInitial isInitialSelf).from T ≫ (ρ_ S).hom).unop) x

Tactic:
change x ⊗ₜ 1 = x ⊗ₜ algebraMap R T.unop 1

Goal state after:
R : Type u
inst✝ : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : ↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left })))
⊢ x ⊗ₜ[R] 1 = x ⊗ₜ[R] (algebraMap R ↑(unop T)) 1
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ (μIso F X Y).symm.hom = (prodComparisonIso F X Y).hom

Tactic:
simpa using δ_of_cartesianMonoidalCategory F X Y

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
X Y : C
⊢ μ F X Y = (prodComparisonIso F X Y).inv

Tactic:
change (μIso F X Y).symm.inv = _; congr; ext : 1; simpa using δ_of_cartesianMonoidalCategory F X Y

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))

Tactic:
rw [Adjunction.comp_homEquiv, Adjunction.comp_homEquiv]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : X ⊗ Y ⟶ Z
⊢ ((fun x x_1 ↦
          ((fun x x_2 ↦
                  (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                    ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                (F.obj x) x_1).trans
            (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
        Y Z)
      ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f) =
    (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z)))
      (curry
        ((adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z)
          ((Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y ≫ f)))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((adj.comp ((ihom.adjunction (F.obj X)).comp adj.toEquivalence.symm.toAdjunction)).homEquiv Y Z).symm f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))).symm f))

Tactic:
rw [Adjunction.comp_homEquiv, Adjunction.comp_homEquiv]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
f : Y ⟶ (ihom X).obj Z
⊢ (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      ((fun x x_1 ↦
              ((fun x x_2 ↦
                      (adj.toEquivalence.symm.toAdjunction.homEquiv ((tensorLeft (F.obj X)).obj x) x_2).trans
                        ((ihom.adjunction (F.obj X)).homEquiv x (F.obj x_2)))
                    (F.obj x) x_1).trans
                (adj.homEquiv x ((F ⋙ ihom (F.obj X)).obj x_1)))
            Y Z).symm
        f =
    (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
      (adj.toEquivalence.symm.toAdjunction.homEquiv (F.obj X ⊗ F.obj Y) Z).symm
        (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))).symm f))
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: α : Type ?u.3
inst✝ : Denumerable α
n : ℕ
⊢ (fun s ↦ encode (lower' ((Finset.map (eqv α).toEmbedding s).sort fun a b ↦ a ≤ b) 0))
      ((fun n ↦ Finset.map (eqv α).symm.toEmbedding (raise'Finset (ofNat (List ℕ) n) 0)) n) =
    n

Tactic:
by
      simp [-Multiset.map_coe, Finset.map, raise'Finset, Finset.sort,
        List.mergeSort_eq_self _ (raise'_sorted _ _).sortedLE.pairwise, lower_raise']

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Function.Surjective (WType.elim (↥(closure s)) (operate s))

Tactic:
← Set.range_eq_univ

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Set.range (WType.elim (↥(closure s)) (operate s)) = Set.univ
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (Y₂ ⊗ Y₁) ◁ (η_ X₁ Y₁ ⊗≫ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ 𝟙 ((X₁ ⊗ X₂) ⊗ Y₂ ⊗ Y₁)) ≫
      (α_ (Y₂ ⊗ Y₁) (X₁ ⊗ X₂) (Y₂ ⊗ Y₁)).inv ≫ (𝟙 ((Y₂ ⊗ Y₁) ⊗ X₁ ⊗ X₂) ⊗≫ Y₂ ◁ ε_ X₁ Y₁ ▷ X₂ ⊗≫ ε_ X₂ Y₂) ▷ (Y₂ ⊗ Y₁) =
    (ρ_ (Y₂ ⊗ Y₁)).hom ≫ (λ_ (Y₂ ⊗ Y₁)).inv

Tactic:
calc
      _ = (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫
          (Y₂ ⊗ Y₁) ◁ (X₁ ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫
          (Y₂ ◁ (ε_ X₁ Y₁ ▷ X₂)) ▷ (Y₂ ⊗ Y₁) ⊗≫
          ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) := by monoidal
      -- Group η₂ and ε₁ so they compose with ≫ (both act on the Y₁ ⊗ X₁ factor):
      --
      --   Y₂  Y₁      ╭── X₁ ────────────╮
      --   │    │      │    ╭── X₂ ───╮   │
      --   │    │      │    │         │   │
      --   │    ╰──ε₁──╯    │         │   │
      --   │                │         │   │
      --   ╰────── ε₂ ──────╯         │   │
      --                              Y₂  Y₁
      --
      _ = (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫
          Y₂ ◁ ((Y₁ ⊗ X₁) ◁ η_ X₂ Y₂ ≫ ε_ X₁ Y₁ ▷ (X₂ ⊗ Y₂)) ▷ Y₁ ⊗≫
          ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) := by monoidal
      -- Slide the η₂ cup past the ε₁ cap (whisker_exchange), separating the
      -- two zigzags into independent snakes:
      --
      --   Y₂   Y₁
      --   │    │   ╭─X₁──╮
      --   │    │   │     │
      --   │    ╰───╯     │       ← snake for (X₁, Y₁)
      --   │              │
      --   │  ╭─X₂──╮     │
      --   │  │     │     │
      --   ╰──╯     │     │       ← snake for (X₂, Y₂)
      --            Y₂    Y₁
      --
      _ = (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫
          Y₂ ◁ (ε_ X₁ Y₁ ▷ (𝟙_ C) ≫ (𝟙_ C) ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫
          ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) := by
        rw [whisker_exchange]
      -- Separate into two snakes and cancel each.
      _ = 𝟙 _ ⊗≫ Y₂ ◁ (Y₁ ◁ η_ X₁ Y₁ ⊗≫ ε_ X₁ Y₁ ▷ Y₁) ⊗≫
          (Y₂ ◁ η_ X₂ Y₂ ⊗≫ ε_ X₂ Y₂ ▷ Y₂) ▷ Y₁ ⊗≫ 𝟙 _ := by monoidal
      _ = _ := by rw [coevaluation_evaluation'', coevaluation_evaluation'']; monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ Module.rank K V + Module.rank K V₁ = Module.rank K V₂ + Module.rank K V₃

Tactic:
have hf : Surjective (coprod db eb) := by
    rwa [← range_eq_top, range_coprod, eq_top_iff]
  conv =>
    rhs
    rw [← rank_prod', rank_eq_of_surjective hf]
  congr 1
  apply LinearEquiv.rank_eq
  let L : V₁ →ₗ[K] ker (coprod db eb) :=
    LinearMap.codRestrict _ (prod cd (-ce)) <| by
      simpa [add_eq_zero_iff_eq_neg] using LinearMap.ext_iff.1 eq
  refine LinearEquiv.ofBijective L ⟨?_, ?_⟩
  · rw [← ker_eq_bot, ker_codRestrict, ker_prod, hgd, bot_inf_eq]
  · rw [← range_eq_top, eq_top_iff, LinearMap.range_codRestrict, ← map_le_iff_le_comap,
      Submodule.map_top, range_subtype]
    rintro ⟨d, e⟩
    have h := eq₂ d (-e)
    simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker,
      Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range,
      Function.prod_apply] at h ⊢
    grind

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
hx : x ∈ p
a : K
hx' : a • v = x
⊢ x ∈ ⊥

Tactic:
rw [← hx'] at hx

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
x : V
a : K
hx : a • v ∈ p
hx' : a • v = x
⊢ x ∈ ⊥
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this : FiniteDimensional F E
⊢ S = ⊥ ∨ S = ⊤

Tactic:
have : FiniteDimensional F S :=
        FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝ : FiniteDimensional F E
this : FiniteDimensional F ↥S
⊢ S = ⊥ ∨ S = ⊤
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:

Tactic:
_ = η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y' := by
        monoidal
      _ = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y' := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [evaluation_coevaluation'']
        simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, (B x) y = 0
y : M
⊢ ∃ u ∈ W, ∃ v ∈ B.ker, u + v = y

Tactic:
rw [← Submodule.mem_sup, hW.sup_eq_top]; exact Submodule.mem_top

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ W ≤ W.dualAnnihilator.subtype.flip.ker

Tactic:
intro w hw

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
w : M
hw : w ∈ W
⊢ w ∈ W.dualAnnihilator.subtype.flip.ker
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
⊢ f.dualMap.range = f.ker.dualAnnihilator

Tactic:
have rr_surj : Function.Surjective f.rangeRestrict := by
    rw [← range_eq_top, range_rangeRestrict]

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
⊢ f.dualMap.range = f.ker.dualAnnihilator
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
t : K
hfy : f (t • x) = 0
hpy : t • x ∈ p
⊢ t • x = 0

Tactic:
have ht : t = 0 := by simpa [hx] using hfy

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
t : K
hfy : f (t • x) = 0
hpy : t • x ∈ p
ht : t = 0
⊢ t • x = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G

Tactic:
simp [PreservesCokernel.iso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ NormalMono.g = 0

Tactic:
by
    have reassoc' {W : C} (h' : S ⟶ W) : f ≫ h ≫ h' = g ≫ k ≫ h' := by
      simp only [← Category.assoc, eq_whisker comm]
    rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso (φ ≫ φ') → QuasiIso φ'

pp: case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso φ' → QuasiIso (φ ≫ φ')

Tactic:
· intro
    exact quasiIso_of_comp_left φ φ'

Goal state after:
case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
⊢ QuasiIso φ' → QuasiIso (φ ≫ φ')
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ (CokernelCofork.IsColimit.ofId S.f hf).desc (CokernelCofork.ofπ S.g ⋯) = 0

Tactic:
change 𝟙 _ ≫ S.g = 0

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : S.HasLeftHomology
hf : S.f = 0
this : IsIso S.leftHomologyπ
⊢ S.cycles ≅ S.leftHomology

Tactic:
exact asIso S.leftHomologyπ

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.H

Tactic:
leftHomologyMap'_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ 𝟙 h₁.H = 𝟙 h₁.H
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.H

Tactic:
leftHomologyMap'_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ 𝟙 h₂.H = 𝟙 h₂.H
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ =
    leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φH ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData

Tactic:
← γ.leftHomologyMap'_eq,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ =
    leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫
      leftHomologyMap' φ h₁ h₂ ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' φ h₁ h₂ ≫ h₂.g' = h₁.g' ≫ φ.τ₃

Tactic:
simp only [← cancel_epi h₁.p, φ.comm₂₃, p_opcyclesMap'_assoc,
    RightHomologyData.p_g'_assoc, RightHomologyData.p_g']

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
wi : F.map h.i ≫ F.map S.g = 0
hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)
f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)
hf' : f' = F.map h.f'
wπ : f' ≫ F.map h.π = 0
⊢ (S.map F).LeftHomologyData

Tactic:
have hπ : IsColimit (CokernelCofork.ofπ (F.map h.π) wπ) := by
    let e : parallelPair f' 0 ≅ parallelPair (F.map h.f') 0 :=
      parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa using hf') (by simp)
    refine IsColimit.precomposeInvEquiv e _
      (IsColimit.ofIsoColimit (CokernelCofork.mapIsColimit _ h.hπ' F) ?_)
    exact Cofork.ext (Iso.refl _) (by simp [e])

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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
wi : F.map h.i ≫ F.map S.g = 0
hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)
f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)
hf' : f' = F.map h.f'
wπ : f' ≫ F.map h.π = 0
hπ : IsColimit (CokernelCofork.ofπ (F.map h.π) wπ)
⊢ (S.map F).LeftHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
p : X✝ ⟶ Y✝
x✝ : Epi p
⊢ NormalEpi p

Tactic:
refine NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
    (isColimitOfIsColimitπ _ ?_ ?_ ?_)
  all_goals apply Abelian.isColimitMapCoconeOfCokernelCoforkOfπ

Goal state after: