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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i : ℕ
⊢ (verschiebung x).coeff (i + 1) ^ p = x.coeff i ^ p

Tactic:
verschiebung_coeff_succ

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i : ℕ
⊢ x.coeff i ^ p = x.coeff i ^ p
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ (verschiebung ((⇑verschiebung)^[k] x)).coeff (k✝ + k).succ = x.coeff k✝

Tactic:
verschiebung_coeff_succ

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
⊢ frobenius = map (_root_.frobenius R p)

Tactic:
ext (x n)

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (frobenius x).coeff n = ((map (_root_.frobenius R p)) x).coeff n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
obtain rfl | hf := eq_or_ne f 0

Goal state after:
case inl
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
g : PreTilt O p
⊢ valAux K v O p (0 * g) = valAux K v O p 0 * valAux K v O p g

case inr
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0

pp: case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
· intro i _ h0
    simp [teichmullerFun, h0, hp.1.ne_zero]

Goal state after:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : R
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
rcases counit_surjective R x with ⟨x, rfl⟩

Goal state after:
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
y : R
x : MvPolynomial R ℤ
⊢ teichmullerFun p ((counit R) x * y) = teichmullerFun p ((counit R) x) * teichmullerFun p y
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)

Tactic:
obtain rfl | hf := eq_or_ne f 0

Goal state after:
case inl
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
g : PreTilt O p
⊢ valAux K v O p (0 + g) ≤ max (valAux K v O p 0) (valAux K v O p g)

case inr
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
⊢ valAux K v O p (f + g) ≤ max (valAux K v O p f) (valAux K v O p g)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ 2 * C ⅟2 = 1

Tactic:
two_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ C ⅟2 + C ⅟2 = 1
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ dickson 1 ((Int.castRingHom R) 1) (m * n) =
    (dickson 1 ((Int.castRingHom R) 1) m).comp (dickson 1 ((Int.castRingHom R) 1) n)

Tactic:
simp only [← map_dickson (Int.castRingHom R), ← map_comp]

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ map (Int.castRingHom R) (dickson 1 1 (m * n)) = map (Int.castRingHom R) ((dickson 1 1 m).comp (dickson 1 1 n))
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + (k + 2)).choose (k + 2) * (k + 2)

Tactic:
(by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))

Goal state after:
case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 2) * (k + 2)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff (k + 2) = hermite_explicit n (k + 2)

Tactic:
(by ring : 2 * (n + 1) + k = 2 * n + (k + 2)),

Goal state after:
case e_a.e_a
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * n + (k + 2))).coeff (k + 2) = hermite_explicit n (k + 2)
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 =
    ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x) +
      a.coeff f.natDegree * b.coeff (f.natDegree - f.natDegree)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))

Tactic:
← sub_eq_iff_eq_add,

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 (f.natDegree - f.natDegree) =
    ∑ x ∈ Finset.range f.natDegree, a.coeff x * b.coeff (f.natDegree - x)
⊢ IsUnit (-(a.coeff f.natDegree * b.coeff 0))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case h.right
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ (y : F[X]),
    (fun h ↦ ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) y → y = p.hilbertPoly d

Tactic:
· rintro h ⟨N, hhN⟩
    apply eq_of_infinite_eval_eq h (hilbertPoly p d)
    apply ((Set.Ioi_infinite (max N p.natDegree)).image cast_injective.injOn).mono
    rintro x ⟨n, hn, rfl⟩
    simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_ofPred_eq] at hn ⊢
    rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsCancelMulZero R[X] ∧ Nontrivial R[X] ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R

Tactic:
nontrivial_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ IsCancelMulZero R[X] ∧ Nontrivial R ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
Module: Mathlib.RingTheory.PowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ MvPowerSeries.IsRestricted (fun x ↦ c) f ↔ Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)

Tactic:
MvPowerSeries.IsRestricted,

Goal state after:
R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ Tendsto (fun t ↦ ‖(MvPowerSeries.coeff t) f‖ * t.prod fun x1 x2 ↦ c ^ x2) cofinite (𝓝 0) ↔
    Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ constantCoeff (log A) = 0

Tactic:
simp [← coeff_zero_eq_constantCoeff_apply]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : u ∈ (rTensor N P.subtype).range
s : Finset S
hs : span R ↑s = P
⊢ ∃ A, A.FG ∧ u ∈ (rTensor N A.val.toLinearMap).range

Tactic:
use Algebra.adjoin R s, Subalgebra.fg_adjoin_finset _

Goal state after:
case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : u ∈ (rTensor N P.subtype).range
s : Finset S
hs : span R ↑s = P
⊢ u ∈ (rTensor N (Algebra.adjoin R ↑s).val.toLinearMap).range
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
hs : s = (X ^ n * mk fun i ↦ (coeff (i + n)) s) + ↑((trunc n) s)
⊢ (coeff i) (f - g * (q + (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) s) * ↑⋯.unit⁻¹)) ∈
    I ^ (k + 1)

Tactic:
set s₀ := s.trunc n

Goal state after:
case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
hs : s = (X ^ n * mk fun i ↦ (coeff (i + n)) s) + ↑s₀
⊢ (coeff i) (f - g * (q + (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) s) * ↑⋯.unit⁻¹)) ∈
    I ^ (k + 1)
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
h✝ :
  (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t) =
    (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (rTensor N (Subalgebra.inclusion hB_le).toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t) =
    (rTensor N (Subalgebra.inclusion hB_le).toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t')
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

Tactic:
use B, le_trans le_sup_left hB_le, le_trans le_sup_right hB_le, hB

Goal state after:
case right
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
hj : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A.val
hj' : (A ⊔ A').val.comp (Subalgebra.inclusion ⋯) = A'.val
h✝ :
  (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t) =
    (rTensor N (A ⊔ A').val.toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t')
B : Subalgebra R S
hB_le : A ⊔ A' ≤ B
hB : B.FG
h :
  (rTensor N (Subalgebra.inclusion hB_le).toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t) =
    (rTensor N (Subalgebra.inclusion hB_le).toLinearMap) ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t')
⊢ (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t = (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) t'
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
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
⊢ s ∈ (φ R gen).range

Tactic:
rw [hgen]

Goal state after:
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 : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ (rTensor M A.val.toLinearMap).range
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (rTensor M (φ R gen).toLinearMap) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R ↑{s}
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
hb : π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t
⊢ (rTensor P (φ R s).toLinearMap)
      ((g.toFun' (MvPolynomial (Fin s.card) R) ∘ f.toFun' (MvPolynomial (Fin s.card) R)) p) =
    (rTensor P (φ R s).toLinearMap) (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))

Tactic:
Function.comp_apply

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
hb : π R N S ⟨s, f.toFun' (MvPolynomial (Fin s.card) R) p⟩ = toFun S f t
⊢ (rTensor P (φ R s).toLinearMap) (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p)) =
    (rTensor P (φ R s).toLinearMap) (g.toFun' (MvPolynomial (Fin s.card) R) (f.toFun' (MvPolynomial (Fin s.card) R) p))
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁸ : CommSemiring R₀
inst✝⁷ : Ring R
inst✝⁶ : Algebra R₀ R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Module.Finite R M
d : ↑(isotypicComponents R M) → ℕ
pos : ∀ (c : ↑(isotypicComponents R M)), NeZero (d c)
S : ↑(isotypicComponents R M) → Submodule R M
h✝ : ∀ (c : ↑(isotypicComponents R M)), S c ≤ ↑c
simple : ∀ (c : ↑(isotypicComponents R M)), IsSimpleModule R ↥(S c)
e : ∀ (c : ↑(isotypicComponents R M)), Nonempty (↥↑c ≃ₗ[R] Fin (d c) → ↥(S c))
⊢ ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (End R ↥(S i)))

Tactic:
exact ⟨_, _, _, fun _ ↦ simple _, fun _ ↦ pos _, ⟨.trans (endAlgEquiv R₀ R M) <| .trans
    (.piCongrRight fun c ↦ ((e c).some.conjAlgEquiv R₀).trans (endVecAlgEquivMatrixEnd ..)) <|
    (.piCongrLeft' R₀ _ (Finite.equivFin _))⟩⟩

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

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : (IsFractionRing.ringEquivOfRingEquiv (frobeniusEquiv p k)) b * a = ↑p ^ m * b
⊢ φ(p, k) b * a = ↑p ^ m * b

Tactic:
convert! hmb

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: case refine_2
o₁ o₂ : Ordinal.{u_1}
⊢ (∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂) → AddCommute o₁ o₂

Tactic:
· rintro ⟨o, n₁, n₂, rfl, rfl⟩
    rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
h₁ : of' l₁ ~ of' l₁
h₂ : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃

pp: case C1.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ l₃
⊢ of' l₁ ~ l₃

Tactic:
· exact h₂

Goal state after:
case C1.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ l₃
⊢ of' l₁ ~ l₃
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ gfpApprox f ≤ gfpApprox g

Tactic:
have : g.dual ≤ f.dual := h

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
this : OrderHom.dual g ≤ OrderHom.dual f
⊢ gfpApprox f ≤ gfpApprox g
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
h : IsMin a
⊢ 𝓝 a = pure a

Tactic:
nhds_eq_pure,

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
h : IsMin a
⊢ ¬IsSuccLimit a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).cmp 0 = Ordering.eq
⊢ e.oadd n a = 0

Tactic:
injection h

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : cmp 0 (e.oadd n a) = Ordering.eq
⊢ 0 = e.oadd n a

Tactic:
injection h

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : (mk β B).Equiv (A a)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Tactic:
rw [← eta (A a)] at e

Goal state after:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : (mk β B).Equiv (mk (A a).Type (A a).Func)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h✝ : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
h : e.oadd n a = 0
⊢ False

Tactic:
injection h

Goal state after:
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{v + 1, max u v} (lift.{u, v} (⋃ (i : α), f i).card) ≤ lift.{v + 1, max u v} (sum fun i ↦ (f i).card)

Tactic:
simpa [cardinalMk_coe_sort, ← coe_iUnion, -mem_iUnion] using
    mk_iUnion_le_sum_mk_lift (f := SetLike.coe ∘ f)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case neg
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

Tactic:
simp_rw [mem_range_veblen h, veblen_opow_eq_opow_iff]

Goal state after:
case neg
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ∀ b < x.invVeblen₁, veblen b x = x
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match n✝ + 1 with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).NFBelow
    b

Tactic:
· exact NFBelow.oadd h₁.fst h₁.snd h₁.lt

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : e₂ = 0
x : ℕ
xe : ↑n₂ = x.succ
⊢ ω ^ e₁.repr * (↑↑n₁ * ↑x.succ) + a₁.repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * ↑x.succ

Tactic:
rw [Nat.cast_add_one x, add_mul_add_one _ ao, mul_assoc]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
injection h

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
fst_eq✝ : scale 1 a = o'
snd_eq✝ : n = m
⊢ o'.NF ∧ o.repr = o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Tactic:
injection h

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
e : o.split' = (a, n)
fst_eq✝ : scale 1 a = o'
snd_eq✝ : n = m
⊢ ω ∣ o'.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ ∀ (k m : ℕ), (e.opowAux a0 a k m).NF

Tactic:
by
  intro k m
  unfold opowAux
  cases m with
  | zero => cases k <;> exact NF.zero
  | succ m =>
    cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      have := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance

Goal state after: