mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) (f r • g)) 1 = r • ((CoextendScalars.equiv f X) g) 1

Tactic:
CoextendScalars.smul_apply,

Goal state after:
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) g) (1 * f r) = r • ((CoextendScalars.equiv f X) g) 1
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
⊢ ↑(TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ LinearMap.rTensor (A ⊗[R] B) comul ∘ₗ comul =
    LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul

Tactic:
by
  ext x y
  let F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S]
    A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
    AlgebraTensorModule.tensorTensorTensorComm _ _ _ _ _ _ _ _ ≪≫ₗ
      AlgebraTensorModule.congr (.refl _ _)
        (AlgebraTensorModule.tensorTensorTensorComm _ _ _ _ _ _ _ _)
  let F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S]
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
    TensorProduct.mapOfCompatibleSMul .. ∘ₗ
        TensorProduct.map .id (TensorProduct.mapOfCompatibleSMul ..) ∘ₗ F.toLinearMap
  convert! congr(F ($(Coalgebra.coassoc_apply x) ⊗ₜ[R] $(Coalgebra.coassoc_apply y))) using 1
  · dsimp
    hopf_tensor_induction comul (R := S) x with x₁ x₂
    hopf_tensor_induction comul (R := R) y with y₁ y₂
    dsimp
    hopf_tensor_induction comul (R := S) x₁ with x₁₁ x₁₂
    hopf_tensor_induction comul (R := R) y₁ with y₁₁ y₁₂
    rfl
  · dsimp
    hopf_tensor_induction comul (R := S) x with x₁ x₂
    hopf_tensor_induction comul (R := R) y with y₁ y₂
    dsimp
    hopf_tensor_induction comul (R := S) x₂ with x₂₁ x₂₂
    hopf_tensor_induction comul (R := R) y₂ with y₂₁ y₂₂
    rfl

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
mul_self,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a : α
⊢ a + a = 0
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
mul_self,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + a * b = a
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
mul_self,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + a * (a * b) = a
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
mul_self,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ 0 + (a + b * c + a * (b * c)) = a + b * c + a * (b * c)
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Bialgebra S A
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
x : A ⊗[R] R
⊢ (TensorProduct.rid R S A).toAlgEquiv x = (Algebra.TensorProduct.rid R S A) x

Tactic:
exact coalgebra_rid_eq_algebra_rid_apply x

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
x : R
inst✝ : Away x S
a b : R
h : (algebraMap R S) a = (algebraMap R S) b
⊢ ∃ n, x ^ n * a = x ^ n * b

Tactic:
obtain ⟨⟨-, n, rfl⟩, hx⟩ := IsLocalization.exists_of_eq (M := Submonoid.powers x) h

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
a b : R
h : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hx : ↑⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩ * a = ↑⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩ * b
⊢ ∃ n, x ^ n * a = x ^ n * b
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) y r * x ∈ univ * s * univ

Tactic:
exact ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I

Tactic:
refine fun h => le_antisymm (fun x hx => ?_) le_jacobson
    contrapose hx
    rw [Ideal.jacobson, mem_sInf]
    push Not
    exact h x hx

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ r * x - 1 ∈ I

Tactic:
rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel_right]; exact I.neg_mem hpi

Goal state after:
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
⊢ IsUnit (a + b) → IsUnit a ∨ IsUnit b

Tactic:
hab

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
a b : S
hab : IsUnit (a + b)
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ (η ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (λ_ X).hom

Tactic:
rw [← cancel_epi (λ_ X).inv]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M X Y : C
inst✝ : MonObj M
e : M ≅ X
⊢ (λ_ X).inv ≫ (η ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom = (λ_ X).inv ≫ (λ_ X).hom
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
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : Y ⟶ Z
inst✝ : IsMonHom f
⊢ η ≫ X ◁ f = η

Tactic:
by simpa using ((inferInstance : IsMonHom (𝟙 X ⊗ₘ f))).one_hom

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ↑R ((map S) l) =
    ↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)

Tactic:
rw [LinearEquiv.eq_toLinearMap_symm_comp, ← LinearEquiv.comp_toLinearMap_symm_eq]
  apply IsLocalizedModule.linearMap_ext S g₁ g₂
  rw [LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp]
  ext
  simp

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

Goal state before:
pp: 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'

Tactic:
· simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← comminr, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ ∀ {m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt},
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
      (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
intro m h₁ h₂
      dsimp at m h₁ h₂ ⊢
      ext
      · simpa using h₂
      · simp [← h₁]

Goal state after:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β : Type u₁}, mapConst = map ∘ Function.const β

Tactic:
by simp [mapConst, Functor.map]

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

Goal state before:
pp: X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
⊢ 0 = (Hom.hom f) 1

Tactic:
← f.hom.map_zero

Goal state after:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
⊢ (Hom.hom f) 0 = (Hom.hom f) 1
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : 0 = x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x

Tactic:
← f.hom.map_zero

Goal state after:
case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
e : (Hom.hom f) 0 = x
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) 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
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
⊢ g a = g b → a = b

Tactic:
hab

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
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
⊢ a = 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
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ iso S (mkLinearMap S M) = LinearEquiv.refl R (LocalizedModule S M)

Tactic:
let f := mkLinearMap S M
  obtain ⟨e, _, univ⟩ := is_universal S f f (map_units f)
  rw [← toLinearMap_inj, univ (iso S f) ((eq_toLinearMap_symm_comp f f).1 (iso_symm_comp S f).symm)]
  exact Eq.symm <| univ (refl R (LocalizedModule S M)) (by simp)

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

Goal state before:
pp: case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app (op one))) x)
⊢ (ConcreteCategory.hom (limit.π F (op zero))) x =
    (ConcreteCategory.hom (F.map (op left))) ((ConcreteCategory.hom (limit.π F (op one))) x)

Tactic:
exact (limit.w_apply F (op left) x).symm

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
⊢ ∀ (j j' : J), F j = F j'

Tactic:
have w := h { j | F j = F j₀ } rfl (fun {j₁} {j₂} f => by
      change F j₁ = F j₀ ↔ F j₂ = F j₀
      simp [a f])

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
w : ∀ (j : J), j ∈ {j | F j = F j₀}
⊢ ∀ (j j' : J), F j = F j'
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
X Y : C
⊢ ObjectProperty.Small.{w, v, u} (pair X Y)

Tactic:
dsimp [pair]
  infer_instance

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ (fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)) ≤ P

pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ P ≤ isoClosure fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)

Tactic:
· intro X hX
    simp only [Set.mem_range, Function.comp_apply, Subtype.exists] at hX
    obtain ⟨Y, hY, rfl⟩ := hX
    exact (φ ⟨Y, hY⟩).2

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ P ≤ isoClosure fun X ↦ X ∈ Set.range (Subtype.val ∘ φ)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
inst✝¹ : CommRing R
ι : Type u_1
inst✝ : Finite ι
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
cases nonempty_fintype ι
    let eqv := (MvPolynomial.renameEquiv R <| Fintype.equivFin ι).symm
    exact
      ⟨Fintype.card ι, eqv, eqv.surjective,
        ((RingHom.injective_iff_ker_eq_bot _).1 eqv.injective).symm ▸ Submodule.fg_bot⟩

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
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
Q : α → ObjectProperty C
x✝ : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ a, P a ≤ Q.isoClosure

Tactic:
refine ⟨⨆ a, Q a, inferInstance, ?_⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
Q : α → ObjectProperty C
x✝ : ∀ (a : α), ObjectProperty.Small.{w, v, u} (Q a)
hQ : ∀ (a : α), P a ≤ (Q a).isoClosure
⊢ ⨆ a, P a ≤ (⨆ a, Q a).isoClosure
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
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
⊢ FinitePresentation A B

Tactic:
let RX := MvPolynomial (Fin n) R

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
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
⊢ FinitePresentation A B
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
⊢ (∃ J x, Nonempty (P.FullSubcategory ≌ J)) ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
by
  refine ⟨fun ⟨J, _, ⟨e⟩⟩ ↦ ?_, fun _ ↦ ?_⟩
  · exact ⟨.ofObj (e.inverse ⋙ P.ι).obj, inferInstance,
      fun X hX ↦ ⟨_, ⟨⟨(e.functor.obj ⟨X, hX⟩)⟩, ⟨P.ι.mapIso (e.unitIso.app ⟨X, hX⟩)⟩⟩⟩⟩
  · obtain ⟨Q, _, h₁, h₂⟩ := EssentiallySmall.exists_small_le.{w} P
    rw [← isEquivalence_ιOfLE_iff h₁] at h₂
    exact ⟨_, _, ⟨((ιOfLE h₁).asEquivalence.symm.trans
      (Shrink.equivalence.{w} Q.FullSubcategory)).trans (ShrinkHoms.equivalence.{w'} _)⟩⟩

Goal state after:
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
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
by
    ext
    · simp [comp]
    · simp [comp, ← NatIso.naturality_2 (Cat.Hom.toNatIso (eqToIso (F.map_comp g.base h.base)) ≪≫
        (eqToIso (Cat.Hom.comp_toFunctor _ _))) f.fiber]

Goal state after:
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 : Fork f g
⊢ (Iso.refl c.op.unop.pt).hom ≫ c.ι = c.op.unop.ι

Tactic:
simp [op_unop_ι]

Goal state after:
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
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
refine ⟨F.obj (IsFiltered.coeq q₁ q₂),
        Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂), ?_⟩
      conv_lhs => rw [IsFiltered.coeq_condition]
      simp only [F.map_comp, ← reassoc_of% h, StructuredArrow.mk_hom_eq_self, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂) =
    (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂

Tactic:
pullbackAssoc_inv_fst_fst

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂) = pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
⊢ IsConnected (CostructuredArrow P.ι d)

Tactic:
by_cases hd : P d

Goal state after:
case pos
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
⊢ IsConnected (CostructuredArrow P.ι d)

case neg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : ¬P d
⊢ IsConnected (CostructuredArrow P.ι d)
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
⊢ P
      ((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' := ⋯ })).comp
        (CommRingCat.Hom.hom e₁.toCommRingCatIso.hom)) ↔
    P (IsLocalization.Away.map R' S' f r)

Tactic:
refine (hP.cancel_right_isIso (CommRingCat.ofHom _) e₂.toCommRingCatIso.hom).symm.trans ?_

Goal state after:
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
⊢ P
      ((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' := ⋯ }))) ↔
    P (IsLocalization.Away.map R' S' f r)