mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.right.right.snd.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.L
⊢ (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝),
      WalkingMultispan.Hom.snd a✝ ≫ WalkingMultispan.Hom.id (WalkingMultispan.right (J.snd a✝)) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.left a✝, WalkingMultispan.right (J.snd a✝), WalkingMultispan.Hom.snd a✝ with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right (J.snd a✝), WalkingMultispan.right (J.snd a✝),
        WalkingMultispan.Hom.id (WalkingMultispan.right (J.snd a✝)) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

Tactic:
cat_disch

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

Goal state before:
pp: case right.right.right.id.id
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
a✝ : J.R
⊢ (match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
      WalkingMultispan.Hom.id (WalkingMultispan.right a✝) ≫ WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
    | x, .(x), WalkingMultispan.Hom.id .(x) =>
      𝟙
        (match x with
        | WalkingMultispan.left a => I.left a
        | WalkingMultispan.right b => I.right b)
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
    | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) =
    (match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
        WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b) ≫
      match WalkingMultispan.right a✝, WalkingMultispan.right a✝,
        WalkingMultispan.Hom.id (WalkingMultispan.right a✝) with
      | x, .(x), WalkingMultispan.Hom.id .(x) =>
        𝟙
          (match x with
          | WalkingMultispan.left a => I.left a
          | WalkingMultispan.right b => I.right b)
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.fst b)), WalkingMultispan.Hom.fst b => I.fst b
      | .(WalkingMultispan.left b), .(WalkingMultispan.right (J.snd b)), WalkingMultispan.Hom.snd b => I.snd b

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀' X₀ X₁ : C
h : X₀' = X₀
f : X₀ ⟶ X₁
⊢ mk₁ (eqToHom h ≫ f) = mk₁ f

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ X₁' : C
f : X₀ ⟶ X₁
h : X₁ = X₁'
⊢ mk₁ (f ≫ eqToHom h) = mk₁ f

Tactic:
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 : 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:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K✝ : Multicofork I
c : Cofan I.left
hc : IsColimit c
d : Cofan I.right
hd : IsColimit d
K K' : Multicofork I
e : K.pt ≅ K'.pt
h : ∀ (i : J.R), K.π i ≫ e.hom = K'.π i
⊢ ∀ (j : WalkingMultispan J), K.ι.app j ≫ e.hom = K'.ι.app j

Tactic:
rintro (i | j) <;> simp [h]

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:
cat_disch

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
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
c : Cocone (D ⋙ T.forget)
t : IsColimit c
A B : J
f : A ⟶ B
⊢ D.map f ≫ { f := c.ι.app B, h := ⋯ } = { f := c.ι.app A, h := ⋯ } ≫ ((const J).obj (coconePoint c t)).map f

Tactic:
ext1
                simpa using (c.w f)

Goal state after:
Module: Mathlib.RingTheory.Flat.CategoryTheory

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ (C.map (tensorLeft M)).Exact

