mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
by
  rw [← comp_τ₁, S.w₀₂, zero_τ₁]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀'.f ≫ S.φ₁ = S.v₁₂.τ₁

Tactic:
dsimp only [L₀']
  simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, φ₂, pullback.lift_fst_assoc,
    S.v₁₂.comm₁₂]

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

Goal state before:
pp: case single.add.h_add
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
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
intros; simp only [add_smul]

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

Goal state before:
pp: case single.add.h_add
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
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
intros; simp only [add_smul]

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

Goal state before:
pp: case add
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₁ f₂ : (X ⟶ Y) →₀ R
w₁ : F.map f₁ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₁
w₂ : F.map f₂ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₂
⊢ (α.app X).hom ≫ G.map f₁ + F.map f₂ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map (f₁ + f₂)

Tactic:
w₂,

Goal state after:
case add
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₁ f₂ : (X ⟶ Y) →₀ R
w₁ : F.map f₁ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₁
w₂ : F.map f₂ ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f₂
⊢ (α.app X).hom ≫ G.map f₁ + (α.app X).hom ≫ G.map f₂ = (α.app X).hom ≫ G.map (f₁ + f₂)
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
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
⊢ (hom fst) p = (hom (h.isoPullback.hom ≫ pullback.fst f g)) p

Tactic:
IsPullback.isoPullback_hom_fst

Goal state after:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
⊢ (hom fst) p = (hom fst) p
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)

Tactic:
apply IsCoreflexivePair.mk' _ _ _
  · apply (cofree T).map (T.ε.app X.A)
  · ext
    dsimp
    rw [← Functor.map_comp, X.counit, Functor.map_id]
  · ext
    apply Comonad.right_counit

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
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
K₁ K₂ : Multifork I
f : K₁ ⟶ K₂
⊢ ∀ (j : WalkingParallelPair), f.hom ≫ (Multifork.toPiFork hc hd K₂).π.app j = (Multifork.toPiFork hc hd K₁).π.app j

Tactic:
by
        rintro (_ | _)
        · apply Fan.IsLimit.hom_ext hc
          simp
        · apply Fan.IsLimit.hom_ext hd
          simp

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

Tactic:
dsimp
          rw [← Functor.map_comp_assoc, ← Category.assoc, t.fac, commuting, Category.assoc, t.fac]
          apply Algebra.Hom.h

Goal state after:
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 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_246✝ = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_246✝

Tactic:
app₀.hom_inv_id_assoc

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 2
app₀ : f.obj' 0 _proof_245✝ ≅ g.obj' 0 _proof_245✝
app₁ : f.obj' 1 _proof_246✝ ≅ g.obj' 1 _proof_246✝
app₂ : f.obj' 2 _proof_247✝ ≅ g.obj' 2 _proof_247✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_246✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_246✝
w₁ : f.map' 1 2 _proof_246✝ _proof_247✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_247✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_246✝ = f.map' 0 1 homMk₁._proof_4 _proof_246✝
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Flat (ULift.{t, u} R) M ↔ Flat R M

Tactic:
refine ⟨fun h ↦ .trans _ (ULift R) _, fun h ↦ ?_⟩
  have : Module.Flat (ULift.{t} R) R := .of_ulift
  let _ := ULift.algebra'
  exact .trans _ R _

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✝
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]
    rw [← Category.assoc, (D.obj j).counit, Category.id_comp]

Goal state after:
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 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_298✝ = app₀.hom ≫ app₀.inv ≫ f.map' 0 1 homMk₁._proof_4 _proof_298✝

Tactic:
app₀.hom_inv_id_assoc

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 3
app₀ : f.obj' 0 _proof_297✝ ≅ g.obj' 0 _proof_297✝
app₁ : f.obj' 1 _proof_298✝ ≅ g.obj' 1 _proof_298✝
app₂ : f.obj' 2 _proof_299✝ ≅ g.obj' 2 _proof_299✝
app₃ : f.obj' 3 _proof_300✝ ≅ g.obj' 3 _proof_300✝
w₀ : f.map' 0 1 homMk₁._proof_4 _proof_298✝ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 homMk₁._proof_4 _proof_298✝
w₁ : f.map' 1 2 _proof_246✝ _proof_299✝ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 _proof_246✝ _proof_299✝
w₂ : f.map' 2 3 _proof_299✝ _proof_300✝ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 _proof_299✝ _proof_300✝
⊢ f.map' 0 1 homMk₁._proof_4 _proof_298✝ = f.map' 0 1 homMk₁._proof_4 _proof_298✝
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)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt

Tactic:
apply (asIso ((comonadicAdjunction R).unit.app _)).trans

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 := ⋯
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ (R ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone c).pt
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ under A ⊥ = ⊥

Tactic:
under_bot

Goal state after:
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring A
inst✝³ : Semiring B
inst✝² : Algebra A B
inst✝¹ : FaithfulSMul A B
p : Ideal A
P : Ideal B
inst✝ : P.LiesOver p
hp : P = ⊥
⊢ ⊥ = ⊥
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I ≠ ⊤
⊢ Nonempty ↑I.minimalPrimes

