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

Goal state before:
pp: case none
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
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ ∃ y_1, (hom (head f)) y_1 = (hom (colimit.ι (wideSpan B X f) none)) y

Tactic:
use y

Goal state after:
case h
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
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : ToType ((wideSpan B X f).obj none)
⊢ (hom (head f)) y = (hom (colimit.ι (wideSpan B X f) none)) y
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
⊢ ∀ {X Y : WalkingMulticospan J} (f : X ⟶ Y),
    F.map f ≫
        (match Y with
          | WalkingMulticospan.left i => left i
          | WalkingMulticospan.right i => right i).hom =
      (match X with
          | WalkingMulticospan.left i => left i
          | WalkingMulticospan.right i => right i).hom ≫
        G.map f

Tactic:
by
    rintro _ _ ⟨_⟩ <;> simp [wl, wr]

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

Goal state before:
pp: J : MultispanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ (right (J.fst i)).hom = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ (right (J.snd i)).hom = (left i).hom ≫ G.map (Hom.snd i)
⊢ ∀ {X Y : WalkingMultispan J} (f : X ⟶ Y),
    F.map f ≫
        (match Y with
          | WalkingMultispan.left i => left i
          | WalkingMultispan.right i => right i).hom =
      (match X with
          | WalkingMultispan.left i => left i
          | WalkingMultispan.right i => right i).hom ≫
        G.map f

Tactic:
by
    rintro _ _ ⟨_⟩ <;> simp [wl, wr]

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
a✝ : J.L
⊢ K.ι.app (WalkingMultispan.left a✝) ≫ f = K.ι.app (WalkingMultispan.left a✝) ≫ g

Tactic:
simp [h]

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
a✝ : J.R
⊢ K.ι.app (WalkingMultispan.right a✝) ≫ f = K.ι.app (WalkingMultispan.right a✝) ≫ g

Tactic:
simp [h]

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

Goal state before:
pp: case left
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
i : J.L
⊢ K.ι.app (WalkingMultispan.left i) ≫ e.hom = K'.ι.app (WalkingMultispan.left i)

Tactic:
simp [h]

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

Goal state before:
pp: case right
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 : J.R
⊢ K.ι.app (WalkingMultispan.right j) ≫ e.hom = K'.ι.app (WalkingMultispan.right j)

Tactic:
simp [h]

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
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝¹ : HasColimit (F ⋙ R)
this✝ : HasColimit F
this : CreatesColimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := comonadicCreatesColimits R
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Tactic:
let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F R

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 := empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝¹ : HasColimit (F ⋙ R)
this✝ : HasColimit F
this : CreatesColimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := comonadicCreatesColimits R
A : PreservesColimit F R := preservesColimit_of_createsColimit_and_hasColimit F R
⊢ R.obj (colimit.cocone F).1 ≅ c.pt
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| g • under A P

Tactic:
pointwise_smul_eq_comap,

Goal state after:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| comap (RingEquiv.symm ((MulSemiringAction.toRingAut G A) g)) (under A P)
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| under A (g • P)

Tactic:
pointwise_smul_eq_comap,

Goal state after:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| under A (comap (RingEquiv.symm ((MulSemiringAction.toRingAut G B) g)) P)
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 T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
left✝ : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n • ⊤ ≤ T
⊢ (S ⊓ T).IsPrimary

Tactic:
refine ⟨by grind, fun ⟨hS', hT'⟩ ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left✝¹ : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S
left✝ : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ n, r ^ n • ⊤ ≤ T
r✝ : R
x✝¹ : M
x✝ : r✝ • x✝¹ ∈ S ⊓ T
hS' : r✝ • x✝¹ ∈ ↑S
hT' : r✝ • x✝¹ ∈ ↑T
⊢ x✝¹ ∈ S ⊓ T ∨ ∃ n, r✝ ^ n • ⊤ ≤ S ⊓ T
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case ih
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

pp: case hxs
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ OrderDual.toDual J ∈ S

Tactic:
swap

Goal state after:
case hxs
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ OrderDual.toDual J ∈ S

case ih
R : Type u_1
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : J.IsPrime
e : I ≤ J
S : Set (Ideal R)ᵒᵈ := ⋯
⊢ ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
⊢ I = ⊤

Tactic:
by_contra hI

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : I.minimalPrimes = ∅
hI : ¬I = ⊤
⊢ False
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ p ∈ {p | I.IsMinimalPrime p}

pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ p ∈ {p | I.radical.IsMinimalPrime p}

Tactic:
· refine ⟨⟨a, a.radical_le_iff.1 ha⟩, ?_⟩
    simp only [and_imp] at *
    exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ p ∈ {p | I.radical.IsMinimalPrime p}
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
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 : ℕ
hI : I ^ n = ⊥
⊢ P I

Tactic:
induction n using Nat.strong_induction_on generalizing S with | _ n H

Goal state after:
case h
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 = ⊥
⊢ P I
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

pp: case h₂
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x

Tactic:
swap

Goal state after:
case h₂
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x

case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h₁
R : Type u_2
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x

Tactic:
introv e H

Goal state after:
case h₁
R : Type u_2
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit ((Ideal.Quotient.mk I) x)
⊢ IsUnit x
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 ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ (a * (algebraMap R A) a_1) ⊗ₜ[R] 1 * 1 ⊗ₜ[R] (X ^ n)) = a ⊗ₜ[R] p

Tactic:
Algebra.TensorProduct.tmul_mul_tmul,

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 ⊗[R] R[X]
a : A
p : R[X]
⊢ (p.sum fun n a_1 ↦ (a * (algebraMap R A) a_1 * 1) ⊗ₜ[R] (1 * X ^ n)) = a ⊗ₜ[R] p
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
x : A ⊗[R] R[X]
⊢ invFun R A ((toFunAlgHom R A) x) = x

Tactic:
by
  refine TensorProduct.induction_on x ?_ ?_ ?_
  · simp [invFun]
  · intro a p
    dsimp only [invFun]
    rw [toFunAlgHom_apply_tmul, eval₂_sum]
    simp_rw [eval₂_monomial, AlgHom.coe_toRingHom, Algebra.TensorProduct.tmul_pow, one_pow,
      Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one,
      one_mul, ← Algebra.commutes, ← Algebra.smul_def, smul_tmul, sum_def, ← tmul_sum]
    conv_rhs => rw [← sum_C_mul_X_pow_eq p]
    simp only [Algebra.smul_def]
    rfl
  · intro p q hp hq
    simp only [map_add, invFun_add, hp, hq]

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
⊢ (toFunAlgHom R A) (a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] (X ^ n)) = (monomial n) a

Tactic:
Algebra.TensorProduct.tmul_mul_tmul,

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
⊢ (toFunAlgHom R A) ((a * 1) ⊗ₜ[R] (1 * X ^ n)) = (monomial n) a
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case right
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
⊢ Function.Surjective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)

Tactic:
· suffices ∀ y, ∀ z ∉ P, ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y) by
      simpa [(IsLocalization.mk'_surjective p.primeCompl).exists,
        (IsLocalization.mk'_surjective P.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, Function.Surjective] using this
    intro y z hzP
    obtain ⟨a, ⟨haP, has⟩, ha⟩ := H.ge (Set.mem_univ y)
    obtain ⟨b, ⟨hbP, hbs⟩, hb⟩ := H.ge (Set.mem_univ z)
    exact ⟨_, mul_mem ha hbs, _, P.primeCompl.mul_mem (mul_mem hbP hzP) haP, mul_mem hb has, 1,
      P.primeCompl.one_mem, by ring⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
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ₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
h : x✝ ∈ p ^ n
⊢ 1 * x✝ ∈ p ^ n

Tactic:
simp [h]

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
H : LocalizationPreserves P
⊢ LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by
  intro R S _ _ f r R' S' _ _ _ _ _ _ hf
  have : IsLocalization ((Submonoid.powers r).map f) S' := by rw [Submonoid.map_powers]; assumption
  exact H f (Submonoid.powers r) R' S' hf

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
t : R
n : ℤ
⊢ (C t).coeff n = if n = 0 then t else 0

Tactic:
simp [← single_eq_C]

Goal state after:
R : Type u_1
inst✝ : Semiring R
t : R
n : ℤ
⊢ (Finsupp.single 0 t) n = if n = 0 then t else 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', toLaurent f' = C a * T n * T ↑n_1

Tactic:
· rcases n with n | n
    · exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
    · refine ⟨n + 1, Polynomial.C a, ?_⟩
      simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.natCast_succ, mul_T_assoc,
        neg_add_cancel, T_zero, mul_one]

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 α
b : n → α
⊢ b = ∑ i, b i • Pi.single i 1

Tactic:
refine (pi_eq_sum_univ b).trans ?_

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
⊢ (∑ i, b i • fun j ↦ if i = j then 1 else 0) = ∑ i, b i • Pi.single i 1
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case mk
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
k n : ℕ
hn : n < r
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
val✝ : ℕ
isLt✝ : val✝ < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl ⟨val✝, isLt✝⟩) (inr ()) =
    if n + 1 ≤ ↑⟨val✝, isLt✝⟩ then 0 else M (inl ⟨val✝, isLt✝⟩) (inr ())
h : n = val✝
⊢ n = ↑⟨val✝, isLt✝⟩

Tactic:
simp [h]

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

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsLeftRegular A

Tactic:
intro B

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B : Matrix n n α
⊢ ∀ ⦃a₂ : Matrix n n α⦄, (fun x ↦ A * x) B = (fun x ↦ A * x) a₂ → B = a₂
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ ∀ (x : β), (f 0) x = 0

Tactic:
intro; exact LinearMap.map_zero₂ _ _

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

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
⊢ IsRightRegular A

Tactic:
intro B

Goal state after:
case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B : Matrix n n α
⊢ ∀ ⦃a₂ : Matrix n n α⦄, (fun x ↦ x * A) B = (fun x ↦ x * A) a₂ → B = a₂
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det =
    (blockDiagonal fun x ↦ A.map fun a ↦ (f a) 1).det * (blockDiagonal fun x ↦ B.map fun b ↦ (f 1) b).det

Tactic:
by
      rw [det_mul, ← diagonal_one, ← diagonal_one, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_right _ fun _ => _, kroneckerMapBilinear_apply_apply,
        kroneckerMap_diagonal_left _ fun _ => _, det_reindex_self]
      · intro; exact LinearMap.map_zero₂ _ _
      · intro; exact map_zero _

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
inst✝¹ : Invertible (⅟C + V * ⅟A * U)
inst✝ : Invertible (A + U * C * V)
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
let := invertibleAddMulMul A U C V

Goal state after:
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
inst✝¹ : Invertible (⅟C + V * ⅟A * U)
inst✝ : Invertible (A + U * C * V)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul U C V
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A
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
inst✝¹ : Invertible (⅟C + V * ⅟A * U)
inst✝ : Invertible (A + U * C * V)
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

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

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

Goal state before:
pp: α : Type u_3
m : Type u_10
n : Type u_11
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn ↦ ↑a * ↑b) = ↑(a * b)

Tactic:
simp_rw [← Nat.cast_mul]; rfl

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 B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M := by
    intro
    rw [RingHom.map_adjugate, f'_inv]

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
⊢ (A * B).adjugate = B.adjugate * A.adjugate
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 : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) • A

Tactic:
by
    rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,
      ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),
      AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_mul _)]

Goal state after: