mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ ∀ (X : Fin (n + 1 + 1)), (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app X = eqToHom ⋯

Tactic:
rintro ⟨_ | _, hi⟩

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
hi : 0 < n + 1 + 1
⊢ (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app ⟨0, hi⟩ = eqToHom ⋯

case succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
⊢ (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app ⟨n✝ + 1, hi⟩ = eqToHom ⋯
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✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (monadicAdjunction R).toMonad.Algebra := Monad.comparison (monadicAdjunction R)
B : (monadicAdjunction R).toMonad.Algebra ⥤ C := (monadicAdjunction R).toMonad.forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ (monadicAdjunction R).toMonad.forget ≅ K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R)) (monadicAdjunction R).toMonad.forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
⊢ CreatesColimit K R

Tactic:
letI : PreservesColimit ((K ⋙ A) ⋙ Monad.forget
    (Adjunction.toMonad (monadicAdjunction R)))
      (Adjunction.toMonad (monadicAdjunction R)).toFunctor := by
    dsimp
    exact preservesColimit_of_iso_diagram _ i.symm

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✝² : MonadicRightAdjoint R
inst✝¹ : PreservesColimit (K ⋙ R) (monadicLeftAdjoint R ⋙ R)
inst✝ : PreservesColimit ((K ⋙ R) ⋙ monadicLeftAdjoint R ⋙ R) (monadicLeftAdjoint R ⋙ R)
A : D ⥤ (monadicAdjunction R).toMonad.Algebra := Monad.comparison (monadicAdjunction R)
B : (monadicAdjunction R).toMonad.Algebra ⥤ C := (monadicAdjunction R).toMonad.forget
i : (K ⋙ Monad.comparison (monadicAdjunction R)) ⋙ (monadicAdjunction R).toMonad.forget ≅ K ⋙ R :=
  K.associator (Monad.comparison (monadicAdjunction R)) (monadicAdjunction R).toMonad.forget ≪≫
    K.isoWhiskerLeft (Monad.comparisonForget (monadicAdjunction R))
this : PreservesColimit ((K ⋙ A) ⋙ (monadicAdjunction R).toMonad.forget) (monadicAdjunction R).toMonad.toFunctor :=
  monadicCreatesColimitOfPreservesColimit._proof_1 R K
⊢ CreatesColimit K R
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
t : IsColimit c := isColimitOfPreserves (monadicLeftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ HasColimit F

Tactic:
apply HasColimit.mk ⟨_, (IsColimit.precomposeInvEquiv _ _).symm t⟩

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) := ⋯
this : PreservesColimitsOfShape J (monadicLeftAdjoint R) := ⋯
t : IsColimit c := ⋯
⊢ (F ⋙ R) ⋙ monadicLeftAdjoint R ≅ F
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
p : Ideal A
inst✝ : P.LiesOver p
⊢ P = ⊤ ↔ p = ⊤

Tactic:
by
  rw [P.over_def p]
  exact comap_eq_top_iff.symm

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
obj : Fin (n + 1) → C
mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ
⊢ ∃ F e, ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi ≫ (e ⟨i + 1, ⋯⟩).hom

Tactic:
induction n with
  | zero => exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
  | succ n hn =>
    obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
    refine ⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i => match i with
      | 0 => Iso.refl _
      | ⟨i + 1, hi⟩ => e _, fun i hi => ?_⟩
    obtain _ | i := i
    · simp
    · exact h i (by valid)

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

Goal state before:
pp: case refine_1
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
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ (k * s) • j ∈ M''

Tactic:
exact M''.smul_of_tower_mem (k * s) hj

Goal state after:
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N N' : Submodule R M
r : R
⊢ r ∈ N.colon ↑N' ↔ r • N' ≤ N

Tactic:
aesop (add simp SetLike.coe_subset_coe)

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
e : I.minimalPrimes = ∅
h : ¬I = ⊤
M : Ideal R
hM : M.IsMaximal
hM' : I ≤ M
p : Ideal R
hp : p ∈ ∅ ∧ p ≤ M
⊢ False

Tactic:
apply Set.notMem_empty _ hp.1

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
⊢ I ⊔ J ≤ p

Tactic:
sup_le_iff

Goal state after:
case refine_1
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
⊢ I ≤ p ∧ J ≤ p
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
q : Ideal R
x✝ : (fun q ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left✝ : q.IsPrime
hq : I ⊔ J ≤ q
⊢ p ≤ q

Tactic:
sup_le_iff

Goal state after:
case refine_2
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
q : Ideal R
x✝ : (fun q ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left✝ : q.IsPrime
hq : I ≤ q ∧ J ≤ q
⊢ p ≤ q
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
hle : ∃ x ∈ ↑I, x ∈ ↑M
⊢ Ideal.map (algebraMap R S) I = ⊤

Tactic:
obtain ⟨y, hy, hny⟩ := hle

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ Ideal.map (algebraMap R S) I = ⊤
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
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ IsLocalization (Submonoid.map f (algebraMapSubmonoid A M)) Bₚ

Tactic:
algebraMapSubmonoid_map_eq M f

Goal state after:
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
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ IsLocalization (algebraMapSubmonoid B M) Bₚ
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
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

Tactic:
have eq : LinearMap.coprod f g = 0 := by
        ext x y
        · simp [f, Submodule.Quotient.mk_eq_zero _ |>.2 x.2]
        · simp [g, Submodule.Quotient.mk_eq_zero _ |>.2 y.2]

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
eq : f.coprod g = 0
⊢ (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_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)

Tactic:
by
  convert! congr_arg (Ideal.map _) AtPrime.under_maximalIdeal.symm
  rw [map_under I.primeCompl]

Goal state after:
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
A : Type u_4
B : Type u_5
C : Type u_6
inst✝²¹ : CommSemiring A
inst✝²⁰ : CommSemiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : IsScalarTower R A B
inst✝¹⁵ : CommSemiring C
inst✝¹⁴ : Algebra A C
inst✝¹³ : Algebra B C
inst✝¹² : IsScalarTower A B C
p : Ideal A
inst✝¹¹ : p.IsPrime
P : Ideal B
inst✝¹⁰ : P.IsPrime
inst✝⁹ : P.LiesOver p
Q : Ideal C
inst✝⁸ : Q.IsPrime
inst✝⁷ : Q.LiesOver P
inst✝⁶ : Q.LiesOver p
inst✝⁵ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝⁴ : IsLiesOverAlgebra p P
inst✝³ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝² : IsLiesOverAlgebra P Q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime Q)
inst✝ : IsLiesOverAlgebra p Q
⊢ algebraMap (Localization.AtPrime p) (Localization.AtPrime Q) =
    (algebraMap (Localization.AtPrime P) (Localization.AtPrime Q)).comp
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime P))

Tactic:
by
    simp [IsLiesOverAlgebra.algebraMap_eq, ← localRingHom_comp, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ x = mk' S y z

Tactic:
rw [hz, Algebra.linearMap_apply, smul_eq_mul, mul_comm, mul_mk'_eq_mk'_of_mul, mul_one]

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

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)
⊢ P e✝

Tactic:
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Goal state after:
case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)
s' : Finset a✝
h₁ : ↑s' ⊆ s
h₂ : Ideal.span ↑s' = ⊤
⊢ P e✝
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
⊢ P e✝

Tactic:
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Goal state after:
case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
s' : Finset b✝
h₁ : ↑s' ⊆ s
h₂ : Ideal.span ↑s' = ⊤
⊢ P e✝
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ Matrix.fromBlocks A Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D

Tactic:
hCB,

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ Matrix.fromBlocks A B Bᵀ Dᵀ = Matrix.fromBlocks A B C D
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ f.degree = ⊥

Tactic:
rw [h, degree_zero]

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
h : i ≠ j
c : R
⊢ (transvection i j c).det = 1

Tactic:
rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]

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

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

Tactic:
← reverse_inv_prod_mul_prod L.reverse,

Goal state after:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L).prod * (List.map toMatrix L.reverse).prod =
    (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse.reverse).prod * (List.map toMatrix L.reverse).prod
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ x, (-1) ^ (↑j + ↑x) * Pi.single i 1 x * ((A.updateRow j (Pi.single i 1)).submatrix j.succAbove x.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
submatrix_updateRow_succAbove

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ x, (-1) ^ (↑j + ↑x) * Pi.single i 1 x * (A.submatrix j.succAbove x.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ ↑Finset.univ.card = ↑(Fintype.card n)

Tactic:
Finset.card_univ

Goal state after:
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 val✝ : ℕ
isLt✝ : val✝ < r
hn : ↑⟨val✝, isLt✝⟩ < r
IH :
  ((List.drop (↑⟨val✝, isLt✝⟩ + 1) (listTransvecCol M)).prod * M) (inl ⟨val✝, isLt✝⟩) (inr ()) =
    if ↑⟨val✝, isLt✝⟩ + 1 ≤ ↑⟨val✝, isLt✝⟩ then 0 else M (inl ⟨val✝, isLt✝⟩) (inr ())
hn' : ↑⟨val✝, isLt✝⟩ < (listTransvecCol M).length
n' : Fin r := ⟨↑⟨val✝, isLt✝⟩, hn⟩
A : (listTransvecCol M)[↑⟨val✝, isLt✝⟩] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = ⟨val✝, isLt✝⟩
⊢ False

Tactic:
simp [n'] at h

Goal state after:
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 β
⊢ (A.map fun a ↦ (f a) 1).det ^ Finset.univ.card * (B.map fun b ↦ (f 1) b).det ^ Finset.univ.card =
    (A.map fun a ↦ (f a) 1).det ^ Fintype.card n * (B.map fun b ↦ (f 1) b).det ^ Fintype.card m

Tactic:
Finset.card_univ

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

Goal state before:
pp: case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
simp only [List.take_add_one, A, ← Matrix.mul_assoc, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]

Goal state after:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
⊢ (M * (List.take n (listTransvecRow M)).prod *
        transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
      (inr ()) (inl i) =
    if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
hM : M.BlockTriangular b
this : ∀ (hs : Finset α), image b univ = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
by
    exact this _ rfl

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ (a₁✝ * a₂✝) • (b₁✝ * b₂✝).map ⇑(algebraMap R A) = a₁✝ • b₁✝.map ⇑(algebraMap R A) * a₂✝ • b₂✝.map ⇑(algebraMap R A)

Tactic:
Matrix.map_mul

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ (a₁✝ * a₂✝) • (b₁✝.map ⇑(algebraMap R A) * b₂✝.map ⇑(algebraMap R A)) =
    a₁✝ • b₁✝.map ⇑(algebraMap R A) * a₂✝ • b₂✝.map ⇑(algebraMap R A)
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ (toFunAlgHom n R A) (invFun n R A M) = M

Tactic:
by
  simp only [invFun, map_sum, toFunAlgHom_apply]
  convert! Finset.sum_product (β := Matrix n n A) ..
  conv_lhs => rw [matrix_eq_sum_single M]
  simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ IsNilpotent (C r)

Tactic:
refine ⟨m, ?_⟩

Goal state after:
R : Type u_1
r : R
inst✝ : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ C r ^ m = 0
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_2.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
⊢ IsNilpotent ((p + C r).coeff 0)

pp: case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent ((p + C r).coeff (i + 1))

Tactic:
· simpa [hp₀] using hr

Goal state after:
case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent ((p + C r).coeff (i + 1))