Tactic:
obtain ⟨m, hm, hle⟩ := Ideal.exists_le_maximal I h
  obtain ⟨p, hp, -⟩ := Ideal.exists_minimalPrimes_le hle
  exact ⟨p, hp⟩

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

Goal state before:
pp: case neg
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI : I ^ n = ⊥
hI' : ¬I = ⊥
⊢ P I

Tactic:
rcases n with - | n

Goal state after:
case neg.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ 0 = ⊥
⊢ P I

case neg.succ
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1) = ⊥
⊢ P I
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ 0 = ⊥
⊢ P I

Tactic:
rw [pow_zero, Ideal.one_eq_top] at hI

Goal state after:
case neg.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : ⊤ = ⊥
⊢ P I
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1) = ⊥
⊢ P I

Tactic:
rcases n with - | n

Goal state after:
case neg.succ.zero
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
H : ∀ m < 0 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (0 + 1) = ⊥
⊢ P I

case neg.succ.succ
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ P I
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ I ^ (2 * n.succ) ≤ ⊥

Tactic:
← hI,

Goal state after:
case neg.succ.succ.a
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ I ^ (2 * n.succ) ≤ I ^ (n + 1 + 1)
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
z : S
⊢ Submodule.localized' S M (Algebra.linearMap R S) I = Submodule.span S (⇑(algebraMap R S) '' ↑I)

Tactic:
Submodule.localized'_eq_span,

Goal state after:
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
z : S
⊢ Submodule.span S (⇑(Algebra.linearMap R S) '' ↑I) = Submodule.span S (⇑(algebraMap R S) '' ↑I)
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
⊢ x ∈ J ∨ y ∈ J

Tactic:
obtain ⟨a, s, ha⟩ := exists_mk'_eq M x

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
⊢ x ∈ J ∨ y ∈ J
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp
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
⊢ J = ⊤ → ∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)

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
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → J = ⊤

Tactic:
· rintro rfl
    exact ⟨1, M.one_mem, ⟨⟩⟩

Goal state after:
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
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → 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
⊢ ((toFunBilinear R A) 1) 1 = 1

Tactic:
toFunBilinear_apply_apply,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ 1 • (aeval X) 1 = 1
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

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
N : Submonoid S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
x : Ideal R
H : x.IsPrime
inst✝ : IsDomain R
⊢ x.primeCompl ≤ nonZeroDivisors R

Tactic:
intro a ha

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
x : Ideal R
H : x.IsPrime
inst✝ : IsDomain R
a : R
ha : a ∈ x.primeCompl
⊢ a ∈ nonZeroDivisors R
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
⊢ (Ideal.map (algebraMap S S') P).LiesOver (Ideal.map (algebraMap R R') p)

Tactic:
suffices h : Ideal.map (algebraMap R R') (under R (under R' (P.map (algebraMap S S')))) =
      Ideal.map (algebraMap R R') p from ⟨by rw [← h, IsLocalization.map_under (M := M)]⟩
  rw [under_under, ← under_under (B := S), under_map_of_isPrime_disjoint _ _ ‹_› disj,
    LiesOver.over (P := P) (p := p)]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)

Tactic:
by
  rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]
  rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
I : Ideal R
⊢ Submodule.localized' S p (Algebra.linearMap R S) I = Submodule.span S (⇑(algebraMap R S) '' ↑I)

Tactic:
Submodule.localized'_eq_span,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
I : Ideal R
⊢ Submodule.span S (⇑(Algebra.linearMap R S) '' ↑I) = Submodule.span S (⇑(algebraMap R S) '' ↑I)
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = det 1

Tactic:
← coeff_det_X_add_C_card _ A,

Goal state after:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ a ∉ p.coeff.support → (Finsupp.single a (p.coeff a)) a = 0

Tactic:
intro ha

Goal state after:
case h₁
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
ha : a ∉ p.coeff.support
⊢ (Finsupp.single a (p.coeff a)) a = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ (A.submatrix ⇑e ⇑e).cramer b i = (A.cramer (b ∘ ⇑e.symm) ∘ ⇑e) i

Tactic:
simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
    det_submatrix_equiv_self e, Function.comp_def]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
M' : Submodule R M
⊢ lift.{uM, max uM uR}
      (Module.rank (FractionRing R) (LocalizedModule R⁰ M ⧸ Submodule.localized R⁰ M') +
        Module.rank (FractionRing R) ↥(Submodule.localized R⁰ M')) =
    lift.{uM, max uM uR} (Module.rank (FractionRing R) (LocalizedModule R⁰ M))

Tactic:
rank_quotient_add_rank_of_divisionRing

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ (Equiv.symm σ) i ≠ j

Tactic:
intro h'

Goal state after:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
h' : (Equiv.symm σ) i = j
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
⊢ ∏ i, of (fun i j ↦ (p j).coeff ↑i) i i = 1

Tactic:
convert! prod_const_one with x _

Goal state after:
case e'_2.a
R : Type v
inst✝ : CommRing R
n : ℕ
p : Fin n → R[X]
h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i
h_monic : ∀ (i : Fin n), (p i).Monic
x : Fin n
a✝ : x ∈ univ
⊢ of (fun i j ↦ (p j).coeff ↑i) x x = 1