mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: case succ
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ x.teichmullerAux (m + 1) ≡ x.teichmullerAux (m + 1 + 1) [SMOD I ^ (m + 1)]

Tactic:
symm

Goal state after:
case succ
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : CharP (R ⧸ I) p
x : Perfection (R ⧸ I) p
m : ℕ
⊢ x.teichmullerAux (m + 1 + 1) ≡ x.teichmullerAux (m + 1) [SMOD I ^ (m + 1)]
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ constantCoeff (z • X 0) = 0

Tactic:
simp only [smul_zero, map_zsmul, constantCoeff_X]

Goal state after:
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ φ = wittStructureInt p Φ

Tactic:
funext k

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ φ k = wittStructureInt p Φ k
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (fun i ↦ (MvPolynomial.eval x) (verschiebungPoly i)) = (verschiebung (mk p x)).coeff

Tactic:
funext k

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
k : ℕ
⊢ (MvPolynomial.eval x) (verschiebungPoly k) = (verschiebung (mk p x)).coeff k
Module: Mathlib.RingTheory.WittVector.MulP

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
⊢ (x * ↑n).coeff = fun n_1 ↦ (aeval x.coeff) (wittMulN p n n_1)

Tactic:
funext k

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_2
_Rcr : CommRing R
x : 𝕎 R
k : ℕ
⊢ (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
hg : IsPoly₂ p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R), f x y = g x y

Tactic:
obtain ⟨φ, hf⟩ := hf
  obtain ⟨ψ, hg⟩ := hg
  intros
  ext n
  rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq' p φ ψ]
  intro k
  apply MvPolynomial.funext
  intro x
  simp only [hom_bind₁]
  specialize h (ULift ℤ) (mk p fun i => ⟨x (0, i)⟩) (mk p fun i => ⟨x (1, i)⟩) k
  simp only [ghostComponent_apply, aeval_eq_eval₂Hom] at h
  apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
  simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]
  convert! h using 1
  all_goals
    simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext1
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext ⟨b, _⟩
    fin_cases b <;> simp only [coeff_mk, uncurry] <;> rfl

Goal state after:
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
⊢ (select P z + select (fun i ↦ ¬P i) z).coeff n = z.coeff n

Tactic:
select_add_select_not P z

Goal state after:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
⊢ z.coeff n = z.coeff n
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : 𝕎 (R ⧸ 𝔭)
h : 𝔭 ^ (0 + 1) = 𝔭
y : 𝕎 R
hy : (map (Ideal.Quotient.mk 𝔭)) y = x
⊢ (quotEquivOfEq h) ((ghostComponentModPPow 0) x) = (ghostComponent 0) x

Tactic:
simp [← hy, ghostComponent_apply]

Goal state after:
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n✝ i : ℕ
hi : i < n✝ + 1
n : ℕ
x✝¹ x✝ :
  ↑{r | r ∈ Finset.Iic n✝ ∧ ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n ≠ 0}
a : ℕ
left✝¹ : a ∈ Finset.Iic n✝
ha : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ a) (x.coeff a)) * ↑p ^ a).coeff n ≠ 0
b : ℕ
left✝ : b ∈ Finset.Iic n✝
hb : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ b) (x.coeff b)) * ↑p ^ b).coeff n ≠ 0
⊢ a = b

Tactic:
rw [← Not.imp_symm (teichmuller_mul_pow_coeff_of_ne _) ha]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n✝ i : ℕ
hi : i < n✝ + 1
n : ℕ
x✝¹ x✝ :
  ↑{r | r ∈ Finset.Iic n✝ ∧ ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n ≠ 0}
a : ℕ
left✝¹ : a ∈ Finset.Iic n✝
ha : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ a) (x.coeff a)) * ↑p ^ a).coeff n ≠ 0
b : ℕ
left✝ : b ∈ Finset.Iic n✝
hb : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ b) (x.coeff b)) * ↑p ^ b).coeff n ≠ 0
⊢ n = b
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
← add_sub_cancel_left 1 (-(_ * _)),

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map ι f)
a b : R[X]
h : f = a * b
hb : IsUnit (Polynomial.map ι b)
hn : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (b.coeff i)
hc : 1 - a.coeff f.natDegree * b.coeff 0 = ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (1 + -(a.coeff f.natDegree * b.coeff 0) - 1)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ ∑ x ∈ Finset.range n.succ, p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1)) =
    ∑ i ∈ p.support, p.coeff i * ↑((n + d - i).choose d)

Tactic:
symm

Goal state after:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
n : ℕ
hn : p.natDegree < n
d : ℕ
hd :
  (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)
h_le : ∀ (i : ↥p.support), ↑i ≤ n
h : ∀ (i : ↥p.support), eval (↑n) (preHilbertPoly F d ↑i) = ↑((n + d - ↑i).choose d)
⊢ ∑ i ∈ p.support, p.coeff i * ↑((n + d - i).choose d) =
    ∑ x ∈ Finset.range n.succ, p.coeff x * ↑((d.succ - 1 + (n - x)).choose (d.succ - 1))
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (0 - X)

Tactic:
zero_sub

Goal state after:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ ↑n ! * shiftedLegendre n = (⇑derivative)^[n] (X ^ n * (1 - X) ^ n)

Tactic:
symm

Goal state after:
n : ℕ
⊢ (⇑derivative)^[n] (X ^ n * (1 - X) ^ n) = ↑n ! * shiftedLegendre n
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (⇑derivative)^[n] ((X - X ^ 2) ^ n) = (⇑derivative)^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m))

Tactic:
congr
    rw [sub_eq_add_neg, add_comm, add_pow]
    congr! 1 with m hm
    rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc,
      ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm]
    rw [Finset.mem_range] at hm
    linarith

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ 0 • f = 0

Tactic:
simp_rw [HSMul.hSMul, SMul.smul]; simp only [Nat.cast_zero, zero_smul f]

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

Goal state before:
pp: R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M ((↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp φ.rangeRestrict)).toLinearMap) p) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)

Tactic:
comp_toLinearMap,

Goal state after:
R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
ht : (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)
⊢ f.toFun' (RingCon.ker ↑ψ).Quotient
      ((rTensor M ((↑(quotientKerEquivRangeₐ ψ).symm).toLinearMap ∘ₗ (h'.comp φ.rangeRestrict).toLinearMap)) p) =
    f.toFun' (RingCon.ker ↑ψ).Quotient ((rTensor M (mkₐ R (RingCon.ker ↑ψ)).toLinearMap) q)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')

Tactic:
have hA'B' : (φ R s').range ≤ (φ R t).range := le_trans hA'B (le_of_eq hB)

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (rTensor M φ.rangeRestrict.toLinearMap) p = (rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (rTensor M φ.toLinearMap) p = (rTensor M (φ.range.val.comp (Subalgebra.inclusion hφ)).toLinearMap) u

Tactic:
comp_toLinearMap,

Goal state after:
case h
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (rTensor M φ.rangeRestrict.toLinearMap) p = (rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (rTensor M φ.toLinearMap) p = (rTensor M (φ.range.val.toLinearMap ∘ₗ (Subalgebra.inclusion hφ).toLinearMap)) u
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case hpq
R : Type u
inst✝⁸ : CommSemiring R
M : Type u_1
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
f : M →ₚₗ[R] N
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (rTensor M (rename j).toLinearMap) p
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
n : Fin s.card
⊢ h ((φ R s) (X n)) = (φ R s') (X (s'.equivFin ⟨h ↑(s.equivFin.symm n), ⋯⟩))

Tactic:
simp only [φ, aeval_X, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n✝ : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1))) → HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (n + 1 + 1))
L : ModuleCat R
this : ∀ (m : ℕ), Subsingleton (Ext S.X₂ L (m + 1))
⊢ 1 + 3 ≤ 5

Tactic:
decide

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : g * (a + H.div f') + ↑(H.mod f') = g * H.div f + ↑(H.mod f)
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
hf'1 : (H.mod f').degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf'2 : f' = g * H.div f' + ↑(H.mod f')
⊢ H.mod f = H.mod f'

Tactic:
exact (H.eq_of_mul_add_eq_mul_add hf'1 hf1 ha).2.symm

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
epi :
  Epi
    { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
        X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
        g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.f
this : S.f = x • 𝟙 M
⊢ Subsingleton (Ext M L (n + 1))

Tactic:
simp only [S, this, AddCommGrpCat.epi_iff_surjective, AddCommGrpCat.hom_ofHom] at epi

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
n✝ n : ℕ
S : ShortComplex (ModuleCat R) := M.smulShortComplex x
hS : S.ShortExact
h : HasProjectiveDimensionLE (of R (QuotSMulTop x ↑M)) (n + 1)
L : ModuleCat R
a✝ : Module.Finite R ↑L
zero : Subsingleton (Ext (of R (QuotSMulTop x ↑M)) L (n + 2))
exac :
  { X₁ := AddCommGrpCat.of (Ext S.X₂ L (n + 1)), X₂ := AddCommGrpCat.of (Ext S.X₁ L (n + 1)),
      X₃ := AddCommGrpCat.of (Ext S.X₃ L (n + 2)), f := AddCommGrpCat.ofHom ((Ext.mk₀ S.f).precomp L ⋯),
      g := AddCommGrpCat.ofHom (hS.extClass.precomp L ⋯), zero := ⋯ }.Exact
this : S.f = x • 𝟙 M
epi : Function.Surjective ⇑((Ext.mk₀ (x • 𝟙 M)).precomp L ⋯)
⊢ Subsingleton (Ext M L (n + 1))
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
reg : IsWeaklyRegular (↑M) rs
mem : ∀ r ∈ rs, r ∈ maximalIdeal R
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑rs.length

Tactic:
by
  generalize len : rs.length = n
  induction n generalizing M rs with
  | zero =>
    rw [List.length_eq_zero_iff.mp len, Ideal.ofList_nil, Submodule.bot_smul]
    simpa using projectiveDimension_eq_of_iso (Submodule.quotEquivOfEqBot ⊥ rfl).toModuleIso
  | succ n hn =>
    match rs with
    | [] => simp at len
    | x :: rs' =>
      simp only [List.mem_cons, forall_eq_or_imp] at mem
      simp only [isWeaklyRegular_cons_iff] at reg
      have := nontrivial_quotSMulTop_of_mem_maximalIdeal M mem.1
      simp only [List.length_cons, Nat.add_right_cancel_iff] at len
      rw [Nat.cast_add, Nat.cast_one, projectiveDimension_eq_of_iso
        (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x rs').toModuleIso, add_comm _ 1,
        ← add_assoc, ← projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular M x reg.1 mem.1,
        ← hn (ModuleCat.of R (QuotSMulTop x M)) rs' reg.2 mem.2 len]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case mem_mul_mem
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz : J.toCotangent w = f (J.toCotangent ⟨z, hz⟩)
mem_bot : y * (Submodule.subtype J) w = 0
eq0 : y • w = 0
this : ⟨y * z, ⋯⟩ = y • ⟨z, hz⟩
⊢ J.toCotangent (y • w) = 0

Tactic:
eq0,

Goal state after:
case mem_mul_mem
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz : J.toCotangent w = f (J.toCotangent ⟨z, hz⟩)
mem_bot : y * (Submodule.subtype J) w = 0
eq0 : y • w = 0
this : ⟨y * z, ⋯⟩ = y • ⟨z, hz⟩
⊢ J.toCotangent 0 = 0
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case refine_2.mk
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
use α

Goal state after:
case h
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ Disjoint (⋃₀ s) (⋂ x, f ↑x ⋯)

Tactic:
rw [disjoint_sUnion_left]

Goal state after:
case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ ∀ s_1 ∈ s, Disjoint s_1 (⋂ x, f ↑x ⋯)