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

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
a : A' ⧸ f.range
c : CharacterModule (A' ⧸ f.range)
⊢ c a = 0

Tactic:
obtain ⟨b, rfl⟩ := QuotientAddGroup.mk'_surjective _ a

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ c ((QuotientAddGroup.mk' f.range.toAddSubgroup) b) = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
a✝ : Nontrivial 𝕜
⊢ {x | n • x = 0}.Finite

Tactic:
obtain rfl | h0 := eq_or_ne n 0

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
a✝ : Nontrivial 𝕜
hn : IsSMulRegular 𝕜 0
⊢ {x | 0 • x = 0}.Finite

case inr
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
a✝ : Nontrivial 𝕜
h0 : n ≠ 0
⊢ {x | n • x = 0}.Finite
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
a✝ : Nontrivial 𝕜
⊢ {x | n • x = 0}.Finite

Tactic:
obtain rfl | h0 := eq_or_ne n 0

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
a✝ : Nontrivial 𝕜
hn : IsSMulRegular 𝕜 0
⊢ {x | 0 • x = 0}.Finite

case inr
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
a✝ : Nontrivial 𝕜
h0 : n ≠ 0
⊢ {x | n • x = 0}.Finite
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
a✝ : Nontrivial 𝕜
hn : IsSMulRegular 𝕜 0
⊢ {x | 0 • x = 0}.Finite

pp: case inr
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℤ
hn : IsSMulRegular 𝕜 n
a✝ : Nontrivial 𝕜
h0 : n ≠ 0
⊢ {x | n • x = 0}.Finite

Tactic:
exacts [hn.not_zero.elim, ENat.card_lt_top.mp <|
    (card_torsion_le_of_isSMulRegular_int p n h0 hn).trans_lt <| ENat.natCast_lt_top _]

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
⊢ S.IsComplex

Tactic:
refine IsComplex.mk (fun i hi => ?_)

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 2
h :
  S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
      S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
    0
i : ℕ
hi : i + 2 ≤ 2
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y X' : Type u
f : X ⟶ Y
⊢ (free R).obj X' ◁ (free R).map f ≫ (μIso R X' Y).hom = (μIso R X' X).hom ≫ (free R).map (X' ◁ f)

Tactic:
rw [← cancel_epi (μIso R X' X).inv]
        aesop

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

Goal state before:
pp: case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ (sum g fun i a ↦ single (h ≫ i) (s * (r * a))) a✝ = (sum g fun a b ↦ r • single (h ≫ a) (s * b)) a✝

Tactic:
simp [mul_left_comm]

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

Goal state before:
pp: case e_g
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
h : X ⟶ Y
s : R
a✝ : X ⟶ Z
⊢ ∀ (i : Y ⟶ Z), single (h ≫ i) (s * 0) = 0

Tactic:
simp [mul_left_comm]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ X.a ≫ (reflectorAdjunction R).unit.app X.A = 𝟙 ((reflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.id_obj]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ X.a ≫ (reflectorAdjunction R).unit.app X.A = 𝟙 ((reflector R ⋙ R).obj X.A)
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ (coreflectorAdjunction R).counit.app X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)

Tactic:
dsimp only [Functor.id_obj]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Coreflective R
X : (coreflectorAdjunction R).toComonad.Coalgebra
⊢ (coreflectorAdjunction R).counit.app X.A ≫ X.a = 𝟙 ((coreflector R ⋙ R).obj X.A)
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.η.app (D.obj j).A ≫ (D.obj j).a ≫ c.ι.app j = c.ι.app j ≫ 𝟙 c.pt

Tactic:
Algebra.unit_assoc (D.obj j)

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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ c.ι.app j = c.ι.app j ≫ 𝟙 c.pt
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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.map (T.map (c.ι.app j)) ≫ T.μ.app c.pt ≫ lambda c t = T.map (T.map (c.ι.app j)) ≫ T.map (lambda c t) ≫ lambda c t

Tactic:
show (T : C ⥤ C).map ((T : C ⥤ C).map _) ≫ _ ≫ _ = _ from T.μ.naturality_assoc _ _,

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 : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ T.μ.app ((D ⋙ T.forget).obj j) ≫ T.map (c.ι.app j) ≫ lambda c t =
    T.map (T.map (c.ι.app j)) ≫ T.map (lambda c t) ≫ lambda c t
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : Flat R S
inst✝ : Flat S M
⊢ Flat R M

Tactic:
rw [Flat.iff_lTensor_injectiveₛ]

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : Flat R S
inst✝ : Flat S M
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(LinearMap.lTensor M N.subtype)
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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ c.π.app B = c.π.app A ≫ (D.map f).f

Tactic:
← c.w

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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ c.π.app ?m.162 ≫ (D ⋙ T.forget).map ?m.164 = c.π.app A ≫ (D.map f).f

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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ ?m.162 ⟶ B

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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ J
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ g.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.inv = app₄.inv ≫ f.map' 4 5 _proof_453✝ _proof_454✝

Tactic:
map'_inv_eq_inv_map' (by valid) app₄ app₅ w₄

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 _proof_449✝ ≅ g.obj' 0 _proof_449✝
app₁ : f.obj' 1 _proof_450✝ ≅ g.obj' 1 _proof_450✝
app₂ : f.obj' 2 _proof_451✝ ≅ g.obj' 2 _proof_451✝
app₃ : f.obj' 3 _proof_452✝ ≅ g.obj' 3 _proof_452✝
app₄ : f.obj' 4 _proof_453✝ ≅ g.obj' 4 _proof_453✝
app₅ : f.obj' 5 _proof_454✝ ≅ g.obj' 5 _proof_454✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_450✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_450✝
w₁ : f.map' 1 2 _proof_246✝ _proof_451✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_451✝
w₂ : f.map' 2 3 _proof_299✝ _proof_452✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_452✝
w₃ : f.map' 3 4 _proof_364✝ _proof_453✝ ≫ app₄.hom = app₃.hom ≫ g.map' 3 4 _proof_364✝ _proof_453✝
w₄ : f.map' 4 5 _proof_453✝ _proof_454✝ ≫ app₅.hom = app₄.hom ≫ g.map' 4 5 _proof_453✝ _proof_454✝
⊢ app₄.inv ≫ f.map' 4 (4 + 1) ⋯ ⋯ = app₄.inv ≫ f.map' 4 5 _proof_453✝ _proof_454✝
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
⊢ ⊥.colon S = (span R S).annihilator

Tactic:
aesop (add simp [mem_colon, mem_annihilator_span])

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ x✝ ∈ (map N.mkQ P).annihilator ↔ x✝ ∈ N.colon ↑P

Tactic:
mem_annihilator,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
x✝ : R
⊢ (∀ n ∈ map N.mkQ P, x✝ • n = 0) ↔ x✝ ∈ N.colon ↑P
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
A : Matrix ι ι R
this : (LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A) = A
⊢ IsNilpotent (toLin' A) ↔ IsNilpotent ((LinearMap.toMatrix (Pi.basisFun R ι) (Pi.basisFun R ι)) (toLin' A))

Tactic:
rw [LinearMap.isNilpotent_toMatrix_iff]

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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (I ^ n)) x) ↔ IsUnit ((mk I) x)

Tactic:
← IsNilpotent.isUnit_quotient_mk_iff (I := Ideal.map (Ideal.Quotient.mk (I ^ n)) I)

Goal state after:
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x)) ↔ IsUnit ((mk I) x)

