mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (Away.awayToAwayRight ↑a ↑b) (f a) * (Away.awayToAwayRight ↑a ↑b) ((algebraMap R (Away ↑a)) (↑a ^ N)) *
      (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (Away.awayToAwayLeft ↑b ↑a) (f b) * (Away.awayToAwayLeft ↑b ↑a) ((algebraMap R (Away ↑b)) (↑b ^ N)) *
      (algebraMap R (Away (↑a * ↑b))) (↑a ^ N)

Tactic:
Away.awayToAwayRight_eq,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝ : ↑↑s → R
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝ a)
N : ℕ := s.attach.sup n
r : ↑↑s → R := fun a ↦ ↑a ^ (N - n a) * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ (Away.awayToAwayRight ↑a ↑b) (f a) * (algebraMap R (Away (↑a * ↑b))) (↑a ^ N) *
      (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (Away.awayToAwayLeft ↑b ↑a) (f b) * (Away.awayToAwayLeft ↑b ↑a) ((algebraMap R (Away ↑b)) (↑b ^ N)) *
      (algebraMap R (Away (↑a * ↑b))) (↑a ^ N)
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
⊢ ∃ a_1, (Units.map ↑f) a_1 = a

Tactic:
obtain ⟨b, hb⟩ := hf (a : S)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
a : Sˣ
b : R
hb : f b = ↑a
⊢ ∃ a_1, (Units.map ↑f) a_1 = a
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f

Tactic:
have : IsIso (F.map f) := (H _ h_1).isIso_from _

Goal state after:
case neg.refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
j : J
h_1 : ¬j = i
f : j ⟶ i
this : IsIso (F.map f)
⊢ ((Functor.const J).obj (F.1 i)).map f ≫ eqToHom ⋯ = (H j h_1).from (((Functor.const J).obj (F.1 i)).obj j) ≫ F.map f
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = ↑n.natAbs - ↑m.natAbs

Tactic:
Int.natAbs_of_nonneg hn,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ n + m = n - ↑m.natAbs
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ a ∈ ↑S, IsUnit ((algebraMap R Aₛ) a)) ↔ ∀ a ∈ ⇑(algebraMap R A) '' ↑S, IsUnit ((algebraMap A Aₛ) a)

Tactic:
Set.forall_mem_image,

Goal state after:
case refine_1
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ (∀ a ∈ ↑S, IsUnit ((algebraMap R Aₛ) a)) ↔ ∀ ⦃x : R⦄, x ∈ ↑S → IsUnit ((algebraMap A Aₛ) ((algebraMap R A) x))
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
e : M ≅ X
⊢ IsMonHom e.hom

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.tacticLet__
    "let"
    (Term.letConfig [])
    (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" (Term.app `MonObj.ofIso [`e]))))
   ";"
   (Tactic.exact
    "exact"
    (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))]))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| tensorμ M N (M ⊗ M) (N ⊗ N) ≫ (M ◁ μ ⊗ₘ N ◁ μ)

pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ tensorμ M N M N

Tactic:
rw [← tensorμ_natural_right]

Goal state after:
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N

case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| μ ⊗ₘ μ

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
| (M ⊗ N) ◁ tensorμ M N M N
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O X : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
A : Mon C
⊢ μ ≫ η = (η ⊗ₘ η) ≫ μ

Tactic:
simp [unitors_equal]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ IsPullback fst' snd' f' g'

Tactic:
apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm

Goal state after:
case commfst
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ fst ≫ e₂.symm.hom = e₁.symm.hom ≫ fst'

case commsnd
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ snd ≫ e₃.symm.hom = e₁.symm.hom ≫ snd'

case commf
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ f ≫ e₄.symm.hom = e₂.symm.hom ≫ f'

case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ g ≫ e₄.symm.hom = e₃.symm.hom ≫ g'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ IsPushout f' g' inl' inr'

Tactic:
apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm

Goal state after:
case commf
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'

case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'

case comminl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'

case comminr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝²¹ : CommSemiring R
S✝ : Submonoid R
A : Type u_2
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : IsLocalization S✝ A
M : Type u_3
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
M' : Type u_4
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M'
inst✝¹³ : Module A M'
inst✝¹² : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring B
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T B
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : IsScalarTower R T B
inst✝⁴ : IsScalarTower R A B
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
this✝ : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this : IsScalarTower A Aₚ M'
⊢ IsLocalizedModule S ((AlgebraTensorModule.rTensor R N) g)

Tactic:
have : IsScalarTower R Aₚ M' :=
    IsScalarTower.of_algebraMap_smul <| fun r x ↦ by simp [IsScalarTower.algebraMap_apply R A Aₚ]

Goal state after:
R : Type u_1
inst✝²¹ : CommSemiring R
S✝ : Submonoid R
A : Type u_2
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : IsLocalization S✝ A
M : Type u_3
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
M' : Type u_4
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M'
inst✝¹³ : Module A M'
inst✝¹² : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring B
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T B
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : IsScalarTower R T B
inst✝⁴ : IsScalarTower R A B
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
this✝¹ : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this✝ : IsScalarTower A Aₚ M'
this : IsScalarTower R Aₚ M'
⊢ IsLocalizedModule S ((AlgebraTensorModule.rTensor R N) g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimit (cospan f g) F

Tactic:
apply preservesLimit_of_preserves_limit_cone h.isLimit

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ IsLimit (F.mapCone h.cone)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ IsLimit (F.mapCone h.cone)

Tactic:
exact (PullbackCone.isLimitMapConeEquiv _ _).symm hF.isLimit

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
⊢ IsSplitEpi (T.ε.app X) ↔ IsIso (T.ε.app X)

Tactic:
by
  refine ⟨fun _ ↦ ⟨section_ (T.ε.app X), ?_, by simp⟩, fun _ ↦ inferInstance⟩
  rw [← map_id, ← show section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 X from IsSplitEpi.id (T.ε.app X),
    map_comp, T.map_counit_app X, T.counit_naturality]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_6
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ m, m * ↑x ∈ S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule S f
x : ↥T
⊢ IsUnit ((algebraMap R (End R N)) ↑x)

Tactic:
obtain ⟨m, mx⟩ := h' x

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_6
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ m, m * ↑x ∈ S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule S f
x : ↥T
m : R
mx : m * ↑x ∈ S
⊢ IsUnit ((algebraMap R (End R N)) ↑x)
Module: Mathlib.CategoryTheory.Limits.ConeCategory

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ Y✝ : CostructuredArrow (const J) F
f : X✝ ⟶ Y✝
j : J
⊢ f.left ≫ { pt := Y✝.left, π := Y✝.hom }.π.app j = { pt := X✝.left, π := X✝.hom }.π.app j

Tactic:
by
        convert! congr_fun (congr_arg NatTrans.app f.w) j
        simp

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : Algebra R X✝
inst✝³ : CommRing Y✝
inst✝² : Algebra R Y✝
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
X Y : CommAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommAlgCat R)).map f)
i : (forget (CommAlgCat R)).obj X ≅ (forget (CommAlgCat R)).obj Y := asIso ((forget (CommAlgCat R)).map f)
e : ↑X ≃ₐ[R] ↑Y :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑↑__src.toRingHom).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
⊢ IsIso f

Tactic:
exact (isoMk e).isIso_hom

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom

Tactic:
RingHom.ker_eq_comap_bot,

Goal state after:
case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
hco : ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom
⊢ Ideal.comap ((↑e).comp f).toRingHom ⊥ = RingHom.ker f.toRingHom
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ (comp (comp f g) h).base = (comp f (comp g h)).base

pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ eqToHom ⋯ ≫ (comp (comp f g) h).fiber = (comp f (comp g h)).fiber

Tactic:
· simp [comp]

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ eqToHom ⋯ ≫ (comp (comp f g) h).fiber = (comp f (comp g h)).fiber
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) ≅ pre F G.functor ⋙ preInv F G

Tactic:
refine (eqToIso ?_)
      ≪≫ (Grothendieck.preUnitIso F G |> isoWhiskerLeft (map _))
      ≪≫ (pre_comp_map_assoc G.functor _ _ |> Eq.symm |> eqToIso)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ map (whiskerRight G.unitInv (G.functor ⋙ F))
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
⊢ IsConnected (StructuredArrow d F)

Tactic:
have : Nonempty (StructuredArrow d F) := by
      have := (I d).inv PUnit.unit
      obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
      exact ⟨StructuredArrow.mk y⟩
    apply zigzag_isConnected
    rintro ⟨⟨⟨⟩⟩, X₁, f₁⟩ ⟨⟨⟨⟩⟩, X₂, f₂⟩
    let y₁ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
    let y₂ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
    have e : y₁ = y₂ := by
      apply (I d).toEquiv.injective
      ext
    have t := Types.colimit_eq.{v, v} e
    clear e y₁ y₂
    exact Final.zigzag_of_eqvGen_colimitTypeRel t

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ RingHom.ker f.toRingHom = Ideal.map g.toRingHom (RingHom.ker (f.comp g).toRingHom)

Tactic:
RingHom.ker_eq_comap_bot,

Goal state after:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap f.toRingHom ⊥ = Ideal.map g.toRingHom (Ideal.comap (f.comp g).toRingHom ⊥)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ P.RespectsIso

Tactic:
apply RespectsIso.of_respects_arrow_iso
  intro f g e
  exact of_isPullback (IsPullback.of_horiz_isIso (CommSq.mk e.inv.w))

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hPQ : CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ P) fun {R S} [CommRing R] [CommRing S] ↦ Q
h : Q (algebraMap R T)
H : P Algebra.TensorProduct.includeRight.toRingHom
x✝ : Algebra T (S ⊗[R] T) := Algebra.TensorProduct.rightAlgebra
⊢ P (algebraMap R S)

Tactic:
apply hPQ h H

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.IsStableUnderComposition
inst✝¹ : P.RespectsIso
inst✝ : P.IsStableUnderBaseChange
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
h₁ : P.diagonal x✝¹
h₂ : P.diagonal x✝
⊢ P (pullback.diagonal (x✝¹ ≫ x✝))

Tactic:
pullback.diagonal_comp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.RespectsIso
inst✝ : P.IsStableUnderBaseChange
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
h₁ : P.diagonal x✝¹
h₂ : P.diagonal x✝
⊢ P
    (pullback.diagonal x✝¹ ≫
      (pullbackDiagonalMapIdIso x✝¹ x✝¹ x✝).inv ≫
        pullback.snd (pullback.diagonal x✝) (pullback.map (x✝¹ ≫ x✝) (x✝¹ ≫ x✝) x✝ x✝ x✝¹ x✝¹ (𝟙 Z✝) ⋯ ⋯))
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 (Over.Hom.left ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)))

Tactic:
exact P.overPullbackMap f _ (by simpa)

Goal state after: