mathlib-initiative/mathlib-tactics huggingface dataset:
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
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Away r A
⊢ Away ((algebraMap R S) r) (S ⊗[R] A)

Tactic:
simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]

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
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Away r A
⊢ IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (S ⊗[R] A)
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
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Away r A
⊢ Away ((algebraMap R S) r) (A ⊗[R] S)

Tactic:
simp only [IsLocalization.Away, ← Algebra.algebraMapSubmonoid_powers]

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
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Away r A
⊢ IsLocalization (Algebra.algebraMapSubmonoid S (Submonoid.powers r)) (A ⊗[R] S)
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
x y : LocalizedModule S M
⊢ (x + y).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
    x.liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + y.liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
refine x.induction_on₂ ?_ y
    intro m₁ m₂ t₁ t₂
    simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left s]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.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
K : J ⥤ C
E : C ⥤ D
inst✝¹ : E.IsEquivalence
inst✝ : HasColimit (K ⋙ E)
⊢ HasColimit K

Tactic:
hasColimit_iff_of_iso
    ((Functor.rightUnitor _).symm ≪≫ isoWhiskerLeft K E.asEquivalence.unitIso)

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
K : J ⥤ C
E : C ⥤ D
inst✝¹ : E.IsEquivalence
inst✝ : HasColimit (K ⋙ E)
⊢ HasColimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
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
y : LocalizedModule S M
a : M
b : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) y
⊢ LocalizedModule.mk a b = y

Tactic:
induction y with | _ a' b'
   =>  _ 

Goal state after:
case h.h
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
a : M
b : ↥S
a' : M
b' : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) (LocalizedModule.mk a' b')
⊢ LocalizedModule.mk a b = LocalizedModule.mk a' b'
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
⊢ IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S')) ↔
    Algebra.IsPushout R R' S S'

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ isPushout_of_isPushout ..⟩
  let e : R' ⊗[R] S ≃+* S' := ((CommRingCat.isPushout_tensorProduct R R' S).isoPushout ≪≫
      h.isoPushout.symm).commRingCatIsoToRingEquiv
  have h2 (r : R') : (CommRingCat.isPushout_tensorProduct R R' S).isoPushout.hom
      (r ⊗ₜ 1) = (pushout.inl (ofHom _) (ofHom _)) r :=
    congr($((CommRingCat.isPushout_tensorProduct R R' S).inl_isoPushout_hom).hom r)
  have h3 (x : R') := congr($(h.inl_isoPushout_inv) x)
  dsimp only [hom_comp, RingHom.coe_comp, Function.comp_apply, hom_ofHom] at h3
  let e' : R' ⊗[R] S ≃ₐ[R'] S' := {
    __ := e
    commutes' r := by simp [Iso.commRingCatIsoToRingEquiv, h2, e, h3] }
  refine Algebra.IsPushout.of_equiv e' ?_
  ext s
  have h1 : (CommRingCat.isPushout_tensorProduct R R' S).isoPushout.hom
      (algebraMap S (R' ⊗[R] S) s) = (pushout.inr (ofHom _) (ofHom _)) s :=
    congr($((CommRingCat.isPushout_tensorProduct R R' S).inr_isoPushout_hom).hom s)
  have h4 (x : S) := congr($(h.inr_isoPushout_inv) x)
  dsimp only [hom_comp, RingHom.coe_comp, Function.comp_apply, hom_ofHom] at h4
  simp [Iso.commRingCatIsoToRingEquiv, h1, e', e, h4]

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
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₁ x₂ : M₁
⊢ (liftOfLE S₁ S₂ h f₁ f₂) x₁ = (liftOfLE S₁ S₂ h f₁ f₂) x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
e

Goal state after:
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
M₁ : Type u_6
M₂ : Type u_7
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
x₁ x₂ : M₁
e : (liftOfLE S₁ S₂ h f₁ f₂) x₁ = (liftOfLE S₁ S₂ h f₁ f₂) x₂
⊢ ∃ c, c • x₁ = c • x₂
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
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective ⇑h
x : M
s : ↥S
y : M
t : ↥S
c : R
hc : c ∈ S
⊢ c • s • h y = c • t • h x → ∃ a ∈ S, a • s • y = a • t • x

Tactic:
e

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
N : Type u_6
N' : Type u_7
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N
inst✝¹ : Module R N'
g : N →ₗ[R] N'
inst✝ : IsLocalizedModule S g
h : M →ₗ[R] N
h_inj : Function.Injective ⇑h
x : M
s : ↥S
y : M
t : ↥S
c : R
hc : c ∈ S
e : c • s • h y = c • t • h x
⊢ ∃ a ∈ S, a • s • y = a • t • x
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ (inv η) = inv (F.map₂ η)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id
  simp [← F.map₂_comp η (inv η)]

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

Goal state before:
pp: case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ (x : ↥M), IsUnit ((algebraMap R (End R S')) ↑x)

pp: case surj
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ (y : S'), ∃ x, x.2 • y = f.toLinearMap x.1

pp: case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ {x₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
· intro x
    rw [Module.End.isUnit_iff]
    constructor
    · rintro a b (e : x • a = x • b)
      simp_rw [Submonoid.smul_def, Algebra.smul_def] at e
      exact (h₁ x x.2).mul_left_cancel e
    · intro a
      refine ⟨((h₁ x x.2).unit⁻¹ :) * a, ?_⟩
      rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]

Goal state after:
case surj
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ (y : S'), ∃ x, x.2 • y = f.toLinearMap x.1

case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ {x₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • x₂
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty C
h : P.op = Q.op
⊢ P = Q

Tactic:
by
  rw [← P.unop_op, ← Q.unop_op, h]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : σ → ↥S
p : MvPolynomial σ R
⊢ (aeval fun i ↦ ↑(x i)) p = ↑((aeval x) p)

Tactic:
convert! aeval_algebraMap_apply A x p

Goal state after:
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 : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
have := (isEquivalence_ιOfLE_iff h₁).2 h₂

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
this : (ιOfLE h₁).IsEquivalence
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
hfp : ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ ι_1 x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp

Goal state after:
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
⊢ ∃ ι_1 x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case refine_2
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
d : D
Z : (X : C) → (d ⟶ F.obj X) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : d ⟶ F.obj X₁) → (k₂ : d ⟶ F.obj X₂) → (f : X₁ ⟶ X₂) → k₁ ≫ F.map f = k₂ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : d ⟶ F.obj X₀
z : Z X₀ k₀
⊢ {j₁ j₂ : StructuredArrow d F} → (j₁ ⟶ j₂) → Z j₂.right j₂.hom → Z j₁.right j₁.hom

Tactic:
· exact fun f a ↦ h₂ _ _ _ _ f.right f.w a

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:

Tactic:
_ = map (𝟙 _) := map_id_eq.symm
      _ = map _ := ?_
      _ = map _ ⋙ map _ := map_comp_eq _ _

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
⊢ map (𝟙 (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F))
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: 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
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
by
    refine ⟨isColimitWhiskerEquiv F _ ?_⟩
    let hc' := isColimitOfPreserves H ((isColimitWhiskerEquiv F _).symm hc)
    exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
this : ∀ (i : Fin n), ∃ a, f' a = f (MvPolynomial.X i)
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
choose g hg using this

Goal state after:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
⊢ (RingHom.ker f.toRingHom).FG
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork f g
⊢ IsColimit c ≃ IsLimit c.unop

Tactic:
apply equivOfSubsingletonOfSubsingleton
  · intro h
    exact ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv walkingParallelPairOpEquiv.symm).toFun h)).unop
  · intro h
    exact (IsColimit.equivIsoColimit c.unopOpIso).toFun
      ((IsColimit.precomposeHomEquiv _ _).invFun ((IsColimit.whiskerEquivalenceEquiv _).toFun h.op))

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ s.fst ≫ pullback.snd f g ≫ g = s.snd ≫ pullback.snd f g ≫ g

Tactic:
← pullback.condition,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ s.fst ≫ pullback.fst f g ≫ f = s.snd ≫ pullback.fst f g ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
g₁ g₂ : Z ⟶ X
⊢ g₁ ≫ f = g₂ ≫ f → g₁ = g₂

Tactic:
e

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
g₁ g₂ : Z ⟶ X
e : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
f g : Arrow C
⊢ ∀ (x : f ≅ g), P f.hom → P g.hom

Tactic:
e

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
f g : Arrow C
e : f ≅ g
⊢ P f.hom → P g.hom
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
this : e = IsLocalization.Away.map R' S' f r
⊢ (CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          {
            toFun := fun x ↦
              (CommRingCat.Hom.hom
                  (CommRingCat.ofHom
                    {
                      toFun :=
                        (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                              ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
            map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) =
    IsLocalization.Away.map R' S' f r

Tactic:
convert! this

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)

Tactic:
e

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
e : X ≅ Y
⊢ ∀ (f : Y ⟶ Z),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

Tactic:
e

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
X Y Z : CommRingCat
e : Y ≅ Z
⊢ ∀ (f : X ⟶ Y),
    toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)