case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
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
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime

Tactic:
refine fun h => ⟨fun hJ => h.left.ne_top (eq_top_iff.2 ?_), ?_⟩

Goal state after:
case mpr.refine_1
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 : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
hJ : J = ⊤
⊢ ⊤ ≤ Ideal.under R J

case mpr.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 : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
⊢ ∀ {x y : S}, x * y ∈ J → x ∈ J ∨ y ∈ J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr.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 : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : mk' S (a * b) (s * t) ∈ J
⊢ x ∈ J ∨ y ∈ J

Tactic:
rw [mk'_mem_iff, ← Ideal.mem_comap] at this

Goal state after:
case mpr.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 : (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
x y : S
hxy : x * y ∈ J
a : R
s : ↥M
ha : mk' S a s = x
b : R
t : ↥M
hb : mk' S b t = y
this : a * b ∈ Ideal.comap (algebraMap R S) J
⊢ x ∈ J ∨ y ∈ J
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k

Tactic:
conv_rhs => rw [coeff_mul]

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))).coeff x.1 *
        (∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff x.2
Module: Mathlib.RingTheory.Localization.Ideal

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
I : Ideal R
⊢ Ideal.map (algebraMap R S) I.radical = (Ideal.map (algebraMap R S) I).radical

Tactic:
by
  refine (I.map_radical_le (algebraMap R S)).antisymm ?_
  rintro x ⟨n, hn⟩
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
  simp only [← IsLocalization.mk'_pow, IsLocalization.mk'_mem_map_algebraMap_iff M] at hn ⊢
  obtain ⟨s, hs, h⟩ := hn
  refine ⟨s, hs, n + 1, by convert! I.mul_mem_left (s ^ n * x) h; ring⟩

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.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⟩)

Tactic:
rw [Ideal.quotientMap_mk, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem, ←
      Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, mk'_eq_mul_mk'_one]

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) ((algebraMap R S) r * mk' S 1 ⟨m, hm⟩)
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
⊢ RingHom.ker (map Q g ⋯) = Ideal.map (algebraMap R S) (RingHom.ker g)

Tactic:
by
  ext x
  obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
  simp [RingHom.mem_ker, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    IsLocalization.mk'_mem_map_algebraMap_iff, ← hT]

Goal state after:
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
y : T
⊢ ∃ x, y * (algebraMap S T) ↑x.2 = (algebraMap S T) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj N y

Goal state after:
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
y : T
x : R
s : ↥N
e : y * (algebraMap R T) ↑(x, s).2 = (algebraMap R T) (x, s).1
⊢ ∃ x, y * (algebraMap S T) ↑x.2 = (algebraMap S T) x.1
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
x✝¹ x✝ : R
⊢ (algebraMap R S) x✝¹ = (algebraMap R S) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝

Tactic:
rw [IsLocalization.eq_iff_exists M]
    exact fun ⟨x, hx⟩ => ⟨⟨_, h x.prop⟩, hx⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁸ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝⁶ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G).ker =
      ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F).range
J : Ideal R
hJ : J.IsMaximal
x : Nₚ J
this :
  ∀ (x : Nₚ J),
    ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) x = 0 ↔
      ∃ y, ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F) y = x
⊢ ((IsLocalizedModule.map J.primeCompl (g J) (h J)) G) x = 0 ↔
    ∃ y, ((IsLocalizedModule.map J.primeCompl (f J) (g J)) F) y = x

Tactic:
exact this x

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁸ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁷ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝⁶ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G).ker =
      ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F).range
r : ↑s
x : Nₚ r
this :
  ∀ (x : Nₚ r),
    ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
      ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G) x = 0 ↔
    ∃ y, ((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F) y = x

Tactic:
exact this x

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S ↔
    ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
by
  constructor <;> intro hσ
  · intro s
    obtain ⟨⟨⟨x, hx⟩, ⟨t, ht⟩, ht'⟩, h⟩ := hσ.1.2 s
    exact ⟨t, ht, ht', h ▸ hx⟩
  · constructor; constructor
    · exact fun y ↦ y.prop
    · intro s
      obtain ⟨t, ht, ht', h⟩ := hσ s
      exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩
    · intro x y e
      exact ⟨1, by simpa using Subtype.ext e⟩

Goal state after: