mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f

Tactic:
obtain ⟨A₂, π₂, hπ₂, x₁, hx₁⟩ := S.exact_C₁_down.exact_up_to_refinements (p ≫ S.φ₁) hp'

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₀.X₃
hx₃ : x₃ ≫ S.δ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
hπ₁ : Epi π₁
p : A₁ ⟶ S.P
hp : π₁ ≫ x₃ = p ≫ pullback.snd S.L₁.g S.v₀₁.τ₃
hp' : (p ≫ S.φ₁) ≫ S.v₂₃.τ₁ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₁ : A₂ ⟶ { X₁ := S.L₁.X₁, X₂ := S.L₂.X₁, X₃ := S.L₃.X₁, f := S.v₁₂.τ₁, g := S.v₂₃.τ₁, zero := ⋯ }.X₁
hx₁ : π₂ ≫ p ≫ S.φ₁ = x₁ ≫ { X₁ := S.L₁.X₁, X₂ := S.L₂.X₁, X₃ := S.L₃.X₁, f := S.v₁₂.τ₁, g := S.v₂₃.τ₁, zero := ⋯ }.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
⊢ ∀ ⦃X Y : WalkingMulticospan J⦄ (f : X ⟶ Y),
    (((Functor.const (WalkingMulticospan J)).obj P).map f ≫
        match Y with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) =
      (match X with
        | WalkingMulticospan.left a => ι a
        | WalkingMulticospan.right b => ι (J.fst b) ≫ I.fst b) ≫
        I.multicospan.map f

Tactic:
rintro (_ | _) (_ | _) (_ | _ | _) <;>
          simp only [WalkingMulticospan.Hom.id_eq_id,
            Functor.map_id, Functor.const_obj_map, Category.comp_id] <;>
          dsimp

Goal state after:
case left.left.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.L
⊢ 𝟙 P ≫ ι a✝ = ι a✝

case left.right.fst
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝

case left.right.snd
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.snd a✝) ≫ I.snd a✝

case right.right.id
C : Type u
inst✝ : Category.{v, u} C
J✝ : MulticospanShape
I✝ : MulticospanIndex J✝ C
K : Multifork I✝
J : MulticospanShape
I : MulticospanIndex J C
P : C
ι : (a : J.L) → P ⟶ I.left a
w : ∀ (b : J.R), ι (J.fst b) ≫ I.fst b = ι (J.snd b) ≫ I.snd b
a✝ : J.R
⊢ 𝟙 P ≫ ι (J.fst a✝) ≫ I.fst a✝ = ι (J.fst a✝) ≫ I.fst a✝
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
a : J.L
⊢ I.fst a ≫ K.π (J.fst a) = K.ι.app (WalkingMultispan.left a)

Tactic:
← K.fst_app_right

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = K.ι.app (WalkingMultispan.left 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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
A B : J
f : A ⟶ B
⊢ ((const J).obj (conePoint c t)).map f ≫ { f := c.π.app B, h := ⋯ } = { f := c.π.app A, h := ⋯ } ≫ D.map f

Tactic:
ext1
        dsimp
        rw [id_comp, ← c.w]
        rfl

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
⊢ PreservesColimit (F ⋙ R) (comonadicRightAdjoint R)

Tactic:
by
      constructor
      intro c h
      have : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
      have : HasColimit F := hasColimit_of_coreflective F R
      constructor
      apply isColimitChangeEmptyCocone D (colimit.isColimit F)
      apply (asIso ((comonadicAdjunction R).unit.app _)).trans
      apply (comonadicRightAdjoint R).mapIso
      letI := comonadicCreatesColimits.{v, v} R
      let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F R
      apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h

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

Goal state before:
pp: M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : Semiring R✝
inst✝³ : MulSemiringAction M R✝
inst✝² : MulSemiringAction N R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : MulSemiringAction M R
a : M
⊢ a • 1 = 1

Tactic:
simp only [Ideal.one_eq_top]

Goal state after:
M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : Monoid N
inst✝⁴ : Semiring R✝
inst✝³ : MulSemiringAction M R✝
inst✝² : MulSemiringAction N R✝
R : Type u_4
inst✝¹ : CommRing R
inst✝ : MulSemiringAction M R
a : M
⊢ a • ⊤ = ⊤
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
rw [IsPrimary, Submodule.IsPrimary, forall_comm]
  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.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Submodule R M
hS : S.IsPrimary
m : M
inst✝ : Decidable (m ∈ S)
⊢ (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical

Tactic:
by
  split_ifs with hm
  · rwa [radical_eq_top, colon_eq_top_iff_subset, Set.singleton_subset_iff]
  · exact hS.radical_colon_singleton_of_notMem hm

Goal state after:
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
a : A
p : R[X]
⊢ ((toFunBilinear R A) a) p = p.sum fun n r ↦ (monomial n) (a * (algebraMap R A) r)

Tactic:
conv_lhs => rw [toFunBilinear_apply_eq_smul, ← p.sum_monomial_eq, sum, Polynomial.map_sum]
  simp [Finset.smul_sum, sum, ← smul_eq_mul]

Goal state after:
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[X]
⊢ (toFunAlgHom R A) (invFun R A x) = x

Tactic:
refine Polynomial.induction_on' x ?_ ?_

Goal state after:
case refine_1
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    (toFunAlgHom R A) (invFun R A p) = p →
      (toFunAlgHom R A) (invFun R A q) = q → (toFunAlgHom R A) (invFun R A (p + q)) = p + q

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) (invFun R A ((monomial n) a)) = (monomial n) a
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: 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
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
⊢ ⊥ < Ideal.under R p

Tactic:
have : IsDomain S := isDomain_of_le_nonZeroDivisors _ hM
  rw [← Ideal.comap_bot_of_injective (algebraMap R S) (IsLocalization.injective _ hM)]
  convert!
    (orderIsoOfPrime M S).lt_iff_lt.mpr
      (show (⟨⊥, Ideal.isPrime_bot⟩ : { p : Ideal S // p.IsPrime }) < ⟨p, hpp⟩ from hp0.bot_lt)

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : FiniteType R S
s : Finset S
hs : adjoin R ↑s = ⊤
x✝ : S
⊢ ∃ t ∈ adjoin R ↑s, IsUnit t ∧ x✝ * t ∈ adjoin R ↑s

Tactic:
simpa only [hs, mem_top, and_true, true_and] using ⟨1, isUnit_one⟩

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
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
h : IsLocalRing S
⊢ (algebraMap R S) x ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using!
      isUnit_to_map_iff S I x

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ S.mkQ (m ⊗ₜ[R] (a • n)) = (RingHom.id A) a • S.mkQ (m ⊗ₜ[R] n)

Tactic:
by
          rw [Submodule.mkQ_apply, Submodule.mkQ_apply, ← Submodule.Quotient.mk_smul, eq_comm,
            Submodule.Quotient.eq, RingHom.id_apply]
          exact Submodule.subset_span ⟨a, m, n, rfl⟩

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
⊢ P f

Tactic:
apply_fun Ideal.map f at hs

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.map f (Ideal.span s) = Ideal.map f ⊤
⊢ P f
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
m : Ideal R
hm : m.IsMaximal
hx : ∀ (i : Ideal R) (i_1 : i.IsPrime), I ≤ i → (algebraMap R (Localization.AtPrime i)) x = 0
hle : ¬I ≤ m
⊢ (algebraMap R (Localization.AtPrime m)) x ∈ map (algebraMap R (Localization.AtPrime m)) I

Tactic:
· simp [IsLocalization.AtPrime.map_eq_top_of_not_le _ hle]

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

Goal state before:
pp: case h.refine_2
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 + γ
⊢ (algebraMap S Sₚ) (↑s * β • x) - (algebraMap S Sₚ) x = (algebraMap S Sₚ) (γ • x)

Tactic:
← e,

Goal state after:
case h.refine_2
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 + γ
⊢ (algebraMap S Sₚ) ((algebraMap R S) α * β • x) - (algebraMap S Sₚ) x = (algebraMap S Sₚ) (γ • x)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case empty
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ M (∑ n ∈ ∅, C (p.coeff n) * T n)

pp: case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ ∀ (a : ℤ) (s : Finset ℤ), a ∉ s → M (∑ n ∈ s, C (p.coeff n) * T n) → M (∑ n ∈ insert a s, C (p.coeff n) * T n)

Tactic:
· convert! h_C 0
      simp only [Finset.sum_empty, map_zero]

Goal state after:
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ ∀ (a : ℤ) (s : Finset ℤ), a ∉ s → M (∑ n ∈ s, C (p.coeff n) * T n) → M (∑ n ∈ insert a s, C (p.coeff n) * T n)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ LeftInverse ⇑trunc ⇑toLaurent

Tactic:
refine fun f => f.induction_on' ?_ ?_

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (p q : R[X]), trunc (toLaurent p) = p → trunc (toLaurent q) = q → trunc (toLaurent (p + q)) = p + q

case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (n : ℕ) (a : R), trunc (toLaurent ((monomial n) a)) = (monomial n) a
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ toLaurent (Polynomial.C a) = C a * T (Int.negSucc n) * T ↑(n + 1)

Tactic:
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.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (f * T ↑0)

Tactic:
← Nat.sub_self n,

Goal state after:
R : Type u_1
inst✝ : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T : ∀ (f : R[X]) (n : ℕ), motive (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ motive (f * T ↑(n - n))
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A.updateRow i (Pi.single j 1)).det = (Aᵀ.updateRow j (Pi.single i 1)).det

Tactic:
updateRow_transpose,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A.updateRow i (Pi.single j 1)).det = (A.updateCol j (Pi.single i 1))ᵀ.det
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
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
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
h' : (Equiv.symm σ) i = j
⊢ False

Tactic:
exact h ((symm_apply_eq σ).mp h')

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

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[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
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max uM uN, max (max uS uT) uP} (Cardinal.lift.{uP, max (max uP uS) uT} (Module.rank ST (ST ⊗[T] P))) =
    Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
      (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))

Tactic:
lift_id'.{uP, max uS uT},

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
inst✝⁴ : StrongRankCondition (S ⊗[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
ST : Type (max uS uT) := S ⊗[R] T
x✝ : Algebra T ST := Algebra.TensorProduct.rightAlgebra
pT : Submonoid T := Algebra.algebraMapSubmonoid T p
hpT : pT ≤ T⁰
⊢ Cardinal.lift.{max uM uN, max (max uS uT) uP} (Module.rank ST (ST ⊗[T] P)) =
    Cardinal.lift.{uM, max (max uS uT uP) (max uN uS) uT}
      (Cardinal.lift.{max uS uT uP, max (max uN uS) uT} (Module.rank ST (ST ⊗[S] N)))
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

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

Tactic:
have : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card
    rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]

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

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
h : A = C * B
⊢ ⅟C * A = B

Tactic:
rw [h, Matrix.invOf_mul_cancel_left]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * B * C).trace = (C * A * B).trace

Tactic:
rw [trace_mul_comm, Matrix.mul_assoc]

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 α
j : n
⊢ A.det = ∑ i, A i j * A.adjugate j i

Tactic:
by
  simpa only [det_transpose, ← adjugate_transpose] using! det_eq_sum_mul_adjugate_row Aᵀ j

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 C h
    refine hA.matrix ?_
    simp only at h ⊢
    rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←
      adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ (↑M * N * (↑M)⁻¹).charpoly = N.charpoly

Tactic:
rw [Matrix.charpoly_mul_comm, ← mul_assoc]

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * ↑M * N).charpoly = N.charpoly
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank

Tactic:
by
  rw [← generators_card p, lift_spanRank_le_iff_exists_span_set_card_le]
  exact ⟨f '' p.generators, Cardinal.mk_image_le_lift, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦
    ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective ⇑g
x : S
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) (g x) p = 0
⊢ g (eval₂ f x p) = g 0

Tactic:
simp [Polynomial.hom_eval₂, hx]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst✝⁹ : Ring B
inst✝⁸ : Ring C
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : Algebra R C
inst✝⁴ : IsScalarTower R A B
inst✝³ : Algebra A C
inst✝² : IsScalarTower R A C
b : B
inst✝¹ : FunLike F B C
inst✝ : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ IsIntegral R (f b)

Tactic:
by
  rw [IsIntegral, ← ((AlgHomClass.toAlgHom f).restrictScalars R).comp_algebraMap]
  exact .map hb (RingHomClass.toRingHom f)

Goal state after: