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

Goal state before:
pp: A : CommGrpCat
⊢ (β_ (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X
          (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X).hom ≫
      μ =
    μ

Tactic:
ext ⟨x : A, y : A⟩
            exact CommMonoid.mul_comm y x

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

Goal state before:
pp: 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

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 ⋯)).sc' ?mp.left.hS 0 1 2
      exact₂_iff._proof_2 exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact

Tactic:
· rw [isComplex₂_iff]
        exact h.toIsComplex.zero 0

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' ⋯ 0 1 2 exact₂_iff._proof_2
      exact₂_iff._proof_4 isComplex₂_iff._proof_5).Exact
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
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (sum f fun f' s ↦ (g + g').sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    (sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)) +
      sum f fun f' s ↦ sum g' fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
← Finsupp.sum_add

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (sum f fun f' s ↦ (g + g').sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    sum f fun a b ↦ (sum g fun g' t ↦ single (a ≫ g') (b * t)) + sum g' fun g' t ↦ single (a ≫ g') (b * t)
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 s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
i : J.R
a :
  (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst i))) (↑x (WalkingMulticospan.left (J.fst i))) =
    ↑x (WalkingMulticospan.right i)
b :
  (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd i))) (↑x (WalkingMulticospan.left (J.snd i))) =
    ↑x (WalkingMulticospan.right i)
⊢ (hom (I.fst i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.fst i)) =
    (hom (I.snd i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.snd i))

Tactic:
← b

Goal state after:
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 : ↑(I.multicospan ⋙ forget C).sections
i : J.R
a :
  (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst i))) (↑x (WalkingMulticospan.left (J.fst i))) =
    (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd i))) (↑x (WalkingMulticospan.left (J.snd i)))
b :
  (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd i))) (↑x (WalkingMulticospan.left (J.snd i))) =
    ↑x (WalkingMulticospan.right i)
⊢ (hom (I.fst i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.fst i)) =
    (hom (I.snd i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.snd i))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MulticospanShape
⊢ ∀ {W X Y Z : WalkingMulticospan J} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rintro (_ | _) (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) (_ | _ | _)

Goal state after:
case left.left.left.left.id.id.id
J : MulticospanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.id (left a✝)) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.id (left a✝)))

case left.left.left.right.id.id.fst
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.fst a✝))).comp (Hom.id (left (J.fst a✝)))).comp (Hom.fst a✝) =
    (Hom.id (left (J.fst a✝))).comp ((Hom.id (left (J.fst a✝))).comp (Hom.fst a✝))

case left.left.left.right.id.id.snd
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.snd a✝))).comp (Hom.id (left (J.snd a✝)))).comp (Hom.snd a✝) =
    (Hom.id (left (J.snd a✝))).comp ((Hom.id (left (J.snd a✝))).comp (Hom.snd a✝))

case left.left.right.right.id.fst.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.fst a✝))).comp (Hom.fst a✝)).comp (Hom.id (right a✝)) =
    (Hom.id (left (J.fst a✝))).comp ((Hom.fst a✝).comp (Hom.id (right a✝)))

case left.left.right.right.id.snd.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (left (J.snd a✝))).comp (Hom.snd a✝)).comp (Hom.id (right a✝)) =
    (Hom.id (left (J.snd a✝))).comp ((Hom.snd a✝).comp (Hom.id (right a✝)))

case left.right.right.right.fst.id.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.fst a✝).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.fst a✝).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))

case left.right.right.right.snd.id.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.snd a✝).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.snd a✝).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))

case right.right.right.right.id.id.id
J : MulticospanShape
a✝ : J.R
⊢ ((Hom.id (right a✝)).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.id (right a✝)).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
⊢ ∀ {W X Y Z : WalkingMultispan J} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rintro (_ | _) (_ | _) (_ | _) (_ | _) (_ | _ | _) (_ | _ | _) (_ | _ | _)

Goal state after:
case left.left.left.left.id.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.id (left a✝)) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.id (left a✝)))

case left.left.left.right.id.id.fst
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.fst a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.fst a✝))

case left.left.left.right.id.id.snd
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.snd a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.snd a✝))

case left.left.right.right.id.fst.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.fst a✝)).comp (Hom.id (right (J.fst a✝))) =
    (Hom.id (left a✝)).comp ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝))))

case left.left.right.right.id.snd.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.snd a✝)).comp (Hom.id (right (J.snd a✝))) =
    (Hom.id (left a✝)).comp ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝))))

case left.right.right.right.fst.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝)))).comp (Hom.id (right (J.fst a✝))) =
    (Hom.fst a✝).comp ((Hom.id (right (J.fst a✝))).comp (Hom.id (right (J.fst a✝))))

case left.right.right.right.snd.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝)))).comp (Hom.id (right (J.snd a✝))) =
    (Hom.snd a✝).comp ((Hom.id (right (J.snd a✝))).comp (Hom.id (right (J.snd a✝))))

case right.right.right.right.id.id.id
J : MultispanShape
a✝ : J.R
⊢ ((Hom.id (right a✝)).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.id (right a✝)).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))
Module: Mathlib.Algebra.Homology.ShortComplex.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
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁

Tactic:
have := (forget₂ C Ab).preservesFiniteLimits_of_preservesHomology

Goal state after:
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
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
this : PreservesFiniteLimits (forget₂ C Ab)
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case neg
J : MultispanShape
a b : J.L
h : ¬a = b
⊢ Subsingleton (left a ⟶ left b)

Tactic:
· have : IsEmpty (left a ⟶ left b) := ⟨by rintro ⟨⟩; simp at h⟩
    infer_instance

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

Goal state before:
pp: case left.right.fst
J : MultispanShape
l : J.L
T₁ : Type := { u // J.fst l = J.fst l }
T₂ : Type := { u // J.snd l = J.fst l }
f : T₁ ⊕ T₂ → (left l ⟶ right (J.fst l)) :=
  Sum.elim
    (fun x ↦
      match x with
      | ⟨val, h⟩ =>
        (h ▸
            let T₁ := { u // J.fst l = J.fst l };
            let T₂ := { u // J.snd l = J.fst l };
            fun x ↦ Hom.fst l)
          x)
    fun x ↦
    match x with
    | ⟨val, h⟩ =>
      (h ▸
          let T₁ := { u // J.fst l = J.snd l };
          let T₂ := { u // J.snd l = J.snd l };
          fun x ↦ Hom.snd l)
        x
⊢ ∃ a, f a = Hom.fst l

Tactic:
exact ⟨Sum.inl ⟨⟨⟩, rfl⟩, rfl⟩

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
h : L ⊣ R
X : C
⊢ L.map (h.unit.app X) ≫ L.map (h.unit.app (R.obj (L.obj X))) =
    L.map (h.unit.app X) ≫ L.map (R.map (L.map (h.unit.app X)))

Tactic:
rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]

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

Goal state before:
pp: case zero.succ.succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
hk : 0 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨0 + 1, hk⟩
⊢ map F f ⟨0, hi⟩ ⟨0 + 1, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨0 + 1, hk⟩ hjk

Tactic:
simp [Fin.le_def] at hjk

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ e₀.hom ≫ G.map reflexion ≫ e₁.inv = F.map reflexion

Tactic:
← reassoc_of% h₃,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ≅ G.obj zero
e₁ : F.obj one ≅ G.obj one
h₁ : F.map left ≫ e₀.hom = e₁.hom ≫ G.map left
h₂ : F.map right ≫ e₀.hom = e₁.hom ≫ G.map right
h₃ : F.map reflexion ≫ e₁.hom = e₀.hom ≫ G.map reflexion
⊢ F.map reflexion ≫ e₁.hom ≫ e₁.inv = F.map reflexion
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
⊢ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N') = I • restrictScalars R N'

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (Submodule.smul_le.mpr fun r hr n hn ↦ ?_)

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
⊢ x ∈ I • restrictScalars R N'

case refine_2
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
r : R
hr : r ∈ I
n : N
hn : n ∈ restrictScalars R N'
⊢ r • n ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
⊢ ∀ (y : ↥(localized₀ p f M')), ∃ x, x.2 • y = (toLocalized₀ p f M') x.1

Tactic:
rintro ⟨y, x, hx, s, rfl⟩
    exact ⟨⟨⟨x, hx⟩, s⟩, by ext; simp⟩

Goal state after:
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
I : Ideal R
z : S
s : ↥M
x : R
hx : x ∈ I
h : z * (algebraMap R S) ↑(⟨x, hx⟩, s).2 = (algebraMap R S) ↑(⟨x, hx⟩, s).1
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) x s = z

Tactic:
rw [← IsLocalization.mk'_eq_mk', eq_comm, IsLocalization.eq_mk'_iff_mul_eq]

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
I : Ideal R
z : S
s : ↥M
x : R
hx : x ∈ I
h : z * (algebraMap R S) ↑(⟨x, hx⟩, s).2 = (algebraMap R S) ↑(⟨x, hx⟩, s).1
⊢ z * (algebraMap R S) ↑s = (algebraMap R S) x
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
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
b : ↥I
s : ↥M
h : (algebraMap R S) (↑s * a) = (algebraMap R S) ↑b
c : ↥M
hc : ↑c * (↑s * a) = ↑c * ↑b
this : a * ↑(c * s) ∈ I
⊢ a ∈ I

Tactic:
exact ((Ideal.isPrimary_iff.mp hI).2 this).resolve_right (Set.disjoint_left.mp key (c * s).2)

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ ((X ^ n).sum fun n r ↦ (monomial n) (a * (algebraMap R A) r)) = (monomial n) a

Tactic:
X_pow_eq_monomial,

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (((monomial n) 1).sum fun n r ↦ (monomial n) (a * (algebraMap R A) r)) = (monomial n) a
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 : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ ∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)

Tactic:
· rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient] at hI
    obtain ⟨n, hn⟩ := hI.3 hM
    obtain ⟨rn, rfl⟩ := Ideal.Quotient.mk_surjective n
    refine ⟨(Ideal.Quotient.mk J) (r * rn), ?_⟩
    -- The rest of the proof is essentially just algebraic manipulations to prove the equality
    replace hn := congr_arg (Ideal.quotientMap I (algebraMap R S) le_rfl) hn
    rw [map_one, map_mul] at hn
    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]
    simp only [mul_eq_mul_left_iff, map_mul]
    refine
      Or.inl
        (mul_left_cancel₀ (M₀ := S ⧸ I)
          (fun hn =>
            hM
              (Ideal.Quotient.eq_zero_iff_mem.2
                (Ideal.mem_comap.2 (Ideal.Quotient.eq_zero_iff_mem.1 hn))))
          (_root_.trans hn ?_))
    rw [← map_mul, ← mk'_eq_mul_mk'_one, mk'_self, map_one]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
a : ↥m ⊗[R] N
b : M ⊗[R] ↥n
f : ↥m ⊗[R] N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
⊢ (map m.mkQ n.mkQ) ((map m.subtype LinearMap.id) a) + (map m.mkQ n.mkQ) ((map LinearMap.id n.subtype) b) = 0

Tactic:
set g := (map m.mkQ n.mkQ) ∘ₗ (map LinearMap.id n.subtype)

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
a : ↥m ⊗[R] N
b : M ⊗[R] ↥n
f : ↥m ⊗[R] N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : M ⊗[R] ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
⊢ (map m.mkQ n.mkQ) ((map m.subtype LinearMap.id) a) + (map m.mkQ n.mkQ) ((map LinearMap.id n.subtype) b) = 0
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
⊢ (equivQuotMaximalIdeal p Rₚ).symm ((Ideal.Quotient.mk (maximalIdeal Rₚ)) (mk' Rₚ x s)) =
    (Ideal.Quotient.mk p) x * ((Ideal.Quotient.mk p) ↑s)⁻¹

Tactic:
have h₁ : Ideal.Quotient.mk p ↑s ≠ 0 := by
    simpa [ne_eq, Ideal.Quotient.eq_zero_iff_mem] using Ideal.mem_primeCompl_iff.mp s.prop
  have h₂ : equivQuotMaximalIdeal p Rₚ (Ideal.Quotient.mk p ↑s) ≠ 0 := by
    rwa [RingEquiv.map_ne_zero_iff]
  rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
    inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotMaximalIdeal_apply_mk, ← map_mul,
    mk'_spec, Ideal.Quotient.mk_algebraMap, equivQuotMaximalIdeal_apply_mk,
    Ideal.Quotient.mk_algebraMap]

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hT :
  ∀ (r : ↑s),
    ∃ Rᵣ Sᵣ x x_1 x_2 x_3,
      ∃ (_ : IsLocalization.Away (↑r) Rᵣ) (_ : IsLocalization.Away (f ↑r) Sᵣ),
        ∃ fᵣ, ∃ (_ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f), P fᵣ
r : ↑s
Rᵣ Sᵣ : Type u
w✝⁵ : CommRing Rᵣ
w✝⁴ : CommRing Sᵣ
w✝³ : Algebra R Rᵣ
w✝² : Algebra S Sᵣ
w✝¹ : IsLocalization.Away (↑r) Rᵣ
w✝ : IsLocalization.Away (f ↑r) Sᵣ
fᵣ : Rᵣ →+* Sᵣ
hfᵣ : fᵣ.comp (algebraMap R Rᵣ) = (algebraMap S Sᵣ).comp f
hf : P fᵣ
e₁ : Localization (Submonoid.powers ↑r) ≃+* Rᵣ := (Localization.algEquiv (Submonoid.powers ↑r) Rᵣ).toRingEquiv
e₂ : Sᵣ ≃+* Localization (Submonoid.powers (f ↑r)) :=
  (IsLocalization.algEquiv (Submonoid.powers (f ↑r)) (Localization (Submonoid.powers (f ↑r))) Sᵣ).symm.toRingEquiv
x : R
⊢ fᵣ ((algebraMap R Rᵣ) x) = (algebraMap S Sᵣ) (f x)

Tactic:
rw [← RingHom.comp_apply, hfᵣ, RingHom.comp_apply]

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

Goal state before:
pp: case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
⊢ t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1

Tactic:
IH,

Goal state after:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
⊢ t.toMatrix * 1 * t.inv.toMatrix = 1
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✝ : NonAssocSemiring R
A B : Matrix m n R
⊢ A = B ↔ ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace

Tactic:
by
  refine ⟨fun h x => h ▸ rfl, fun h => ?_⟩
  ext i j
  classical
  simpa [trace_single_mul] using h (single j i (1 : R))

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 α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : ((reindex e e) A).det = ∑ x, (reindex e e) A (e i) x * ((reindex e e) A).adjugate x (e i)
⊢ A.det = ∑ j, A i j * A.adjugate j i

Tactic:
det_reindex_self,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A.det = ∑ x, (reindex e e) A (e i) x * ((reindex e e) A).adjugate x (e i)
⊢ A.det = ∑ j, A i j * A.adjugate j i
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (A.map fun a ↦ includeLeft a).det ^ Fintype.card n * (B.map fun b ↦ includeRight b).det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]

Goal state after:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ includeLeft A.det ^ Fintype.card n * includeRight B.det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
⊢ (A ^ k).adjugate * A.adjugate = A.adjugate ^ (k + 1)

Tactic:
IH,

Goal state after:
case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
k : ℕ
IH : (A ^ k).adjugate = A.adjugate ^ k
⊢ A.adjugate ^ k * A.adjugate = A.adjugate ^ (k + 1)