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

Goal state before:
pp: case refine_3.zero
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (ghostComponent 0) (x✝ + y✝).verschiebungFun = (ghostComponent 0) (x✝.verschiebungFun + y✝.verschiebungFun)

pp: case refine_3.succ
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ (ghostComponent (n✝ + 1)) (x✝ + y✝).verschiebungFun =
    (ghostComponent (n✝ + 1)) (x✝.verschiebungFun + y✝.verschiebungFun)

Tactic:
<;>

Goal state after:
case refine_3.zero
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (ghostComponent 0) (x✝ + y✝).verschiebungFun = (ghostComponent 0) (x✝.verschiebungFun + y✝.verschiebungFun)

case refine_3.succ
p : ℕ
S : Type u_2
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
R : Type u_1
R._inst : CommRing R
x✝ y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ (ghostComponent (n✝ + 1)) (x✝ + y✝).verschiebungFun =
    (ghostComponent (n✝ + 1)) (x✝.verschiebungFun + y✝.verschiebungFun)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case «0»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ ![x✝.coeff, x✝.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2 =
    (aeval x✝.coeff) (![X, X] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2)

pp: case «1»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ ![x✝.coeff, x✝.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2 =
    (aeval x✝.coeff) (![X, X] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2)

Tactic:
<;>

Goal state after:
case «0»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ ![x✝.coeff, x✝.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2 =
    (aeval x✝.coeff) (![X, X] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2)

case «1»
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
⊢ ![x✝.coeff, x✝.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2 =
    (aeval x✝.coeff) (![X, X] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2)
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ (ghostComponent 0) (verschiebung (x * frobenius y)) = (ghostComponent 0) (verschiebung x * y)

pp: case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
n✝ : ℕ
⊢ (ghostComponent (n✝ + 1)) (verschiebung (x * frobenius y)) = (ghostComponent (n✝ + 1)) (verschiebung x * y)

Tactic:
<;>

Goal state after:
case refine_3.zero
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
⊢ (ghostComponent 0) (verschiebung (x * frobenius y)) = (ghostComponent 0) (verschiebung x * y)

case refine_3.succ
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung (x * frobenius y)
this : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y
R : Type u_1
R._inst : CommRing R
x y : 𝕎 R
n✝ : ℕ
⊢ (ghostComponent (n✝ + 1)) (verschiebung (x * frobenius y)) = (ghostComponent (n✝ + 1)) (verschiebung x * 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 : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) r = 0

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Goal state after:
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 : ℕ
r : O
h : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
hp : ↑p ∣ r
⊢ ↑p ∣ r
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 : ℕ
hp : Fact (Nat.Prime p)
x y : ModP O p
hx : x ^ p ≠ 0
hy : y ^ p ≠ 0
⊢ x * y ≠ 0

Tactic:
by
  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
  obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
  have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos)
  rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_mul]
  rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_pow] at hx hy
  rw [← v_p_lt_val hv] at hx hy ⊢
  rw [map_pow, v.map_pow, ← rpow_lt_rpow_iff h1p, ← rpow_natCast, ← rpow_mul,
    mul_one_div_cancel (Nat.cast_ne_zero.2 hp.1.ne_zero : (p : ℝ) ≠ 0), rpow_one] at hx hy
  rw [map_mul, v.map_mul]; refine lt_of_le_of_lt ?_ (mul_lt_mul'' hx hy zero_le zero_le)
  by_cases hvp : v p = 0
  · rw [hvp]; exact zero_le
  replace hvp := zero_lt_iff.2 hvp
  conv_lhs => rw [← rpow_one (v p)]
  rw [← rpow_add (ne_of_gt hvp)]
  refine rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_
  rw [← add_div, div_le_one (Nat.cast_pos.2 hp.1.pos : 0 < (p : ℝ))]; exact mod_cast hp.1.two_le

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

Goal state before:
pp: case pos
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ x.coeff n = (aeval x.coeff) (X n)

pp: case neg
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ 0 = (aeval x.coeff) 0

Tactic:
<;>

Goal state after:
case pos
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : P n
⊢ x.coeff n = (aeval x.coeff) (X n)

case neg
p : ℕ
R : Type u_1
inst✝ : CommRing R
P : ℕ → Prop
x : 𝕎 R
n : ℕ
hi : ¬P n
⊢ 0 = (aeval x.coeff) 0
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case «0»
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
n k : ℕ
⊢ g (![x.coeff, y.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2

pp: case «1»
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
n k : ℕ
⊢ g (![x.coeff, y.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2

Tactic:
<;>

Goal state after:
case «0»
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
n k : ℕ
⊢ g (![x.coeff, y.coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] ((fun i ↦ i) ⟨0, ⋯⟩, k).1 ((fun i ↦ i) ⟨0, ⋯⟩, k).2

case «1»
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
n k : ℕ
⊢ g (![x.coeff, y.coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] ((fun i ↦ i) ⟨1, ⋯⟩, k).1 ((fun i ↦ i) ⟨1, ⋯⟩, k).2
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ((teichmuller p) 0).coeff 0 = coeff 0 0

pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = coeff 0 (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ ((teichmuller p) 0).coeff 0 = coeff 0 0

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = coeff 0 (n✝ + 1)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 1 = 1

pp: case refine_2
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (x y : S), liftFun f (x * y) = liftFun f x * liftFun f y

pp: case refine_3
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 0 = 0

pp: case refine_4
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (x y : S), liftFun f (x + y) = liftFun f x + liftFun f y

Tactic:
<;>

Goal state after:
case refine_1
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 1 = 1

case refine_2
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (x y : S), liftFun f (x * y) = liftFun f x * liftFun f y

case refine_3
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ liftFun f 0 = 0

case refine_4
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ ∀ (x y : S), liftFun f (x + y) = liftFun f x + liftFun f 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 : PreTilt O p
⊢ (val K v O hv p) f = 0 ↔ f = 0

Tactic:
by_cases hf0 : f = 0

Goal state after:
case pos
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 : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

case neg
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 : PreTilt O p
hf0 : ¬f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
f h : R⟦X⟧
g : R[X]
distinguish : g.IsDistinguishedAt I
notMem : PowerSeries.constantCoeff h ∉ I
eq : f = ↑g * h
⊢ ↑g.natDegree = ((PowerSeries.map (Ideal.Quotient.mk I)) f).order

Tactic:
by
  rw [natDegree, distinguish.degree_eq_coe_lift_order_map f h notMem eq]
  exact ENat.natCast_lift _ <| order_finite_iff_ne_zero.2 <|
    distinguish.map_ne_zero_of_eq_mul f h notMem eq

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

Goal state before:
pp: case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ Field K

pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ CharP K p

pp: case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ Infinite K

Tactic:
<;>

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ Field K

case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ CharP K p

case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])).comp C
this✝ : CharP K p
this : Infinite K
⊢ Infinite K
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case «0»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 0 < 3
⊢ z ^ 0 = 1 ∨ z ^ 0 = z ∨ z ^ 0 = z ^ 2

pp: case «1»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 1 < 3
⊢ z ^ 1 = 1 ∨ z ^ 1 = z ∨ z ^ 1 = z ^ 2

pp: case «2»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 2 < 3
⊢ z ^ 2 = 1 ∨ z ^ 2 = z ∨ z ^ 2 = z ^ 2

Tactic:
<;>

Goal state after:
case «0»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 0 < 3
⊢ z ^ 0 = 1 ∨ z ^ 0 = z ∨ z ^ 0 = z ^ 2

case «1»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 1 < 3
⊢ z ^ 1 = 1 ∨ z ^ 1 = z ∨ z ^ 1 = z ^ 2

case «2»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 2 < 3
⊢ z ^ 2 = 1 ∨ z ^ 2 = z ∨ z ^ 2 = z ^ 2
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case a.e_a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ ↑((x + n)! / x !) = ↑(n ! * (x + n)! / (x ! * n !))

pp: case a.e_a.H
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ x ! * n ! ∣ (x + n)!

Tactic:
· rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]

Goal state after:
case a.e_a.H
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ x ! * n ! ∣ (x + n)!
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2}
⊢ (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2)

Tactic:
show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp

Goal state after:
T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (C ((algebraMap T S) a) * X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c)).roots = {x1, x2}
⊢ (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2)
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2}
⊢ (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Tactic:
show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp

Goal state after:
T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
haroots : (C ((algebraMap T S) a) * X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c)).roots = {x1, x2}
⊢ (algebraMap T S) c = (algebraMap T S) a * x1 * x2
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2} ↔
    (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2) ∧ (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Tactic:
show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp

Goal state after:
T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (C ((algebraMap T S) a) * X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c)).roots = {x1, x2} ↔
    (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2) ∧ (algebraMap T S) c = (algebraMap T S) a * x1 * x2
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝² : CommRing T
inst✝¹ : Field S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (map (algebraMap T S) (C a * X ^ 2 + C b * X + C c)).roots = {x1, x2} ↔
    x1 + x2 = -(algebraMap T S) b / (algebraMap T S) a ∧ x1 * x2 = (algebraMap T S) c / (algebraMap T S) a

Tactic:
show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp

Goal state after:
T : Type u_2
S : Type u_3
inst✝² : CommRing T
inst✝¹ : Field S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (C ((algebraMap T S) a) * X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c)).roots = {x1, x2} ↔
    x1 + x2 = -(algebraMap T S) b / (algebraMap T S) a ∧ x1 * x2 = (algebraMap T S) c / (algebraMap T S) a
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
f : R⟦X⟧
⊢ (expand p hp) f = subst (X ^ p) f

Tactic:
simp [expand, MvPowerSeries.expand, subst, X]

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

Goal state before:
pp: case pos
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
n : ℕ
h✝ : n = 0
⊢ f 0 = 0

pp: case neg
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
n : ℕ
h✝ : ¬n = 0
⊢ f ((algebraMap ℚ A) ((-1) ^ (n + 1) / ↑n)) = (algebraMap ℚ A') ((-1) ^ (n + 1) / ↑n)

Tactic:
<;>

Goal state after:
case pos
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
n : ℕ
h✝ : n = 0
⊢ f 0 = 0

case neg
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
n : ℕ
h✝ : ¬n = 0
⊢ f ((algebraMap ℚ A) ((-1) ^ (n + 1) / ↑n)) = (algebraMap ℚ A') ((-1) ^ (n + 1) / ↑n)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
⊢ -f + f = 0

Tactic:
by
    ext S _ _ m
    simp only [add_def_apply, neg_def, Pi.smul_apply, zero_def, Pi.zero_apply]
    nth_rewrite 2 [← _root_.one_smul (M := R) (b := f.toFun' S m)]
    rw [← _root_.add_smul]
    simp only [neg_add_cancel, _root_.zero_smul]

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
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'
⊢ (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:
obtain ⟨B, hAB, hA'B, ⟨t, hB⟩, h⟩ :=
    TensorProduct.Algebra.eq_of_fg_of_subtype_eq' (R := R) uFG u'FG huu'

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 : Algebra.adjoin R ↑t = B
⊢ (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')