mathlib-initiative/mathlib-tactics huggingface dataset:
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
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) ≫ s.pt.a =
    T.map (c.ι.app j) ≫ lambda c t ≫ t.desc (T.forget.mapCocone s)

Tactic:
← Category.assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) ≫ s.pt.a =
    (T.map (c.ι.app j) ≫ lambda c t) ≫ t.desc (T.forget.mapCocone s)
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
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ (T.mapCocone c).ι.app j ≫ T.map (t.desc (T.forget.mapCocone s)) ≫ s.pt.a =
    (T.mapCocone c).ι.app j ≫ (liftedCocone c t).pt.a ≫ t.desc (T.forget.mapCocone s)

Tactic:
by
          dsimp
          rw [← Functor.map_comp_assoc, ← Category.assoc, t.fac, commuting, Category.assoc, t.fac]
          apply Algebra.Hom.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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ R.obj (limit.cone F).1 ≅ c.pt

Tactic:
letI := monadicCreatesLimits.{v, v} R

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
⊢ R.obj (limit.cone F).1 ≅ c.pt
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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ (D.obj j).a ≫ T.ε.app (D.obj j).A ≫ c.ι.app j = c.ι.app j

Tactic:
← Category.assoc,

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ ((D.obj j).a ≫ T.ε.app (D.obj j).A) ≫ c.ι.app j = c.ι.app j
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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ (D.obj j).a ≫ T.δ.app (D.obj j).A ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))

Tactic:
← Category.assoc,

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ ((D.obj j).a ≫ T.δ.app (D.obj j).A) ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))
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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ c.ι.app j ≫ t.desc (newCocone D c) ≫ T.map (t.desc (T.forget.mapCocone s)) =
    c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a

Tactic:
← Category.assoc,

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (c.ι.app j ≫ t.desc (newCocone D c)) ≫ T.map (t.desc (T.forget.mapCocone s)) =
    c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a
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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (c.ι.app j ≫ t.desc (newCocone D c)) ≫ T.map (t.desc (T.forget.mapCocone s)) =
    c.ι.app j ≫ t.desc (T.forget.mapCocone s) ≫ s.pt.a

Tactic:
← Category.assoc,

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
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (c.ι.app j ≫ t.desc (newCocone D c)) ≫ T.map (t.desc (T.forget.mapCocone s)) =
    (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) ≫ s.pt.a
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: case mk
R✝ : Type u_1
inst✝¹⁶ : CommRing R✝
R : Type u_2
inst✝¹⁵ : CommSemiring R
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹⁴ : CommRing A
inst✝¹³ : CommRing B
inst✝¹² : CommRing C
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Algebra A C
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : IsScalarTower R A B
P : Ideal B
Q : Ideal C
p : Ideal A
inst✝⁶ : Q.LiesOver p
inst✝⁵ : P.LiesOver p
G : Type u_6
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : SMulCommClass G A B
E : Type u_7
inst✝¹ : EquivLike E B C
inst✝ : AlgEquivClass E A B C
σ : E
h : Q = map σ P
r✝ : A ⧸ p
x : A
⊢ (P.quotientEquiv Q (↑σ) h).toFun ((algebraMap (A ⧸ p) (B ⧸ P)) (Quot.mk (⇑(quotientRel p)) x)) =
    (algebraMap (A ⧸ p) (C ⧸ Q)) (Quot.mk (⇑(quotientRel p)) x)

Tactic:
exact congrArg (Ideal.Quotient.mk Q) (AlgHomClass.commutes σ x)

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
x : ι
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
simp [hx]

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

Goal state before:
pp: R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ ∀ (x : S), IsNilpotent x → x = 0

Tactic:
hf.forall,

Goal state after:
R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ ∀ (x : R), IsNilpotent (f x) → f x = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case neg.succ.succ.a
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
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ map (Quotient.mk (I ^ 2)) I ^ 2 = ⊥

Tactic:
← Ideal.map_pow,

Goal state after:
case neg.succ.succ.a
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
S : Type u_1
inst✝ : CommRing S
I : Ideal S
hI' : ¬I = ⊥
n : ℕ
H : ∀ m < n + 1 + 1, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
hI : I ^ (n + 1 + 1) = ⊥
⊢ map (Quotient.mk (I ^ 2)) (I ^ 2) = ⊥
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: 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)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
this : x * y - 1 ∈ I
⊢ (x * y - 1) ^ 2 = 0

Tactic:
rw [← Ideal.mem_bot, ← e]

Goal state after:
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)
y : S
hy : (Ideal.Quotient.mk I) y = ↑H.unit⁻¹
this : x * y - 1 ∈ I
⊢ (x * y - 1) ^ 2 ∈ I ^ 2
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 : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ (Ideal.Quotient.mk I) ((algebraMap R S) rn) = (Ideal.Quotient.mk I) (mk' S 1 ⟨m, hm⟩) ∨
    (Ideal.Quotient.mk I) ((algebraMap R S) r) = 0

Tactic:
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 ?_))

Goal state after:
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 : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ 1 = (Ideal.Quotient.mk I) ((algebraMap R S) m) * (Ideal.Quotient.mk I) (mk' S 1 ⟨m, hm⟩)
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
ι : Type u_9
v : ι → M
H : ∀ (P : Ideal R) [inst : P.IsMaximal], LinearIndependent (Rₚ P) (⇑(f P) ∘ v)
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Injective
    ⇑((IsLocalizedModule.map P.primeCompl (Finsupp.mapRange.linearMap (Algebra.linearMap R (Rₚ P))) (f P))
        (Finsupp.linearCombination R v))

Tactic:
map_linearCombination

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
ι : Type u_9
v : ι → M
H : ∀ (P : Ideal R) [inst : P.IsMaximal], LinearIndependent (Rₚ P) (⇑(f P) ∘ v)
P : Ideal R
x✝ : P.IsMaximal
⊢ Function.Injective ⇑(↑R (Finsupp.linearCombination (Rₚ P) (⇑(f P) ∘ v)))
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this : Nontrivial T
⊢ IsFractionRing S T

Tactic:
have := (algebraMap S T).domain_nontrivial

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
⊢ IsFractionRing S T
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
⊢ (algebraMap R Rₚ) x✝ ∈ Ideal.map (algebraMap R Rₚ) p ^ n ↔ x✝ ∈ p ^ n

Tactic:
← Ideal.map_pow,

Goal state after:
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
⊢ (algebraMap R Rₚ) x✝ ∈ Ideal.map (algebraMap R Rₚ) (p ^ n) ↔ x✝ ∈ p ^ n
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
⊢ (Matrix.fromBlocks A B C D).IsSymm

Tactic:
have hCB : Cᵀ = B := by
    rw [← hBC]
    simp

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 C D).IsSymm
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

Tactic:
by_cases ha : e t_i = a <;> by_cases hb : e t_j = b <;> by_cases hab : a = b

Goal state after:
case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : e t_i = a
hb : ¬e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case pos
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
hab : a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b

case neg
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
ha : ¬e t_i = a
hb : ¬e t_j = b
hab : ¬a = b
⊢ (1 + single (e t_i) (e t_j) c✝) a b = (reindexAlgEquiv R R e) (1 + single t_i t_j c✝) a b
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: 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
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
by
  have inj := FaithfulSMul.algebraMap_injective R T
  have := inj.noZeroDivisors _ (map_zero _) (map_mul _)
  cases subsingleton_or_nontrivial R
  · have := (algebraMap R T).codomain_trivial; simp only [rank_subsingleton, lift_one]
  have := (isDomain_iff_noZeroDivisors_and_nontrivial T).mpr
    ⟨‹_›, (FaithfulSMul.algebraMap_injective R T).nontrivial⟩
  let FR := FractionRing R
  let FT := FractionRing T
  replace inj : Function.Injective (algebraMap R FT) := (IsFractionRing.injective T _).comp inj
  let g := TensorProduct.mk T FT P 1
  have : IsLocalizedModule R⁰ (TensorProduct.mk R FR FT 1) := inferInstance
  let _ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
  let _ := isLocalizedModule_iff_isLocalization.mp this |>.atUnits _ _ ?_ |>.symm.isField
    (Field.toIsField FT) |>.toField
  on_goal 2 => rintro _ ⟨_, mem, rfl⟩; exact (map_ne_zero_of_mem_nonZeroDivisors _ inj mem).isUnit
  have := bc.comp_iff.2 ((isLocalizedModule_iff_isBaseChange T⁰ FT g).1 inferInstance)
  rw [← lift_inj.{_, max uT uP}, lift_lift, lift_lift, ← lift_lift.{max uT uP, uM},
    ← IsLocalizedModule.lift_rank_eq T⁰ g le_rfl, lift_lift, ← lift_lift.{uM},
    ← IsLocalization.rank_eq FT T⁰ le_rfl,
    lift_rank_eq_of_le_nonZeroDivisors FR (LocalizedModule.mkLinearMap R⁰ M) le_rfl
      (map_le_nonZeroDivisors_of_injective _ inj le_rfl) this, lift_lift]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : -((∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s) * ↑s ^ x = g 0 * r * ↑s ^ x
⊢ g i = 0

Tactic:
← neg_mul

Goal state after:
case neg
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
⊢ g i = 0
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 • 1 = ↑(Fintype.card n)

Tactic:
nsmul_one,

Goal state after:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ ↑Finset.univ.card = ↑(Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹ = A⁻¹ʳ

Tactic:
by_cases h_det : IsUnit A.det
  · cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible
    rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
  · have h := mt A.isUnit_iff_isUnit_det.mp h_det
    rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]

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

Goal state before:
pp: m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ LinearIndependent K A.col ↔ IsUnit A

Tactic:
← row_transpose,

Goal state after:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ LinearIndependent K Aᵀ.row ↔ IsUnit A
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
⊢ ∀ x ∈ univ, (fun j ↦ M i j) x * (fun j_1 ↦ N j_1 j) x = 0

Tactic:
intro k _

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
⊢ (fun j ↦ M i j) k * (fun j_1 ↦ N j_1 j) k = 0
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 R
⊢ ∑ p, (algebraMap R A) (M p.1 p.2) ⊗ₜ[R] single p.1 p.2 1 = 1 ⊗ₜ[R] M

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum]

Goal state after:
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 R
⊢ 1 ⊗ₜ[R] ∑ a, M a.1 a.2 • single a.1 a.2 1 = 1 ⊗ₜ[R] M
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: case e_f
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
i : ℕ
⊢ f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * ↑(powSubPowFactor x y i) * (x - y)

Tactic:
rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]

Goal state after: