mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case id
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x : C
⊢ W' (𝟙 x)

Tactic:
exact W'.id_mem _

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x ∈
    (QuotientAddGroup.mk' (Relations F)).ker

Tactic:
QuotientAddGroup.ker_mk'

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j ↦ ↑(F.obj j)) j) x ∈
    Relations F
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
⊢ (fun β ↦
        TwoSquare.mk G L₁ L₂ H
          ((G ⋙ L₂).leftUnitor.inv ≫
            whiskerRight adj₁.unit (G ⋙ L₂) ≫
              ((L₁ ⋙ R₁).associator G L₂).inv ≫
                whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                  whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                    whiskerRight (L₁.associator H R₂).inv L₂ ≫
                      ((L₁ ⋙ H).associator R₂ L₂).hom ≫ (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
      ((fun α ↦
          TwoSquare.mk R₁ H G R₂
            ((R₁ ⋙ G).rightUnitor.inv ≫
              (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                  R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                    R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                      R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                        (R₁.associator L₁ (H ⋙ R₂)).inv ≫ whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
        α) =
    α

Tactic:
by
    ext
    simp only [comp_obj, whiskerLeft_comp, whiskerLeft_twice, assoc, Iso.hom_inv_id_assoc,
      whiskerRight_comp, comp_app, id_obj, leftUnitor_inv_app, Functor.whiskerRight_app,
      Functor.comp_map, associator_inv_app, associator_hom_app, map_id, Functor.whiskerLeft_app,
      rightUnitor_inv_app, leftUnitor_hom_app, rightUnitor_hom_app, comp_id, id_comp,
      counit_naturality, counit_naturality_assoc, left_triangle_components_assoc]
    rw [← assoc, ← Functor.comp_map, α.natTrans.naturality, Functor.comp_map, assoc, ← H.map_comp,
      left_triangle_components, map_id]
    simp only [comp_obj, comp_id]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul

Tactic:
by
  ext : 1
  · rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
  · rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
⊢ map ((↑f).copy f' h) ((↑f).copy f' h) ∘ₗ comul = comul ∘ₗ (↑f).copy f' h

Tactic:
simp only [(f : A →ₗ[R] B).copy_eq f' h,
      CoalgHomClass.map_comp_comul]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ↑(TensorProduct.assoc R B B B) ∘ₗ LinearMap.rTensor B comul ∘ₗ comul = LinearMap.lTensor B comul ∘ₗ comul

Tactic:
simp only [← ((f : A ≃ₗ[R] B).comp_toLinearMap_symm_eq _ _).2 f.map_comp_comul,
      ← LinearMap.comp_assoc]
    congr 1
    ext x
    simpa only [toCoalgHom_eq_coe, CoalgHom.toLinearMap_eq_coe, LinearMap.coe_comp,
      LinearEquiv.coe_coe, Function.comp_apply, ← (ℛ R _).eq, map_sum, TensorProduct.map_tmul,
      LinearMap.coe_coe, CoalgHom.coe_coe, LinearMap.rTensor_tmul, coe_symm_toLinearEquiv,
      symm_apply_apply, LinearMap.lTensor_comp_map, TensorProduct.sum_tmul,
      TensorProduct.assoc_tmul, TensorProduct.tmul_sum] using (sum_map_tmul_tmul_eq f f f x).symm

Goal state after:
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
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x y : S
⊢ g ((x + y) * s) = g (x * s) + g (y * s)

Tactic:
by rw [add_mul, map_add]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_3
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ ∀ (m : S) (x : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (m • x) =
      (RingHom.id S) m • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x

Tactic:
· intro s z
    change lift _ (s • z) = s • lift _ z
    induction z using TensorProduct.induction_on with
    | zero => rw [smul_zero, map_zero, smul_zero]
    | tmul s' x => simp [mul_smul]
    | add _ _ ih1 ih2 => rw [smul_add, map_add, ih1, ih2, map_add, smul_add]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
⊢ Bialgebra S (A ⊗[R] B)

Tactic:
by
  have hcounit := congr(DFunLike.coe $(counit_eq_algHom_toLinearMap R S A B))
  have hcomul := congr(DFunLike.coe $(comul_eq_algHom_toLinearMap R S A B))
  refine Bialgebra.mk' S (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_) <;>
  simp_all only [AlgHom.toLinearMap_apply] <;>
  simp only [map_one, map_mul]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ f aᶜ = (f a)ᶜ

Tactic:
← himp_bot,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ f (a ⇨ ⊥) = (f a)ᶜ
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ f (a ⇨ ⊥) = (f a)ᶜ

Tactic:
← himp_bot,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ f (a ⇨ ⊥) = f a ⇨ ⊥
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1.inl.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) y r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

pp: case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
· exact .inr <| ⟨x * y, ⟨x, mem_univ _, y, hy, rfl⟩, r, mem_univ _, mul_assoc ..⟩

Goal state after:
case refine_1.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

case refine_1.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a ∣ b
H : Function.Surjective ⇑(awayMap f a)
⊢ Function.Surjective ⇑(awayMap f b)

Tactic:
simp only [awayMap_surjective_iff] at H ⊢
  obtain ⟨b, rfl⟩ := h
  refine fun x ↦ ?_
  obtain ⟨c, m, e⟩ := H x
  exact ⟨b ^ m * c, m, by simp [mul_pow, e, mul_assoc, mul_left_comm]⟩

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

Goal state before:
pp: case neg
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)) 𝔪
⊢ x * r ∈ 𝔪

Tactic:
suffices x ∈ 𝔪₀ by simpa [𝔪₀] using this

Goal state after:
case neg
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)) 𝔪
⊢ x ∈ 𝔪₀
Module: Mathlib.RingTheory.Localization.Integer

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
inst✝ : IsLocalization M S
a : S
⊢ ∃ b, IsInteger R (a * (algebraMap R S) ↑b)

Tactic:
apply exists_integer_multiple'

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

Goal state before:
pp: case h
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'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ 1 •
      (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
        (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
    1 •
      ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
        ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)

Tactic:
simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm]

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 ⥤ D
E : D ⥤ C
inst✝¹ : E.IsEquivalence
inst✝ : HasLimit (K ⋙ E)
⊢ HasLimit K

Tactic:
rw [← hasLimit_iff_of_iso
    (isoWhiskerLeft K E.asEquivalence.unitIso.symm ≪≫ Functor.rightUnitor _)]

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 ⥤ D
E : D ⥤ C
inst✝¹ : E.IsEquivalence
inst✝ : HasLimit (K ⋙ E)
⊢ HasLimit (K ⋙ E.asEquivalence.functor ⋙ E.asEquivalence.inverse)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
⊢ IsLocalHom (Hom.hom (limit.π F (op one)))

Tactic:
refine Limits.π_isLocalHom _ (limit.isLimit _) (op one) fun x hx i ↦ ?_
  rcases i with _ | _
  · refine ⟨op zero, 𝟙 _, op left, inferInstance, ?_⟩
    simp only [CategoryTheory.Functor.map_id, hom_id, limit.cone_x, limit.cone_π,
      RingHom.id_apply]
    exact (limit.w_apply F (op left) x).symm
  · exact ⟨op one, 𝟙 _, 𝟙 _, inferInstance, by simp⟩

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

Goal state before:
pp: 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
⊢ IsLocalizedModule M f.toLinearMap

Tactic:
replace h₃ := fun x =>
    Iff.intro (h₃ x) fun ⟨⟨m, hm⟩, e⟩ =>
      (h₁ m hm).mul_left_cancel <| by
        rw [← Algebra.smul_def]
        simpa [Submonoid.smul_def] using f.congr_arg e
  constructor
  · 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]
  · exact h₂
  · intro x y
    dsimp only [AlgHom.toLinearMap_apply]
    rw [← sub_eq_zero, ← map_sub, h₃]
    simp_rw [smul_sub, sub_eq_zero]
    exact id

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

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ (J + K) ^ (n + m) ≤ I

Tactic:
add_pow,

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∑ m_1 ∈ Finset.range (n + m + 1), J ^ m_1 * K ^ (n + m - m_1) * ↑((n + m).choose m_1) ≤ I
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ((Finset.range (n + m + 1)).sup fun m_1 ↦ J ^ m_1 * K ^ (n + m - m_1) * ↑((n + m).choose m_1)) ≤ I

Tactic:
Finset.sup_le_iff

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∀ b ∈ Finset.range (n + m + 1), J ^ b * K ^ (n + m - b) * ↑((n + m).choose b) ≤ I
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
⊢ Ideal.comap ((↑e).comp f).toRingHom ⊥ = RingHom.ker f.toRingHom

Tactic:
hco,

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.toRingEquiv).comp f.toRingHom) ⊥ = RingHom.ker f.toRingHom
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1
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
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A ↑f.range

Tactic:
(AlgHom.range_eq_top _).mpr hf

Goal state after:
case refine_1
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
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A ↑⊤
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ AsSmall.up.map ((G.map (𝟙 Y✝.base)).toFunctor.map ((α.app Y✝.base).toFunctor.map f.fiber.down)) ≍
    AsSmall.up.map ((α.app Y✝.base).toFunctor.map f.fiber.down)

Tactic:
G.map_id

Goal state after:
case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ AsSmall.up.map ((𝟙 (G.obj Y✝.base)).toFunctor.map ((α.app Y✝.base).toFunctor.map f.fiber.down)) ≍
    AsSmall.up.map ((α.app Y✝.base).toFunctor.map f.fiber.down)
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
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
hom_comp :
  ∀ (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃),
    hom (f ≫ g) =
      hom f ≫ (F.map f).toFunctor.whiskerLeft (hom g) ≫ eqToHom (@_proof_146 C inst✝² F E inst✝ fib c₁ c₂ c₃ f g)
X✝ Y✝ Z✝ : Grothendieck F
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (hom (f ≫ g).base).app X✝.fiber ≫ (fib Z✝.base).map (f ≫ g).fiber =
    ((hom f.base).app X✝.fiber ≫ (fib Y✝.base).map f.fiber) ≫ (hom g.base).app Y✝.fiber ≫ (fib Z✝.base).map g.fiber

Tactic:
simp [hom_comp]

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

Goal state before:
pp: case star.of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
Y : C
f : star ⟶ of Y
⊢ G.map f ≫
      (match of Y with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

pp: case star.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
f : star ⟶ star
⊢ G.map f ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f

Tactic:
· cases f

Goal state after:
case star.star
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → F.obj x ⟶ Z
hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x
G : WithTerminal C ⥤ D
h : incl ⋙ G ≅ F
hG : G.obj star ≅ Z
hh : ∀ (x : C), G.map (starTerminal.from (incl.obj x)) ≫ hG.hom = h.hom.app x ≫ M x
f : star ⟶ star
⊢ G.map f ≫
      (match star with
        | of x => h.app x
        | star => hG).hom =
    (match star with
        | of x => h.app x
        | star => hG).hom ≫
      (lift F M hM).map f
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
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
j x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ s.π.app x✝¹ = s.π.app x✝

Tactic:
by simpa using s.w f

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

Goal state before:
pp: case h.none
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

Tactic:
exact hp

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

Goal state before:
pp: case h.none
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

Tactic:
exact hp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : WithTerminal (Discrete J)
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
constructor
  intro a b
  casesm* WithTerminal _, (_ : WithTerminal _) ⟶ (_ : WithTerminal _)
  · exact congr_arg (ULift.up ∘ PLift.up) rfl
  · rfl
  · rfl

Goal state after: