mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: ⊢ ∀ {X Y : MonCat} (f : X ⟶ Y),
    (inverse ⋙ functor).map f ≫
        (let __src := Equiv.refl (inverse.obj Y).X;
            { toEquiv := __src, map_mul' := ⋯ }).toMonCatIso.hom =
      (let __src := Equiv.refl (inverse.obj X).X;
            { toEquiv := __src, map_mul' := ⋯ }).toMonCatIso.hom ≫
        (𝟭 MonCat).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: ⊢ ∀ {X Y : Mon (Type u)} (f : X ⟶ Y),
    (functor ⋙ forget MonCat).map f ≫ (Iso.refl ((functor ⋙ forget MonCat).obj Y)).hom =
      (Iso.refl ((functor ⋙ forget MonCat).obj X)).hom ≫ (Mon.forget (Type u)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: ⊢ ∀ {X Y : CommMonCat} (f : X ⟶ Y),
    (CommMonTypeEquivalenceCommMon.inverse ⋙ CommMonTypeEquivalenceCommMon.functor).map f ≫
        (let __src := Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj Y).X;
            { toEquiv := __src, map_mul' := ⋯ }).toCommMonCatIso.hom =
      (let __src := Equiv.refl (CommMonTypeEquivalenceCommMon.inverse.obj X).X;
            { toEquiv := __src, map_mul' := ⋯ }).toCommMonCatIso.hom ≫
        (𝟭 CommMonCat).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp

Goal state before:
pp: ⊢ ∀ {X Y : GrpCat} (f : X ⟶ Y),
    (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).map f ≫
        (let __src := Equiv.refl ↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj Y);
            { toEquiv := __src, map_mul' := ⋯ }).toGrpIso.hom =
      (let __src := Equiv.refl ↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj X);
            { toEquiv := __src, map_mul' := ⋯ }).toGrpIso.hom ≫
        (𝟭 GrpCat).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_

Goal state before:
pp: ⊢ ∀ {X Y : CommGrpCat} (f : X ⟶ Y),
    (CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).map f ≫
        (let __src :=
              Equiv.refl ↑((CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).obj Y);
            { toEquiv := __src, map_mul' := ⋯ }).toCommGrpIso.hom =
      (let __src := Equiv.refl ↑((CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).obj X);
            { toEquiv := __src, map_mul' := ⋯ }).toCommGrpIso.hom ≫
        (𝟭 CommGrpCat).map f

Tactic:
by cat_disch

Goal state after:
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
this : (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom (↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv ≫ (mk (↟N.subtype)).arrow)).range

Tactic:
hom_comp,

Goal state after:
case e'_2
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
this : (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) =
    (Hom.hom (mk (↟N.subtype)).arrow ∘ₗ Hom.hom (↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv)).range
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (fst X X + snd X X) ▷ X ≫ (fst X X + snd X X) = (α_ X X X).hom ≫ X ◁ (fst X X + snd X X) ≫ (fst X X + snd X X)

Tactic:
by simp [add_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
exact hS x₂ hx₂

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

Goal state before:
pp: 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 : Free R C
f : X ⟶ Y
r : R
⊢ (lift R F).map (r • f) = r • (lift R F).map f

Tactic:
dsimp
    rw [Finsupp.sum_smul_index] <;> simp [Finsupp.smul_sum, mul_smul]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst✝¹ : HasPullback f₁ f₂
inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)
x : ToType (pullback f₁ f₂)
⊢ ∃ x₁ x₂, ∃ (h : (hom f₁) x₁ = (hom f₂) x₂), x = pullbackMk f₁ f₂ x₁ x₂ h

Tactic:
obtain ⟨⟨⟨x₁, x₂⟩, h⟩, rfl⟩ := (pullbackEquiv f₁ f₂).symm.surjective x
  exact ⟨x₁, x₂, h, rfl⟩

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

Goal state before:
pp: case left.right.snd
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
b' : J.R
⊢ (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd b')))
      ((fun j ↦
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
        (WalkingMulticospan.left (J.snd b'))) =
    (fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)))
      (WalkingMulticospan.right b')

Tactic:
dsimp
          exact (x.2 b').symm

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
R : D ⥤ C
inst✝ : R.Full
L : C ⥤ D
adj : L ⊣ R
X✝ Y✝ : D
f : (Monad.comparison adj).obj X✝ ⟶ (Monad.comparison adj).obj Y✝
⊢ (Monad.comparison adj).map (R.preimage f.f) = f

Tactic:
by cat_disch

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
R : D ⥤ C
inst✝ : R.Full
L : C ⥤ D
adj : R ⊣ L
X✝ Y✝ : D
f : (Comonad.comparison adj).obj X✝ ⟶ (Comonad.comparison adj).obj Y✝
⊢ (Comonad.comparison adj).map (R.preimage f.f) = f

Tactic:
by cat_disch

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
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
⊢ CreatesLimit K R

Tactic:
letI B := Comonad.forget (Adjunction.toComonad (comonadicAdjunction R))

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
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
⊢ CreatesLimit K R
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
h : a⁻¹ • x ∈ S
⊢ x ∈ a • S

Tactic:
by simpa using smul_mem_pointwise_smul a _ _ h

Goal state after:
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 • (fun x ↦ -x) '' t = (fun x ↦ -x) '' (s • t)

Tactic:
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
g h : ↥(MulAction.stabilizer G P)
⊢ algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B (g * h)) ⋯ =
    algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B g) ⋯ * algEquivOfEqMap p (MulSemiringAction.toAlgEquiv A B h) ⋯

Tactic:
ext ⟨x⟩
    exact congrArg (Ideal.Quotient.mk P) (mul_smul g h x)

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
⊢ (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical

Tactic:
split_ifs with hm

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
hm : m ∈ S
⊢ (S.colon {m}).radical = ⊤

case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
hm : m ∉ S
⊢ (S.colon {m}).radical = (S.colon Set.univ).radical
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
· rw [← span_singleton_le_iff_mem, ← mul_top (span {x}), ← h, mul_add,
        span_singleton_mul_span_singleton, add_le_iff, span_singleton_le_iff_mem]
      exact Or.inl ⟨mul_le_right, hxy⟩

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
obtain ⟨m, hm, hy⟩ := exists_le_maximal (I + span {y}) h

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
m : Ideal R
hm : m.IsMaximal
hy : I + span {y} ≤ m
⊢ x ∈ I ∨ y ∈ I.radical
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
⊢ (∀ n ∈ map N.mkQ P, x✝ • n = 0) ↔ x✝ ∈ N.colon ↑P

Tactic:
mem_colon

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) ↔ ∀ s ∈ ↑P, x✝ • s ∈ N
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case pos
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
hI : ⊥ ^ n = ⊥
⊢ 0 ^ 2 = 0

Tactic:
zero_pow two_ne_zero

Goal state after:
case pos
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
hI : ⊥ ^ n = ⊥
⊢ 0 = 0
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
x : R
y : ↥M
I : Ideal S
h : mk' S x y * (algebraMap R S) ↑y ∈ I
⊢ mk' S x y ∈ I

Tactic:
obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.1 (map_units S y)

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
x : R
y : ↥M
I : Ideal S
h : mk' S x y * (algebraMap R S) ↑y ∈ I
b : S
hb : (algebraMap R S) ↑y * b = 1
⊢ mk' S x y ∈ I
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
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
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ (algebraMap R S) (↑c * z') = ↑z * (algebraMap R S) ↑(c * s)

Tactic:
rw [map_mul, ← eq₂, Submonoid.coe_mul, map_mul, mul_left_comm]

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
⊢ IsFractionRing S T

Tactic:
apply isFractionRing_of_isLocalization M S T

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
⊢ M ≤ nonZeroDivisors R
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) I

Tactic:
by rw [hIJ, ← Ideal.comap_coe f, Ideal.comap_comap, RingEquiv.comp_symm, Ideal.comap_id]

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

Goal state before:
pp: case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝ : a ∈ s
⊢ ∀ b ∈ s,
    b ∉ P →
      ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)

Tactic:
b

Goal state after:
case left
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
a : S
a✝ : a ∈ s
b : S
⊢ b ∈ s →
    b ∉ P →
      ∀ c ∈ s, ∀ d ∈ s, d ∉ P → ∀ x ∉ P, x * (a * d) = x * (c * b) → ∃ a_6 ∉ P, a_6 ∈ s ∧ a_6 * (a * d) = a_6 * (c * b)
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.add
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 y : T ⊗[R] S
hx :
  ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ x * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy :
  ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ y * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ (x + y) * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx

Goal state after:
case h.add
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 y : T ⊗[R] S
hy :
  ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ y * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ (x + y) * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.RingTheory.Localization.Submodule

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
x : S
a : Set R
⊢ (∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z) → ∃ y ∈ Submodule.span R (⇑(algebraMap R S) '' a), ∃ z, x = mk' S 1 z • y

Tactic:
rintro ⟨y, hy, z, hz⟩
    refine ⟨algebraMap R S y, Submodule.map_mem_span_algebraMap_image _ _ hy, z, ?_⟩
    rw [hz, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

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

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ ((comp m m n n α) A).IsSymm ↔ ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'

Tactic:
simp [IsSymm.ext_iff]
  grind

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
⊢ AddMonoidAlgebra.single n r = C r * T n

Tactic:
by
  simp [C, T, single_mul_single]

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
← mvPolynomialX_mapMatrix_aeval ℤ A,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).adjugate.det =
    ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).det ^ (Fintype.card n - 1)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ ⅟A * (A * B) = B

Tactic:
← Matrix.mul_assoc,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ ⅟A * A * B = B
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ A * (⅟A * B) = B

Tactic:
← Matrix.mul_assoc,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ A * ⅟A * B = B
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : ℕ
h : i < (listTransvecRow M).length
⊢ (listTransvecRow M)[i] = transvection (inr ()) (inl ⟨i, ⋯⟩) (-M (inr ()) (inl ⟨i, ⋯⟩) / M (inr ()) (inr ()))

Tactic:
by
  simp [listTransvecRow]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : CommMagma R
A : Matrix m n R
B : Matrix n m R
⊢ (A * B).trace = (B * A).trace

Tactic:
rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * (B * C)).trace = (C * (A * B)).trace

Tactic:
← Matrix.mul_assoc,

Goal state after:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * B * C).trace = (C * (A * B)).trace