mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case cons
R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
a : ι → A
s : ι → ↥S
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, mk (a i) (s i) = mk (∏ i ∈ s✝, a i) (∏ i ∈ s✝, s i)
⊢ ∏ i ∈ Finset.cons a✝¹ s✝ h✝, mk (a i) (s i) = mk (∏ i ∈ Finset.cons a✝¹ s✝ h✝, a i) (∏ i ∈ Finset.cons a✝¹ s✝ h✝, s i)

Tactic:
simp [OreLocalization.one_def, *, mk_mul_mk]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case h
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this : DecidablePred fun x ↦ x ∈ s
x : FreeCommRing α
hx : x.IsSupported s
⊢ (lift fun a ↦ if a ∈ s then 0 else X) (-1) = ↑(-1)

Tactic:
rw [map_neg, map_one, Int.cast_neg, Int.cast_one]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.e_m
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n

pp: case e_s
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)

Tactic:
· simp only [Submonoid.smul_def, smul_add, ← mul_smul, Submonoid.coe_mul]; ring_nf

Goal state after:
case e_s
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
p : LocalizedModule S M
x✝² x✝¹ : M × ↥S
a : M
b : ↥S
a' : M
b' : ↥S
x✝ : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1

Tactic:
rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ s]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R M'
f : M →ₗ[R] M'
inst✝⁶ : IsLocalizedModule S f
R₀ : Type u_6
inst✝⁵ : SMul R₀ R
inst✝⁴ : SMul R₀ M
inst✝³ : SMul R₀ M'
inst✝² : IsScalarTower R₀ R R
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsScalarTower R₀ R M'
r : R₀
m : M
s : ↥S
⊢ mk' f (r • m) s = r • mk' f m s

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R M'
f : M →ₗ[R] M'
inst✝⁶ : IsLocalizedModule S f
R₀ : Type u_6
inst✝⁵ : SMul R₀ R
inst✝⁴ : SMul R₀ M
inst✝³ : SMul R₀ M'
inst✝² : IsScalarTower R₀ R R
inst✝¹ : IsScalarTower R₀ R M
inst✝ : IsScalarTower R₀ R M'
r : R₀
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (r • m) s) = r • (fromLocalizedModule S f) (LocalizedModule.mk m s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ + mk' f m₂ s₂ = mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) + (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) =
    (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ mk' f m 1 = f m

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = f m
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f (s • m) s = f m

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s • m) s) = f m
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) =
    (fromLocalizedModule S f) (LocalizedModule.mk m s₂)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) =
    (fromLocalizedModule S f) (LocalizedModule.mk m s₁)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ = mk' f m₂ s₂ ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) = (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) ↔
    ∃ s, s • s₁ • m₂ = s • s₂ • m₁
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : SubtractionCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f (-m) s = -mk' f m s

Tactic:
delta mk'

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : SubtractionCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (-m) s) = -(fromLocalizedModule S f) (LocalizedModule.mk m s)
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝.right = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }.right

Tactic:
· exact h₂.uniq ((snd _ _).mapCocone s) _ (by simp [← hm])

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : AddCommMonoid M''
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
inst✝¹¹ : Module A M'
inst✝¹⁰ : IsLocalization S A
inst✝⁹ : Module R M
inst✝⁸ : Module R M'
inst✝⁷ : Module R M''
inst✝⁶ : IsScalarTower R A M'
f : M →ₗ[R] M'
g✝ : M →ₗ[R] M''
inst✝⁵ : IsLocalizedModule S f
N : Type ?u.59
N' : Type ?u.61
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h₁ h₂ : M →ₗ[R] N
⊢ lift S f (g ∘ₗ (h₁ + h₂)) ⋯ ∘ₗ f = (lift S f (g ∘ₗ h₁) ⋯ + lift S f (g ∘ₗ h₂) ⋯) ∘ₗ f

Tactic:
simp only [lift_comp, LinearMap.add_comp, LinearMap.comp_add]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
inst✝ : IsLocalHom (Hom.hom g)
⊢ IsLocalHom (Hom.hom (pullback.fst f g))

Tactic:
refine Limits.π_isLocalHom _ (limit.isLimit _) left fun x hx i ↦ ?_
  rcases i with _ | _ | _
  · exact ⟨one, 𝟙 _, Hom.inl, inferInstance, by simp; rfl⟩
  · exact ⟨left, 𝟙 _, 𝟙 _, inferInstance, by simp⟩
  · refine ⟨one, Hom.inr, Hom.inl, ‹_›, ?_⟩
    exact DFunLike.congr_fun (congr(Hom.hom $(pullback.condition (f := f) (g := g)))) x |>.symm

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ (F.comp G.toPrelaxFunctor).map₂ (λ_ f).inv =
    (λ_ ((F.comp G.toPrelaxFunctor).map f)).inv ≫
      (G.mapId (F.obj a✝) ≫ G.map₂ (F.mapId a✝)) ▷ (F.comp G.toPrelaxFunctor).map f ≫
        G.mapComp (F.map (𝟙 a✝)) (F.map f) ≫ G.map₂ (F.mapComp (𝟙 a✝) f)

Tactic:
by
    dsimp
    simp only [map₂_leftUnitor, PrelaxFunctor.map₂_comp, assoc, mapComp_naturality_left_assoc,
      comp_whiskerRight]

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
⊢ (ofObj X).op = ofObj fun i ↦ op (X i)

Tactic:
by
  ext Z
  simp only [op_iff, ofObj_iff]
  constructor
  · rintro ⟨i, hi⟩
    exact ⟨i, by rw [hi]⟩
  · rintro ⟨i, hi⟩
    exact ⟨i, by rw [← hi]⟩

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing A
f : R →+* S
g : S →+* A
hf : (RingHom.ker f).FG
hg : (RingHom.ker g).FG
hsur : Function.Surjective ⇑f
this✝² : Algebra R S := f.toAlgebra
this✝¹ : Algebra R A := (g.comp f).toAlgebra
this✝ : Algebra S A := g.toAlgebra
this : IsScalarTower R S A := IsScalarTower.of_algebraMap_eq fun x ↦ rfl
f₁ : R →ₗ[R] S := Algebra.linearMap R S
g₁ : S →ₗ[R] A := (IsScalarTower.toAlgHom R S A).toLinearMap
⊢ (RingHom.ker (g.comp f)).FG

Tactic:
exact Submodule.fg_ker_comp f₁ g₁ hf
    (Submodule.FG.restrictScalars_of_surjective hg hsur) hsur

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case singleton
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
⊢ ∃ n, (R ∙ x) ^ n ≤ I

Tactic:
obtain ⟨n, hn⟩ := hJK (subset_span (Set.mem_singleton x))

Goal state after:
case singleton
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J : Ideal R
x : R
hJK : R ∙ x ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ ∃ n, (R ∙ x) ^ n ≤ I
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
⊢ Function.Surjective fun x ↦
    match x with
    | Sum.inl x => ⟨↑x, ⋯⟩
    | Sum.inr x => ⟨↑x, ⋯⟩

Tactic:
rintro ⟨x, hx | hx⟩

Goal state after:
case inl
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : P x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩

case inr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
x : C
hx : Q x
⊢ ∃ a,
    (fun x ↦
          match x with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        a =
      ⟨x, ⋯⟩
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
by
  rw [← essentiallySmall_op_iff, op_unop]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_2
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type w
inst✝ : EssentiallySmall.{w, v, u} C
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : ⊤ ≤ P.isoClosure
y : F.Elements
x✝ : ⊤ y
⊢ ObjectProperty.isoClosure (fun x ↦ P x.fst) y

Tactic:
obtain ⟨Z, hZ, ⟨e⟩⟩ := hP y.fst (by simp)

Goal state after:
case refine_2
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type w
inst✝ : EssentiallySmall.{w, v, u} C
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : ⊤ ≤ P.isoClosure
y : F.Elements
x✝ : ⊤ y
Z : C
hZ : P Z
e : y.fst ≅ Z
⊢ ObjectProperty.isoClosure (fun x ↦ P x.fst) y
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝ : HasColimitsOfShape C H
X✝ Y✝ : Grothendieck F ⥤ H
x✝ : X✝ ⟶ Y✝
⊢ (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
    (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝

Tactic:
iterate 2 apply colimit.hom_ext; intro

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝ : HasColimitsOfShape C H
X✝ Y✝ : Grothendieck F ⥤ H
x✝ : X✝ ⟶ Y✝
j✝¹ : C
j✝ : ↑(F.obj j✝¹)
⊢ colimit.ι (Grothendieck.ι F j✝¹ ⋙ X✝) j✝ ≫
      colimit.ι ((fiberwiseColim F H).obj X✝) j✝¹ ≫
        (fiberwiseColim F H ⋙ colim).map x✝ ≫ (colimitFiberwiseColimitIso Y✝).hom =
    colimit.ι (Grothendieck.ι F j✝¹ ⋙ X✝) j✝ ≫
      colimit.ι ((fiberwiseColim F H).obj X✝) j✝¹ ≫ (colimitFiberwiseColimitIso X✝).hom ≫ colim.map x✝
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
z : G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂

Tactic:
rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w, z]

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ : C
⊢ ∀ (X₂ : C) (k₁ : X ⟶ F.obj X₁✝) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁✝ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ → G.map k₁ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂ ≫ c.ι.app X₂ = G.map f ≫ c.ι.app Y

Tactic:
_

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
⊢ ∀ (k₁ : X ⟶ F.obj X₁✝) (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁ ≫ F.map f_1 = k₂ → G.map k₁ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
⊢ ∀ (k₁ : X ⟶ F.obj X₁✝) (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁ ≫ F.map f_1 = k₂ → G.map k₁ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y

Tactic:
_

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
⊢ ∀ (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁✝ ≫ F.map f_1 = k₂ → G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
⊢ ∀ (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁✝ ≫ F.map f_1 = k₂ → G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y

Tactic:
_

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
⊢ ∀ (f_1 : X₁✝ ⟶ X₂✝),
    k₁✝ ≫ F.map f_1 = k₂✝ →
      G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
⊢ ∀ (f_1 : X₁✝ ⟶ X₂✝),
    k₁✝ ≫ F.map f_1 = k₂✝ →
      G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y

Tactic:
_

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
⊢ k₁✝ ≫ F.map f✝ = k₂✝ → G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ : C
⊢ ∀ (X₂ : C) (k₁ : X ⟶ F.obj X₁✝) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁✝ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ → G.map k₂ ≫ c.ι.app X₂ = G.map f ≫ c.ι.app Y → G.map k₁ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y

Tactic:
_

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
⊢ ∀ (k₁ : X ⟶ F.obj X₁✝) (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁ ≫ F.map f_1 = k₂ → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y → G.map k₁ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
⊢ ∀ (k₁ : X ⟶ F.obj X₁✝) (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁ ≫ F.map f_1 = k₂ → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y → G.map k₁ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y

Tactic:
_

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
⊢ ∀ (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁✝ ≫ F.map f_1 = k₂ → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y → G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
⊢ ∀ (k₂ : X ⟶ F.obj X₂✝) (f_1 : X₁✝ ⟶ X₂✝),
    k₁✝ ≫ F.map f_1 = k₂ → G.map k₂ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y → G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y

Tactic:
_

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
⊢ ∀ (f_1 : X₁✝ ⟶ X₂✝),
    k₁✝ ≫ F.map f_1 = k₂✝ →
      G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y → G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y