Tactic:
rw [moduleCat_exact_iff_function_exact] at hC ⊢
  exact lTensor_exact M hC

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
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ monadicLeftAdjoint R) := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (monadicLeftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
⊢ HasColimit F

Tactic:
let t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit _)

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
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ monadicLeftAdjoint R) := (monadicLeftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (monadicLeftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ HasColimit F
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocone.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
        (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).π =
    G.ι.app zero

Tactic:
Cofork.π

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ ((Cocone.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
            (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).ι.app
      WalkingParallelPair.one =
    G.ι.app zero
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ (I ≠ ⊤ ∧ ∀ (b a : R), a • b ∈ I → b ∈ I ∨ ∃ n, a ^ n • ⊤ ≤ I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
simp only [mul_comm, mem_radical_iff,
    ← Submodule.ideal_span_singleton_smul, smul_eq_mul, mul_top, span_singleton_le_iff_mem]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit ((Ideal.Quotient.mk I) x) ↔ IsUnit x

Tactic:
refine ⟨?_, fun h => h.map <| Ideal.Quotient.mk I⟩

Goal state after:
R : Type u_2
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit ((Ideal.Quotient.mk I) x) → IsUnit 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 J : Ideal R
⊢ Ideal.map (algebraMap R S) (I ⊓ J) = Ideal.map (algebraMap R S) I ⊓ Ideal.map (algebraMap R S) J

Tactic:
by
  refine le_antisymm (Ideal.map_inf_le (algebraMap R S)) fun x hx ↦ ?_
  simp only [Ideal.mem_inf, IsLocalization.mem_map_algebraMap_iff M, Prod.exists] at hx ⊢
  obtain ⟨⟨⟨i, hi⟩, mi, hi'⟩, ⟨j, hj⟩, mj, hj'⟩ := hx
  simp only [← IsLocalization.eq_mk'_iff_mul_eq] at hi' hj'
  obtain ⟨m, hm⟩ := IsLocalization.eq.mp (hi'.symm.trans hj')
  rw [← mul_assoc, ← mul_assoc, mul_comm, ← mul_comm (j : R)] at hm
  refine ⟨⟨i * (m * mj : M), I.mul_mem_right _ hi, hm ▸ J.mul_mem_right _ hj⟩, mi * (m * mj), ?_⟩
  rwa [← IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, IsLocalization.mk'_cancel]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ((IsLocalizedModule.map p f f') g).ker = localized₀ p f g.ker

Tactic:
by
  ext x
  simp only [Submodule.mem_localized₀, mem_ker]
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨⟨a, b⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x
    simp only [Function.uncurry_apply_pair, map_mk', mk'_eq_zero, eq_zero_iff p f'] at h
    obtain ⟨c, hc⟩ := h
    refine ⟨c • a, by simpa, c * b, by simp⟩
  · rintro ⟨m, hm, a, ha, rfl⟩
    simp [IsLocalizedModule.map_mk', hm]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ((IsLocalizedModule.map p f f') g).range = localized₀ p f' g.range

Tactic:
ext; simp [mem_localized₀, mem_range, (mk'_surjective p f).exists]

Goal state after:
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
hy : M ≤ Submonoid.comap g T
x y : ↥(ker g)
⊢ ⟨(algebraMap R S) ↑(x + y), ⋯⟩ = ⟨(algebraMap R S) ↑x, ⋯⟩ + ⟨(algebraMap R S) ↑y, ⋯⟩

Tactic:
by
    simp only [Submodule.coe_add, map_add, AddMemClass.mk_add_mk]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : CommSemiring Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)
⊢ ((map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ)) (Algebra.linearMap R S)) 1 = 1

Tactic:
show 1 = Algebra.linearMap R Rₚ 1 by simp,

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : CommSemiring Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)
⊢ ((map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ)) (Algebra.linearMap R S))
      ((Algebra.linearMap R Rₚ) 1) =
    1
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
⊢ EssFiniteType R S ↔ ∃ S₀ M, FiniteType R ↥S₀ ∧ IsLocalization M S

Tactic:
refine ⟨fun h ↦ ⟨subalgebra R S, submonoid R S, inferInstance, inferInstance⟩, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∃ S₀ M, FiniteType R ↥S₀ ∧ IsLocalization M S) → EssFiniteType R S
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 : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
H :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R),
    Ideal.span s = ⊤ → (∀ r ∈ s, P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) → P (algebraMap R S)
⊢ OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
introv R hs hf
  algebraize [f]
  let _ := fun r : R => (Localization.awayMap (algebraMap R S) r).toAlgebra
  refine H s hs (fun r hr ↦ ?_)
  have : algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S) =
      ((IsLocalization.Away.tensorRightEquiv S r (Localization.Away r)).symm : _ →+* _).comp
        (algebraMap (Localization.Away r) (Localization.Away (algebraMap R S r))) := by
    apply IsLocalization.ringHom_ext (Submonoid.powers r)
    ext
    simp [RingHom.algebraMap_toAlgebra, Localization.awayMap, IsLocalization.Away.map,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, RingHom.algebraMap_toAlgebra]
  rw [this]
  exact hP.1 _ _ (hf ⟨r, hr⟩)

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

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
this : x + γ • x ∈ pS
⊢ (algebraMap R S) γ ∈ pS

Tactic:
exact Ideal.mem_map_of_mem _ hγ

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

