mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
H : ∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0
x✝ : ↑A
⊢ (Hom.hom (f ≫ ofHom (((Hom.hom f).liftOfSurjective hf) ⟨Hom.hom x, H⟩))) x✝ = (Hom.hom x) x✝

Tactic:
;

Goal state after:
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
H : ∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0
x✝ : ↑A
⊢ (Hom.hom (f ≫ ofHom (((Hom.hom f).liftOfSurjective hf) ⟨Hom.hom x, H⟩))) x✝ = (Hom.hom x) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : N
j : ι
⊢ ((piScalarRightHom R S N ι ∘ₗ piScalarRightInv R S N ι) ∘ₗ single S (fun i ↦ N) i) x j =
    (LinearMap.id ∘ₗ single S (fun i ↦ N) i) x j

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : N
j : ι
⊢ ((piScalarRightHom R S N ι ∘ₗ piScalarRightInv R S N ι) ∘ₗ single S (fun i ↦ N) i) x j =
    (LinearMap.id ∘ₗ single S (fun i ↦ N) i) x j
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
⊢ ((AlgebraTensorModule.curry (piScalarRightInv R S N ι ∘ₗ piScalarRightHom R S N ι)) x ∘ₗ single R (fun i ↦ R) i) 1 =
    ((AlgebraTensorModule.curry LinearMap.id) x ∘ₗ single R (fun i ↦ R) i) 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
⊢ ((AlgebraTensorModule.curry (piScalarRightInv R S N ι ∘ₗ piScalarRightHom R S N ι)) x ∘ₗ single R (fun i ↦ R) i) 1 =
    ((AlgebraTensorModule.curry LinearMap.id) x ∘ₗ single R (fun i ↦ R) i) 1
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := ⋯
n : ℕ
P : CommRingCat := ⋯
iP : R ⟶ P := ⋯
π : MvPolynomial (Fin n) ↑R →ₐ[↑R] ↑S
h₁ : Function.Surjective ⇑π
h₂ : (ker π.toRingHom).FG
⊢ CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom ↑π) = CommRingCat.Hom.hom f

Tactic:
;

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := ⋯
n : ℕ
P : CommRingCat := ⋯
iP : R ⟶ P := ⋯
π : MvPolynomial (Fin n) ↑R →ₐ[↑R] ↑S
h₁ : Function.Surjective ⇑π
h₂ : (ker π.toRingHom).FG
⊢ CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom ↑π) = CommRingCat.Hom.hom f
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
⊢ ∀ (r : ↥s), ∃ i' hi', (ConcreteCategory.hom (F.map hi')) ((ConcreteCategory.hom g') ↑r) = 0

Tactic:
intro r

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
⊢ ∃ i' hi', (ConcreteCategory.hom (F.map hi')) ((ConcreteCategory.hom g') ↑r) = 0
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_1
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ ↑s ⊆ ↑(ker (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none))))

Tactic:
intro r

Goal state after:
case refine_1
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
r : ↑P
⊢ r ∈ ↑s → r ∈ ↑(ker (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none))))
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ g₁ (i₁ y) = i₂ (f₁ y)

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ g₁ (i₁ y) = i₂ (f₁ y)
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ x ∈ Set.range ⇑F

Tactic:
refine ⟨k, h ?_⟩

Goal state after:
case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ ι₃ (F k) = ι₃ x
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : N₁
H : G (π₁ x) = 0
y : M₂
hy : i₂ y = g₁ x
⊢ π₁ x ∈ Set.range ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)

Tactic:
obtain ⟨z, hz⟩ : f₂ y ∈ range ι₃ := (hι₃ (f₂ y)).mp (by rw [← i₃.comp_apply, ← h₂,
      g₂.comp_apply, hy, hg.apply_apply_eq_zero])

Goal state after:
case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : N₁
H : G (π₁ x) = 0
y : M₂
hy : i₂ y = g₁ x
z : K₃
hz : ι₃ z = f₂ y
⊢ π₁ x ∈ Set.range ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R S : CommRingCat
inst✝⁴ : Algebra ↑R ↑S
A B : Type u
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra (↑R) A
inst✝ : Algebra (↑R) B
f g : A →ₐ[↑R] B
a : ↥(f.equalizer g)
⊢ (ConcreteCategory.hom (Under.Hom.right ((f.equalizer g).val.toUnder ≫ f.toUnder))) a =
    (ConcreteCategory.hom (Under.Hom.right ((f.equalizer g).val.toUnder ≫ g.toUnder))) a

Tactic:
;

Goal state after:
R S : CommRingCat
inst✝⁴ : Algebra ↑R ↑S
A B : Type u
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra (↑R) A
inst✝ : Algebra (↑R) B
f g : A →ₐ[↑R] B
a : ↥(f.equalizer g)
⊢ (ConcreteCategory.hom (Under.Hom.right ((f.equalizer g).val.toUnder ≫ f.toUnder))) a =
    (ConcreteCategory.hom (Under.Hom.right ((f.equalizer g).val.toUnder ≫ g.toUnder))) a
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : PullbackCone f g
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (PullbackCone f g)).map f✝ ≫ Y✝.eta.hom =
    X✝.eta.hom ≫
      ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        f✝

Tactic:
;

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : PullbackCone f g
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (PullbackCone f g)).map f✝ ≫ Y✝.eta.hom =
    X✝.eta.hom ≫
      ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        f✝
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : PullbackCone f g
f✝ : X✝ ⟶ Y✝
⊢ ((𝟭 (PullbackCone f g)).map f✝ ≫ Y✝.eta.hom).hom =
    (X✝.eta.hom ≫
        ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f✝).hom

Tactic:
;

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : PullbackCone f g
f✝ : X✝ ⟶ Y✝
⊢ ((𝟭 (PullbackCone f g)).map f✝ ≫ Y✝.eta.hom).hom =
    (X✝.eta.hom ≫
        ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f✝).hom
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f : Y ⟶ X✝
g : Z ⟶ X✝
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ Over.Hom.left
      (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).fst =
    Over.Hom.left
      ((Over.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X).pt.left)
            ⋯).hom ≫
        ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).fst)

Tactic:
;

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z : C
f : Y ⟶ X✝
g : Z ⟶ X✝
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ Over.Hom.left
      (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).fst =
    Over.Hom.left
      ((Over.isoMk
            (Iso.refl
              (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                          map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                          map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X).pt.left)
            ⋯).hom ≫
        ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).fst)