mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ)))
        ((ConcreteCategory.hom (c.ι.app j)) x)).down =
    ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)))
        ((ConcreteCategory.hom (c.ι.app j)) x)).down

Tactic:
← Quot.ι_desc _ c j x

Goal state after:
case refine_1
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ ψ : CharacterModule ↑c.pt
eq : (CharacterModule.dual (Quot.desc F c).toIntLinearMap) χ = (CharacterModule.dual (Quot.desc F c).toIntLinearMap) ψ
j : J
x : ↑(F.obj j)
⊢ ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv χ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down =
    ((ConcreteCategory.hom ((fun f ↦ ofHom f) (AddEquiv.ulift.symm.addMonoidHomCongrRightEquiv ψ)))
        ((Quot.desc F c) ((Quot.ι F j) x))).down
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : ↑x = ↑y
⊢ x = y

Tactic:
suffices (⟨x, hx⟩ : Ioc a (a + p)) = ⟨y, hy⟩ by exact Subtype.mk.inj this

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x y : 𝕜
hx : x ∈ Ioc a (a + p)
hy : y ∈ Ioc a (a + p)
h : ↑x = ↑y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), instTopologicalSpaceQuot] (equivIccQuot p a).toFun

Tactic:
isQuotientMap_quotient_mk'.continuous_iff,

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ Continuous[inst✝¹, instTopologicalSpaceQuot] ((equivIccQuot p a).toFun ∘ Quotient.mk')
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom ((underlyingIso (↟N.subtype)).inv ≫ (mk (↟N.subtype)).arrow)).range

pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = (Hom.hom (↟N.subtype)).range

Tactic:
· have :
            (underlyingIso (ofHom N.subtype)).inv =
              ofHom (underlyingIso (ofHom N.subtype)).symm.toLinearEquiv.toLinearMap := by
              ext x
              rfl
          rw [this, hom_comp, hom_ofHom, LinearEquiv.range_comp]

Goal state after:
case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = (Hom.hom (↟N.subtype)).range
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (finsuppTensorFinsupp' R X Y).toModuleIso.hom) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single y 1) =
    Finsupp.single (x, y) 1

Tactic:
finsuppTensorFinsupp'_single_tmul_single

Goal state after:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ Finsupp.single (x, y) (1 * 1) = Finsupp.single (x, y) 1
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact

Tactic:
exact₂_iff

Goal state after:
case mp.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).sc' ?mp.left.hS 0 1 2
      exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

case mp.left.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).IsComplex
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
exact₂_iff

Goal state after:
case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ ((mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).sc' ?mp.right.hS 0 1 2 exact₂_iff._proof_2
      exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

case mp.right.hS
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).IsComplex
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_2, u_2} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
k : ℕ
hk : k + 3 ≤ n
h₀ : S.map' k (k + 1) ⋯ ⋯ = 0
h₁ : S.map' (k + 2) (k + 3) ⋯ hk = 0
⊢ IsIso (S.map' (k + 1) (k + 2) ⋯ ⋯)

Tactic:
have := (hS.exact k).mono_g h₀
  have := (hS.exact (k + 1)).epi_f h₁
  apply isIso_of_mono_of_epi

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

Goal state before:
pp: case single
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f' : X ⟶ Y
r : R
⊢ (sum (single f' r ≫ g) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'

Tactic:
induction g using Finsupp.induction_linear with

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

Goal state before:
pp: case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ (r • F.map (single f' 1)) ≫ α.hom.app Y = α.hom.app X ≫ G.map (r • single f' 1)

Tactic:
G.map_smul,

Goal state after:
case single
R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
X Y : Free R C
f' : X ⟶ Y
r : R
⊢ (r • F.map (single f' 1)) ≫ α.hom.app Y = α.hom.app X ≫ (r • G.map (single f' 1))
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ Set.range ⇑(hom fst) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
by
  let e := h.isoPullback ≪≫ Types.pullbackIsoPullback f g
  have : fst = _root_.Prod.fst ∘ Subtype.val ∘ e.hom := by
    ext p
    suffices fst p = pullback.fst f g (h.isoPullback.hom p) by simpa
    rw [← comp_apply h.isoPullback.hom (pullback.fst f g), IsPullback.isoPullback_hom_fst]
  rw [this, Set.range_comp, Set.range_comp, Set.range_eq_univ.mpr (surjective_of_epi e.hom)]
  ext
  simp [eq_comm]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
m : E.pt ⟶ K.pt
hm : ∀ (j : WalkingMulticospan J), m ≫ K.π.app j = E.π.app j
i : J.L
⊢ m ≫ K.ι i = ι E i

Tactic:
apply hm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
m : K.pt ⟶ S.pt
hm : ∀ (j : WalkingMultispan J), K.ι.app j ≫ m = S.ι.app j
i : J.R
⊢ K.π i ≫ m = π S i

Tactic:
apply hm

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ (T.map (t.lift (T.forget.mapCone s)) ≫ t.lift (newCone D c)) ≫ c.π.app j =
    (s.pt.a ≫ t.lift (T.forget.mapCone s)) ≫ c.π.app j

Tactic:
rw [Category.assoc, Category.assoc, t.fac, newCone_π_app, ← Functor.map_comp_assoc,
            t.fac, Functor.mapCone_π_app]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (T.forget.map (s.π.app j)) ≫ (D.obj j).a = s.pt.a ≫ T.forget.map (s.π.app j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type w
inst✝ : LinearOrder ι
I : MultispanIndex (MultispanShape.prod ι) C
c : Multicofork I
hc : IsColimit c
h : I.SymmStruct
s : Multicofork I.toLinearOrder
m : c.toLinearOrder.pt ⟶ s.pt
hm : ∀ (i : (MultispanShape.ofLinearOrder ι).R), c.toLinearOrder.π i ≫ m = s.π i
i : (MultispanShape.prod ι).R
this : c.π i ≫ hc.desc (s.ofLinearOrder h) = (s.ofLinearOrder h).π i
⊢ c.π i ≫ m = (s.ofLinearOrder h).π i

Tactic:
apply hm

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ ∀ (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p

Tactic:
have hₗ : StructuredArrow.mk left ∈ p := (h₂ (StructuredArrow.homMk .left)).1 h₁

Goal state after:
case one
C : Type u
inst✝ : Category.{v, u} C
p : Set (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)
h₁ : StructuredArrow.mk (𝟙 WalkingReflexivePair.one) ∈ p
h₂ : ∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
hₗ : StructuredArrow.mk left ∈ p
⊢ ∀ (j : StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair), j ∈ p
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : HasEqualizerOfIsCosplitPair F
inst✝ : PreservesLimitOfIsCosplitPair F
⊢ ComonadicLeftAdjoint F

Tactic:
have : ReflectsLimitOfIsCosplitPair F := ⟨fun f g _ => by
    have := HasEqualizerOfIsCosplitPair.out F f g
    apply reflectsLimit_of_reflectsIsomorphisms⟩
  apply comonadicOfHasPreservesReflectsFSplitEqualizers adj

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
⊢ ∀ {c : Cone (F ⋙ R)} (hc : IsLimit c), Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Tactic:
intro c

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
⊢ ∀ (hc : IsLimit c), Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
Module: Mathlib.CategoryTheory.Monad.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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ c.ι.app j ≫ t.desc (newCocone D c) ≫ T.ε.app c.pt = c.ι.app j ≫ 𝟙 c.pt

Tactic:
simp only [Functor.comp_obj, forget_obj, Functor.id_obj,
      IsColimit.fac_assoc, newCocone_ι_app, assoc, NatTrans.naturality, Functor.id_map, comp_id]

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
⊢ ∀ {c : Cocone (F ⋙ R)} (hc : IsColimit c), Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
intro c

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cocone (F ⋙ R)
⊢ ∀ (hc : IsColimit c), Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddGroup β
inst✝ : DistribSMul α β
s : Set α
t : Set β
⊢ s • -t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]
  exact image_image2_right_comm smul_neg

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P✝ : Ideal B
Q : Ideal C
p✝ : Ideal A
inst✝⁶ : Q.LiesOver p✝
inst✝⁵ : P✝.LiesOver p✝
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
p : Ideal R
P : Ideal A
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
⊢ (map (mk (map (algebraMap R A) p)) P).IsPrime

Tactic:
apply Ideal.isPrime_map_quotientMk_of_isPrime
  rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]

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

Goal state before:
pp: case smul
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s : M
a✝¹ : R
x✝ : M
hx✝ : x✝ ∈ span R S
a✝ : r • x✝ ∈ N
⊢ r • a✝¹ • x✝ ∈ N

Tactic:
| smul =>

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
⊢ (Ideal.Quotient.mk I) x * ↑H.unit⁻¹ = 1

Tactic:
IsUnit.mul_val_inv

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
⊢ 1 = 1
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp.refine_2
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
J : Ideal S
h : J.IsPrime
x y : R
hxy : (algebraMap R S) (x * y) ∈ J
⊢ x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J

Tactic:
map_mul

Goal state after:
case mp.refine_2
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
J : Ideal S
h : J.IsPrime
x y : R
hxy : (algebraMap R S) x * (algebraMap R S) y ∈ J
⊢ x ∈ Ideal.under R J ∨ y ∈ Ideal.under R J
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case e_a.e_a
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ∑ x ∈ Finset.antidiagonal k, (algebraMap R A) (p₁.coeff x.1 * p₂.coeff x.2) =
    ∑ x ∈ Finset.antidiagonal k, (algebraMap R A) (p₁.coeff x.1) * (algebraMap R A) (p₂.coeff x.2)

Tactic:
map_mul

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯)
      ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m * (Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
map_mul

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.quotientMap I (algebraMap R S) H) ((Ideal.Quotient.mk J) (r * rn)) = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn) - mk' S r ⟨m, hm⟩) = 0

Tactic:
map_sub,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) (r * rn)) - (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩) = 0
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
this : IsUnit ((algebraMap R S) ↑⟨m * ↑y, hm⟩)
⊢ IsUnit ((algebraMap R S) ↑y)

Tactic:
map_mul

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
this : IsUnit ((algebraMap R S) m * (algebraMap R S) ↑y)
⊢ IsUnit ((algebraMap R S) ↑y)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x : R
y : ↥M
⊢ (algebraMap R T) x = (algebraMap S T) (mk' S x y) * (algebraMap R T) ↑⟨↑y, ⋯⟩

Tactic:
simp only [IsScalarTower.algebraMap_apply R S T, ← map_mul, mk'_spec]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z * x = 0

Tactic:
rw [← (map_units S s).mul_left_inj, mul_assoc, e, ← map_mul, hz, map_zero,
      zero_mul]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
⊢ ∀ (c : B) (x : B ⧸ Ideal.map (algebraMap A B) I),
    ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        (c • x) =
      c •
        ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
          x

Tactic:
intro c

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
c : B
⊢ ∀ (x : B ⧸ Ideal.map (algebraMap A B) I),
    ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        (c • x) =
      c •
        ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                  (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
                Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
          x
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x✝ : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
x : S
hx : x ∈ adjoin R ↑σ
this : TensorProduct.includeRight x ∈ Subalgebra.map TensorProduct.includeRight (adjoin R ↑σ)
⊢ 1 ⊗ₜ[R] x ∈ ↑(adjoin R ↑(Finset.image (⇑TensorProduct.includeRight) σ))

Tactic:
simpa [← Algebra.adjoin_image] using this

Goal state after: