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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ sc'Map e.hom h₁ h₂ i j k hij hjk hk ≫ sc'Map e.inv h₂ h₁ i j k hij hjk hk = 𝟙 (S₁.sc' h₁ i j k hij hjk hk)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i j k : ℕ
hij : i + 1 = j
hjk : j + 1 = k
hk : k ≤ n
⊢ sc'Map e.inv h₂ h₁ i j k hij hjk hk ≫ sc'Map e.hom h₁ h₂ i j k hij hjk hk = 𝟙 (S₂.sc' h₂ i j k hij hjk hk)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ scMap e.hom h₁ h₂ i hi ≫ scMap e.inv h₂ h₁ i hi = 𝟙 (S₁.sc h₁ i hi)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
h₂ : S₂.IsComplex
i : ℕ
hi : i + 2 ≤ n
⊢ scMap e.inv h₂ h₁ i hi ≫ scMap e.hom h₁ h₂ i hi = 𝟙 (S₂.sc h₂ i hi)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 1
i : ℕ
hi : i + 2 ≤ 1
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h : S.IsComplex
⊢ 0 + 2 ≤ 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
i : ℕ
hi : i + 2 ≤ 2
⊢ i = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : S.Exact
⊢ 0 + 2 ≤ 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
hS : S.IsComplex
h : (S.sc' hS 0 1 2 exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
i : ℕ
hi : i + 2 ≤ 2
⊢ i = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ 0 + 2 ≤ n + 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ n + 2 ≤ n + 2

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ : S.map' k (k + 1) ⋯ ⋯ = 0
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
⊢ IsIso (S.map' (k + 1) (k + 2) ⋯ ⋯)

Tactic:
have := (hS.exact k).mono_g h₀

Goal state after:
C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ : S.map' k (k + 1) ⋯ ⋯ = 0
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
this : Mono (S.sc ⋯ k ⋯).g
⊢ IsIso (S.map' (k + 1) (k + 2) ⋯ ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ S.L₁.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ S.v₁₂.τ₁
x₂' : A₂ ⟶ S.L₁.X₂ := x₁ ≫ S.L₁.f
x₂ : A₂ ⟶ S.L₁.X₂ := π₂ ≫ p ≫ pullback.fst S.L₁.g S.v₀₁.τ₃
hx₂' : (x₂ - x₂') ≫ S.v₁₂.τ₂ = 0
k₂ : A₂ ⟶ S.L₀.X₂ := ⋯.lift (x₂ - x₂') hx₂'
hk₂ : k₂ ≫ S.v₀₁.τ₂ = x₂ - x₂'
hk₂' : k₂ ≫ S.L₀.g = π₂ ≫ p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
⊢ (π₂ ≫ π₁) ≫ x₃ = k₂ ≫ S.L₁'.f

Tactic:
by simp only [assoc, L₁'_f, ← hk₂', hp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case id
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
X✝ : WalkingMulticospan J
⊢ F.map (Hom.id X✝) ≫
      (match X✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom =
    (match X✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom ≫
      G.map (Hom.id X✝)

Tactic:
simp [wl, wr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case fst
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
b✝ : J.R
⊢ F.map (Hom.fst b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom =
    (match WalkingMulticospan.left (J.fst b✝) with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom ≫
      G.map (Hom.fst b✝)

Tactic:
simp [wl, wr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case snd
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
b✝ : J.R
⊢ F.map (Hom.snd b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom =
    (match WalkingMulticospan.left (J.snd b✝) with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom ≫
      G.map (Hom.snd b✝)

Tactic:
simp [wl, wr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case id
J : MultispanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ (right (J.fst i)).hom = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ (right (J.snd i)).hom = (left i).hom ≫ G.map (Hom.snd i)
X✝ : WalkingMultispan J
⊢ F.map (Hom.id X✝) ≫
      (match X✝ with
        | WalkingMultispan.left i => left i
        | WalkingMultispan.right i => right i).hom =
    (match X✝ with
        | WalkingMultispan.left i => left i
        | WalkingMultispan.right i => right i).hom ≫
      G.map (Hom.id X✝)

Tactic:
simp [wl, wr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case fst
J : MultispanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ (right (J.fst i)).hom = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ (right (J.snd i)).hom = (left i).hom ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ F.map (Hom.fst a✝) ≫
      (match WalkingMultispan.right (J.fst a✝) with
        | WalkingMultispan.left i => left i
        | WalkingMultispan.right i => right i).hom =
    (match WalkingMultispan.left a✝ with
        | WalkingMultispan.left i => left i
        | WalkingMultispan.right i => right i).hom ≫
      G.map (Hom.fst a✝)

Tactic:
simp [wl, wr]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case snd
J : MultispanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ (right (J.fst i)).hom = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ (right (J.snd i)).hom = (left i).hom ≫ G.map (Hom.snd i)
a✝ : J.L
⊢ F.map (Hom.snd a✝) ≫
      (match WalkingMultispan.right (J.snd a✝) with
        | WalkingMultispan.left i => left i
        | WalkingMultispan.right i => right i).hom =
    (match WalkingMultispan.left a✝ with
        | WalkingMultispan.left i => left i
        | WalkingMultispan.right i => right i).hom ≫
      G.map (Hom.snd a✝)

Tactic:
simp [wl, wr]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃ ≫ D.δ)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) =
    (ConcreteCategory.hom (D.φ₁ ≫ D.v₂₃.τ₁)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁

Tactic:
rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at eq

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this✝ : PreservesFiniteLimits (forget₂ C Ab)
this : PreservesFiniteLimits (forget C)
eq :
  (ConcreteCategory.hom D.δ)
      ((ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)) =
    (ConcreteCategory.hom D.v₂₃.τ₁) ((ConcreteCategory.hom D.φ₁) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂))
eq₁ : (ConcreteCategory.hom (pullback.fst D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₂
eq₂ : (ConcreteCategory.hom (pullback.snd D.L₁.g D.v₀₁.τ₃)) (Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂) = x₃
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
i : ℕ
hi : i ≤ n
⊢ i < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
i j : ℕ
hij : autoParam (i ≤ j) map'._auto_1
hjn : autoParam (j ≤ n) map'._auto_3
⊢ i < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
i j : ℕ
hij : autoParam (i ≤ j) map'._auto_1
hjn : autoParam (j ≤ n) map'._auto_3
⊢ j < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
⊢ i = j ∨ j = k

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j : Fin 2
hij : i ≤ j
hjk : j ≤ j
⊢ map f i j ⋯ = map f i j hij ≫ map f j j hjk

Tactic:
rw [map_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n✝ m : ℕ
F G : ComposableArrows C n✝
n k l : ℕ
h : k + l ≤ n
x✝ : Fin (l + 1)
i : ℕ
isLt✝ : i < l + 1
⊢ k + i < n + 1

Tactic:
lia

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : adj.toComonad.Coalgebra
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
⊢ F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (G.map A.a) =
    F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))) ≫ F.map (adj.unit.app (G.obj A.A))

Tactic:
rw [← F.map_comp, equalizer.condition, F.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ ((D.obj j).a ≫ T.ε.app (D.obj j).A) ≫ c.ι.app j = c.ι.app j

Tactic:
(D.obj j).counit,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ 𝟙 (D.obj j).A ≫ c.ι.app j = c.ι.app j
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun x ↦ comap f (restrictScalars R x)) N'
⊢ localized' S p f M' ≤ N'

Tactic:
rw [localized'_eq_span, span_le]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M'' M' : Submodule R M
N' : Submodule S N
h : M' ≤ (fun x ↦ comap f (restrictScalars R x)) N'
⊢ ⇑f '' ↑M' ⊆ ↑N'
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ (∀ n ∈ map N.mkQ P, x✝ • n = 0) ↔ ∀ s ∈ ↑P, x✝ • s ∈ N

Tactic:
exact ⟨fun H p hp ↦ (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
    fun H _ ⟨p, hp, hpm⟩ ↦ hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ n + 1 + 1 ≤ 2 * (n + 1)

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
⊢ IsUnit ((mk I) x) ↔ x ∉ I

Tactic:
isUnit_iff_ne_zero

Goal state after:
S : Type u_1
inst✝¹ : CommRing S
I : Ideal S
inst✝ : I.IsMaximal
n : ℕ
hn : n ≠ 0
x : S
this : Field (S ⧸ I) := Quotient.field I
⊢ (mk I) x ≠ 0 ↔ x ∉ I
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.zero
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ 0 * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
exact ⟨1, one_mem _, isUnit_one, by simp⟩

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.toRingHom.comp f)

Tactic:
by
    let := e.toRingHom.toAlgebra
    have : IsLocalization.Away (1 : S) T :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective
    exact hP.right T (1 : S) f hf

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case h₀
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ ∀ b ∈ p.coeff.support, b ≠ a → (Finsupp.single b (p.coeff b)) a = 0

pp: case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ a ∉ p.coeff.support → (Finsupp.single a (p.coeff a)) a = 0

Tactic:
· intro b _ hb
    rw [single_eq_of_ne' hb]

Goal state after:
case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ a ∉ p.coeff.support → (Finsupp.single a (p.coeff a)) a = 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
a : ℕ
⊢ ↑a ≠ n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).degree = (C a * T 0).degree

Tactic:
by rw [T_zero, mul_one]

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

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max (max uS uT) uM uN, max (max uP uS) uT} (Module.rank ST (ST ⊗[T] P)) =
    Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
      (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))

Tactic:
← lift_lift.{max uS uT uN, uM},

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{uM, max (max uS uT uN) (max uP uS) uT}
      (Cardinal.lift.{max uS uT uN, max (max uP uS) uT} (Module.rank ST (ST ⊗[T] P))) =
    Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
      (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
r : R
⊢ (eval₂ f x) (C r) = f r

Tactic:
by
  rw [← toLaurent_C, eval₂_toLaurent, Polynomial.eval₂_C]

Goal state after: