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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ a + 1 + a * 1 = 1

Tactic:
mul_one,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
a : α
⊢ a + 1 + a = 1
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + b + (a * b + a * b * (a * b)) + (a * (b * b) + a * a * b) = a + b

Tactic:
by simp only [mul_self, add_self, add_zero]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case e'_2.e'_3
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hp : Irreducible p
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hx0 : ¬x = 0
⊢ p = normalize p

Tactic:
exact hnorm.symm

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (g x)
y : ↥(Submonoid.powers x)
⊢ IsUnit (g ↑y)

Tactic:
obtain ⟨n, hn⟩ := y.2
      rw [← hn, g.map_pow]
      exact IsUnit.map (powMonoidHom n : P →* P) hg

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ e * e = e * 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
n : ℕ
⊢ e * e = e
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
mul_one,

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r
⊢ 1 - s * b ∈ 𝔪₀
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
⊢ (algebraMap R (Away (↑a * ↑b))) (r a) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (algebraMap R (Away (↑a * ↑b))) (r b) * (algebraMap R (Away (↑a * ↑b))) (↑a ^ N)

Tactic:
← Away.awayToAwayRight_eq (S := Away a.1) a.1 b (r a),

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) ((algebraMap R (Away ↑a)) (r a)) * (algebraMap R (Away (↑a * ↑b))) (↑b ^ N) =
    (algebraMap R (Away (↑a * ↑b))) (r b) * (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✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨a, rfl⟩ := hf a

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : IsLocalRing R
inst✝² : Semiring S
inst✝¹ : Nontrivial S
f : R →+* S
inst✝ : IsLocalHom f
hf : Function.Surjective ⇑f
b : S
a : R
hab : IsUnit (f a + b)
⊢ IsUnit (f a) ∨ IsUnit b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * (mk' B a 1 * 1) = b * selfZPow x B d
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b

Tactic:
mul_one,

Goal state after:
case mp
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
a : R
b : B
m d : ℤ
h : selfZPow x B m * mk' B a 1 * selfZPow x B (-d) = b
this : selfZPow x B m * mk' B a 1 = b * selfZPow x B d
⊢ selfZPow x B m * mk' B a 1 = selfZPow x B d * b
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ η = (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ≫ μ

Tactic:
simp [tensorHom_def, H, ← unitors_equal]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
Z : C
f : Z ⟶ M
⊢ f ▷ 𝟙_ C ≫ M ◁ η ≫ μ = (ρ_ Z).hom ≫ f

Tactic:
mul_one,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : MonObj M
Z : C
f : Z ⟶ M
⊢ f ▷ 𝟙_ C ≫ (ρ_ M).hom = (ρ_ Z).hom ≫ f
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
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 ◁ η ≫ μ

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) ◁ (λ_ (𝟙_ C)).inv

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
| tensorμ M N (𝟙_ C) (𝟙_ C)

Tactic:
mul_one,

Goal state after:
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).hom ⊗ₘ 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) ◁ (λ_ (𝟙_ C)).inv

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
| tensorμ M N (𝟙_ C) (𝟙_ C)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (M ⊗ M) ◁ (λ_ (𝟙_ C)).hom ≫ (ρ_ (M ⊗ M)).hom ≫ μ =
    ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ

Tactic:
slice_lhs 1 3 => rw [← rightUnitor_monoidal]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ μ = ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ 𝟙 (M ⊗ M) ≫ μ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
⊢ (s.fst ≫ g₁) ≫ g₂ = s.snd ≫ i₃

Tactic:
rw [← s.condition, Category.assoc]

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ (s * 1) ⊗ₜ[R] (mk' A x y * (algebraMap R A) ↑y) = (algebraMap S (S ⊗[R] A)) ((algebraMap R S) x * s)

Tactic:
mul_one,

Goal state after:
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] (mk' A x y * (algebraMap R A) ↑y) = (algebraMap S (S ⊗[R] A)) ((algebraMap R S) x * 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
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''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ IsUnit ((algebraMap R (End R M'')) ↑s)

Tactic:
show algebraMap R (Module.End R M'') s = e ∘ₗ (algebraMap R (Module.End R M') s) ∘ₗ e.symm
      by ext; simp,

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''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
s : ↥S
⊢ IsUnit (↑e ∘ₗ (algebraMap R (End R M')) ↑s ∘ₗ ↑e.symm)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
⊢ h' (a ⊗ₜ[R] b) = (Hom.hom h) ((a * 1) ⊗ₜ[R] (1 * b))

Tactic:
mul_one,

Goal state after:
case property.right.right
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
a : A
b : B
⊢ h' (a ⊗ₜ[R] b) = (Hom.hom h) (a ⊗ₜ[R] (1 * b))
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 m s = 0 ↔ ∃ s', s' • m = 0

Tactic:
simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]

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'
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✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ (algebraMap R A) x • f m = x • f m

Tactic:
algebraMap_smul

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'
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✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : R
m : M
s t : ↥S
⊢ x • f m = x • f m
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R : CommRingCat
x✝ : of (ULift.{u, 0} ℤ) ⟶ R
⊢ Hom.hom x✝ = Hom.hom default

Tactic:
rw [← RingHom.cancel_right (f := (ULift.ringEquiv.{0, u} (R := ℤ)).symm.toRingHom)
        (hf := ULift.ringEquiv.symm.surjective)]

Goal state after:
R : CommRingCat
x✝ : of (ULift.{u, 0} ℤ) ⟶ R
⊢ (Hom.hom x✝).comp ULift.ringEquiv.symm.toRingHom = (Hom.hom default).comp ULift.ringEquiv.symm.toRingHom
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.isoClosure = P.unop.op.isoClosure

Tactic:
op_unop

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ P.isoClosure = P.isoClosure
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (Discrete.mk ∘ F) X✝ = (Discrete.mk ∘ F) Y✝

Tactic:
ext; exact h _ _ f

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

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

Tactic:
op_unop

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.Small.{w, v, u} P ↔ ObjectProperty.Small.{w, v, u} P
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
⊢ P.op ≤ Q.isoClosure.unop.op

Tactic:
op_unop

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
⊢ P.op ≤ Q.isoClosure
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.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
op_unop

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P ↔ ObjectProperty.EssentiallySmall.{w, v, u} P
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁶ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁵ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁴ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝³ : Q.IsMultiplicative
inst✝² : W.IsMultiplicative
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
A✝ B✝ : MorphismProperty.Comma L R P Q W
f : A✝ ⟶ B✝
hf : IsIso (Hom.hom f)
⊢ IsIso f

Tactic:
rw [← hom_homFromCommaOfIsIso f]

Goal state after:
A : Type u_1
inst✝⁶ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁵ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁴ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝³ : Q.IsMultiplicative
inst✝² : W.IsMultiplicative
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
A✝ B✝ : MorphismProperty.Comma L R P Q W
f : A✝ ⟶ B✝
hf : IsIso (Hom.hom f)
⊢ IsIso (homFromCommaOfIsIso (Hom.hom f))
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✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    G.map ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber) ≫
      (Grothendieck.ι F x✝.base ⋙ G).map f.fiber ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber

Tactic:
simp only [← Category.assoc, Functor.comp_obj, Functor.comp_map, ← G.map_comp]

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✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
x✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    G.map ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber ≫ (Grothendieck.ι F x✝.base).map f.fiber) ≫
      colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
⊢ IsIso (colimMap c.ι)

Tactic:
suffices colimMap c.ι = ((colimit.isColimit _).coconePointUniqueUpToIso hc ≪≫
      (isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit _)).hom by
    rw [this]; infer_instance
  ext j
  simp only [ι_colimMap, colimit.cocone_x, Iso.trans_hom,
    colimit.comp_coconePointUniqueUpToIso_hom_assoc]
  congr 1
  simp [← Iso.comp_inv_eq_id]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
⊢ { obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.map
        ((NatIso.ofComponents
                (fun F ↦
                  liftUnique (incl ⋙ F) (fun x ↦ F.map (starTerminal.from (of x))) ⋯ F (Iso.refl (incl ⋙ F))
                    (Iso.refl (F.obj star)) ⋯)
                ⋯).hom.app
          x) ≫
      (NatIso.ofComponents
              (fun F ↦
                Iso.refl
                  (({ obj := ofCommaObject, map := fun {X Y} ↦ ofCommaMorphism, map_id := ⋯, map_comp := ⋯ } ⋙
                        { obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }).obj
                    F))
              ⋯).hom.app
        ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.obj x) =
    𝟙 ({ obj := mkCommaObject, map := fun {X Y} ↦ mkCommaMorphism, map_id := ⋯, map_comp := ⋯ }.obj x)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, liftUnique, lift_obj, NatIso.ofComponents_hom_app,
      Iso.refl_hom, Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
⊢ mkCommaMorphism
      (NatIso.ofComponents
          (fun X ↦
            match X with
            | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
            | star => Iso.refl (x.obj star))
          ⋯).hom =
    𝟙 (mkCommaObject x)
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
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
⊢ x ∈ adjoin R (Set.range MvPolynomial.X)

Tactic:
adjoin_range_X

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)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
⊢ x ∈ ⊤