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

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ (aeval fun a ↦ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] a.1 a.2) (χ n) =
    (aeval fun i ↦
        (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
          (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] i.1 i.2))
      (χ n)

Tactic:
apply eval₂Hom_congr rfl _ rfl

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n : ℕ
⊢ (fun a ↦ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] a.1 a.2) = fun i ↦
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] i.1 i.2)
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
h : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
f g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
χ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hh : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (h x y).coeff = fun n ↦ peval (χ n) ![x.coeff, y.coeff]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n✝ n : ℕ
⊢ ![fun n ↦ (aeval x✝.coeff) (φ n), fun n ↦ (aeval y✝.coeff) (ψ n)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
      ((fun i ↦ i) ⟨0, ⋯⟩, n).2 =
    (aeval fun a ↦ ![x✝.coeff, y✝.coeff] a.1 a.2)
      (![fun k ↦ (rename (Prod.mk 0)) (φ k), fun k ↦ (rename (Prod.mk 1)) (ψ k)] ((fun i ↦ i) ⟨0, ⋯⟩, n).1
        ((fun i ↦ i) ⟨0, ⋯⟩, n).2)

Tactic:
simp [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp_def]

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

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

Tactic:
simp [aeval_eq_eval₂Hom, eval₂Hom_rename, Function.comp_def]

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

Goal state before:
pp: 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 : ℕ
⊢ (aeval fun a ↦ ![x✝.coeff, x✝.coeff] a.1 a.2) (φ n) = (aeval fun i ↦ (aeval x✝.coeff) (![X, X] i.1 i.2)) (φ n)

Tactic:
apply eval₂Hom_congr rfl _ rfl

Goal state after:
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 : ℕ
⊢ (fun a ↦ ![x✝.coeff, x✝.coeff] a.1 a.2) = fun i ↦ (aeval x✝.coeff) (![X, X] i.1 i.2)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ peval (wittNeg p n) ![x✝.coeff] = (eval₂Hom (algebraMap ℤ R✝) (x✝.coeff ∘ Prod.snd)) (wittNeg p n)

Tactic:
apply eval₂Hom_congr rfl _ rfl

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ uncurry ![x✝.coeff] = x✝.coeff ∘ Prod.snd
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
⊢ frobenius (verschiebung x) = x * ↑p

Tactic:
by
  have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) :=
    IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly)
  have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p
  ghost_calc x
  ghost_simp [mul_comm]

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

Goal state before:
pp: case neg
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ¬i = 1
⊢ (↑p).coeff i = 0

Tactic:
simpa only [pow_one] using coeff_p_pow_eq_zero p R hi

Goal state after:
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 : ℕ
x : ModP O p
h : preVal K v O p x = 0
⊢ x = 0

Tactic:
contrapose! h

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 : ℕ
x : ModP O p
h : x ≠ 0
⊢ preVal K v O p x ≠ 0
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
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
hfn : (coeff (Nat.find h + k)) f ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)

Tactic:
induction k with

Goal state after:
case succ
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
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg.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
m n k : ℕ
hm : (Perfection.coeff (ModP O p) p (max (max m n) k)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max (max m n) k)) g ≠ 0
hk : (Perfection.coeff (ModP O p) p (max (max m n) k)) (f + g) ≠ 0
h :
  ModP.preVal K v O p ((coeff (max (max m n) k)) f + (coeff (max (max m n) k)) g) ≤
    ModP.preVal K v O p ((coeff (max (max m n) k)) g)
⊢ ModP.preVal K v O p ((coeff (max (max m n) k)) f + (coeff (max (max m n) k)) g) ^ p ^ max (max m n) k ≤
    max (ModP.preVal K v O p ((coeff (max (max m n) k)) f) ^ p ^ max (max m n) k)
      (ModP.preVal K v O p ((coeff (max (max m n) k)) g) ^ p ^ max (max m n) k)

Tactic:
exact le_max_of_le_right (pow_le_pow_left' h _)

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

Goal state before:
pp: case insert
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this✝ : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
this : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0
⊢ (x a).coeff n + (∑ s ∈ S', x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n

Tactic:
hind n

Goal state after:
case insert
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n : ℕ
this✝ : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
hind : ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
this : ∀ (n : ℕ), (x a).coeff n = 0 ∨ (∑ s ∈ S', x s).coeff n = 0
⊢ (x a).coeff n + ∑ s ∈ S', (x s).coeff n = (x a).coeff n + ∑ s ∈ S', (x s).coeff n
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
hi : Irreducible (Polynomial.map φ f)
⊢ Irreducible f

Tactic:
let R' := R ⧸ nilradical R
  let ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ
    (haveI := RingHom.ker_isPrime φ; nilradical_le_prime (RingHom.ker φ))
  let ι := algebraMap R R'
  rw [show φ = ψ.comp ι from rfl, ← map_map] at hi
  replace hi := hm.map ι |>.irreducible_of_irreducible_map _ _ hi
  refine ⟨fun h ↦ hi.1 <| (mapRingHom ι).isUnit_map h, fun a b h ↦ ?_⟩
  wlog hb : IsUnit (b.map ι) generalizing a b
  · exact (this b a (mul_comm a b ▸ h)
      (hi.2 (by rw [h, Polynomial.map_mul]) |>.resolve_right hb)).symm
  have hn (i : ℕ) (hi : i ≠ 0) : IsNilpotent (b.coeff i) := by
    obtain ⟨_, _, h⟩ := Polynomial.isUnit_iff.1 hb
    simpa only [coeff_map, coeff_C, hi, ite_false, ← RingHom.mem_ker,
      show RingHom.ker ι = nilradical R from Ideal.mk_ker] using! congr(coeff $(h.symm) i)
  refine .inr <| isUnit_of_coeff_isUnit_isNilpotent (isUnit_of_mul_isUnit_right
    (x := a.coeff f.natDegree) <| (IsUnit.neg_iff _).1 ?_) hn
  have hc : f.leadingCoeff = _ := congr(coeff $h f.natDegree)
  rw [hm, coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j ↦ a.coeff i * b.coeff j,
    Finset.sum_range_succ, ← sub_eq_iff_eq_add, Nat.sub_self] at hc
  rw [← add_sub_cancel_left 1 (-(_ * _)), ← sub_eq_add_neg, hc]
  exact IsNilpotent.isUnit_sub_one <| show _ ∈ nilradical R from sum_mem fun i hi ↦
    Ideal.mul_mem_left _ _ <| hn _ <| Nat.sub_ne_zero_of_lt (List.mem_range.1 hi)

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

Goal state before:
pp: n : ℕ
z : ℂ
⊢ ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)

Tactic:
rintro ⟨h1, h2⟩

Goal state after:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ False
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : F k ⊗[R] N
⊢ LinearMap.rTensor N (f h' ∘ₗ f h) = LinearMap.rTensor N (f ⋯)

Tactic:
ext p n

Goal state after:
R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : F k ⊗[R] N
p : F k
n : N
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor N (f h' ∘ₗ f h))) p) n =
    ((AlgebraTensorModule.curry (LinearMap.rTensor N (f ⋯))) p) n
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
P : { P // P.FG }
u : ↥↑P ⊗[R] N
⊢ ↑(directLimit R M N) ∘ₗ
      Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun x x_1 hPQ ↦ rTensor N (inclusion hPQ)) P =
    rTensor N (↑P).subtype

Tactic:
ext p n

Goal state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
P : { P // P.FG }
u : ↥↑P ⊗[R] N
p : ↥↑P
n : N
⊢ ((AlgebraTensorModule.curry
          (↑(directLimit R M N) ∘ₗ
            Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun x x_1 hPQ ↦ rTensor N (inclusion hPQ)) P))
        p)
      n =
    ((AlgebraTensorModule.curry (rTensor N (↑P).subtype)) p) n
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : M ⊗[R] F k
⊢ LinearMap.lTensor M (f h' ∘ₗ f h) = LinearMap.lTensor M (f ⋯)

Tactic:
ext p n

Goal state after:
R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : M ⊗[R] F k
p : M
n : F k
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M (f h' ∘ₗ f h))) p) n =
    ((AlgebraTensorModule.curry (LinearMap.lTensor M (f ⋯))) p) n
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
⊢ ↑(directLimit R M N) ∘ₗ
      Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q =
    lTensor M (↑Q).subtype

Tactic:
ext p n

Goal state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
p : M
n : ↥↑Q
⊢ ((AlgebraTensorModule.curry
          (↑(directLimit R M N) ∘ₗ
            Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q))
        p)
      n =
    ((AlgebraTensorModule.curry (lTensor M (↑Q).subtype)) p) n
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ IsWeierstrassDivisionAt 0 g 0 0 I

Tactic:
by
  constructor
  · rw [Polynomial.degree_zero]
    exact WithBot.bot_lt_coe _
  · simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
kerf : f.ker = x • ⊤
fg : g.ker.FG
y : I →₀ R
hy : y ∈ g.ker
⊢ y ∈ x • ⊤

Tactic:
simp [← kerf, ← hg, LinearMap.mem_ker.mp hy]

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
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
k : ℕ
⊢ ∀ (i : ℕ), (coeff i) q ∈ I ^ k

Tactic:
induction k with

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
h : Subsingleton (QuotSMulTop x ↑M)
⊢ Subsingleton ↑M

Tactic:
contrapose! h

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
h : Nontrivial ↑M
⊢ Nontrivial (QuotSMulTop x ↑M)
Module: Mathlib.RingTheory.RingInvo

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
e f : RingInvo R
h₁ : e.toFun = f.toFun
h₂ : e.invFun = f.invFun
⊢ e = f

Tactic:
rcases e with ⟨⟨tE, _⟩, _⟩; rcases f with ⟨⟨tF, _⟩, _⟩
    cases tE
    cases tF
    congr

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) g ≠ 0
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f.IsWeierstrassDivision g (IsWeierstrassDivisorAt.div ⋯ f) (IsWeierstrassDivisorAt.mod ⋯ f)

Tactic:
exact (IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ Submodule.map p S

Tactic:
rw [← S.range_subtype, ← LinearMap.range_comp, eq, e.symm.range_comp, S'.range_subtype]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Subsingleton α
⊢ moebius (1 * b) = moebius 1 * moebius b

Tactic:
moebius_one,

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Subsingleton α
⊢ moebius (1 * b) = 1 * moebius b
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0

Tactic:
clear hpi

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ↑p ^ i ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.mapDomain (Prod.mk 0) (Finsupp.single x (p ^ (n + 1 - x)))).support ⊆ univ ×ˢ range (n + 1)

pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0

Tactic:
Finsupp.mapDomain_single

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (0, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)

case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.mapDomain (Prod.mk 1) (Finsupp.single x (p ^ (n + 1 - x)))).support ⊆ univ ×ˢ range (n + 1)

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0

Tactic:
Finsupp.mapDomain_single

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ (Finsupp.single (1, x) (p ^ (n + 1 - x))).support ⊆ univ ×ˢ range (n + 1)

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑p ^ x ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rw [polyOfInterest_vars_eq]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars ⊆
    univ ×ˢ range (n + 1)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
⊢ ¬IsStationary s ↔ ∃ t, IsClub t ∧ Disjoint s t

Tactic:
by
  simp [IsStationary, disjoint_iff, not_nonempty_iff_eq_empty]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
h : IsStationary (⋃₀ s)
⊢ ∃ x ∈ s, IsStationary x

Tactic:
contrapose! h

Goal state after:
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
h : ∀ x ∈ s, ¬IsStationary x
⊢ ¬IsStationary (⋃₀ s)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : IsStationary (⋃₀ s)
⊢ ∃ x ∈ s, IsStationary x

Tactic:
contrapose! h

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : ∀ x ∈ s, ¬IsStationary x
⊢ ¬IsStationary (⋃₀ s)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNF.rec b H0 H 0 = H0

Tactic:
CNF.rec,

Goal state after:
C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ (if h : 0 = 0 then ⋯ ▸ H0 else H 0 h (CNF.rec b H0 H (0 % b ^ log b 0))) = H0
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNF.rec b H0 H o = H o ho (CNF.rec b H0 H (o % b ^ log b o))

Tactic:
CNF.rec,

Goal state after:
b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ (if h : o = 0 then ⋯ ▸ H0 else H o h (CNF.rec b H0 H (o % b ^ log b o))) = H o ho (CNF.rec b H0 H (o % b ^ log b o))