Goal state before:
pp: α : Type u_1
n : Type u_3
A : Matrix n n α
⊢ Aᵀ.IsSymm ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.transpose)⟩
  rw [← A.transpose_transpose]
  exact h.transpose

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : InvolutiveNeg α
A : Matrix n n α
h : (-A).IsSymm
⊢ (- -A).IsSymm

Tactic:
exact h.neg

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

Goal state before:
pp: case h.refine_1
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✝
p✝ : Ideal R✝
inst✝²³ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝²² : CommSemiring Rₚ✝
inst✝²¹ : Algebra R✝ Rₚ✝
inst✝²⁰ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁹ : IsLocalRing Rₚ✝
Sₚ✝ : Type u_5
inst✝¹⁸ : CommSemiring Sₚ✝
inst✝¹⁷ : Algebra S✝ Sₚ✝
inst✝¹⁶ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ✝
inst✝¹⁵ : Algebra Rₚ✝ Sₚ✝
P : Ideal S✝
S : Type u_6
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ₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : S
s : ↥(algebraMapSubmonoid S p.primeCompl)
α : R
hα : α ∉ p
e : (algebraMap R S) α = ↑s
β γ : R
hγ : γ ∈ p
hβ : α * β = 1 + γ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact Ideal.mem_map_of_mem _ hγ

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

Goal state before:
pp: case pos
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
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1

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
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
· -- Everything except `(i, j)` (= `(σ j, j)`) is given by A, and the rest is a single `1`.
    congr
    ext j'
    subst h
    have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
    rw [updateRow_apply, updateCol_apply]
    simp_rw [this]
    rw [← dite_eq_ite, ← dite_eq_ite]
    congr 1 with rfl
    rw [Pi.single_eq_same, Pi.single_eq_same]

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
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝² : NoZeroDivisors R
h✝ : Nontrivial R
this✝¹ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this✝ : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
this : IsBaseChange FT (↑R g ∘ₗ g✝)
⊢ Cardinal.lift.{uP, max uM uP uT} (Cardinal.lift.{uM, max uP uT} (Module.rank FT (FT ⊗[T] P))) =
    Cardinal.lift.{max uP uT, uM} (Module.rank R M)

Tactic:
lift_rank_eq_of_le_nonZeroDivisors FR (LocalizedModule.mkLinearMap R⁰ M) le_rfl
      (map_le_nonZeroDivisors_of_injective _ inj le_rfl) this,

Goal state after:
case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝² : NoZeroDivisors R
h✝ : Nontrivial R
this✝¹ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this✝ : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
this : IsBaseChange FT (↑R g ∘ₗ g✝)
⊢ Cardinal.lift.{uP, max uM uP uT} (Cardinal.lift.{max uP uT, uM} (Module.rank R M)) =
    Cardinal.lift.{max uP uT, uM} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A.adjugateᴴ = Aᴴ.adjugate

Tactic:
dsimp only [conjTranspose]
  have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ
  rw [A.adjugate_transpose, this]

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 α
k : ℕ
⊢ (A ^ k).adjugate = A.adjugate ^ k

Tactic:
induction k with
  | zero => simp
  | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]

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 α
⊢ A * (A.adjugate * A.adjugate.adjugate) = A * A.det ^ (Fintype.card n - 1) • 1

Tactic:
rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]

Goal state after:
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✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible (C + C * V * ⅟A * U * C)
inst✝ : Invertible (A + U * C * V)
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A

Tactic:
by
  let := invertibleAddMulMul' A U C V
  convert! (rfl : ⅟(A + U * C * V) = _)

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

Goal state before:
pp: case zero
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = 0
⊢ A.adjugate.adjugate = A.det ^ (0 - 2) • A

pp: case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = n' + 1
⊢ A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A

Tactic:
· subsingleton [Fintype.card_eq_zero_iff.mp h_card]

Goal state after:
case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = n' + 1
⊢ A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ M.det =
    (fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
        (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j)).det

Tactic:
rw [← Matrix.det_reindex_self (Equiv.sumCompl p).symm M]
  rw [det_apply', det_apply']
  congr; ext σ; congr; ext x
  generalize hy : σ x = y
  cases x <;> cases y <;>
    simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr,
      Equiv.sumCompl_apply_inl, fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁,
      fromBlocks_apply₂₂, Matrix.submatrix_apply]

Goal state after: