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

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (trunc' R (p • n)) ((map (frobenius R p)) ((expand p hp) f)) = (trunc' R (p • n)) (f ^ p)

Tactic:
have : (((trunc' R (p • n) f).expand p).map (frobenius R p)).toMvPowerSeries =
      MvPowerSeries.map (frobenius R p) ((trunc' R (p • n) f).expand p) := by
      simp only [MvPolynomial.map_expand, ← expand_eq_expand p hp, map_expand]
      congr
    rw [trunc'_map, trunc'_expand, ← trunc'_trunc'_pow (Nat.one_le_iff_ne_zero.mpr
      (expChar_ne_zero R p)), ← MvPolynomial.coe_pow p, ← MvPolynomial.map_frobenius_expand, this,
        trunc'_map, trunc'_expand_trunc' p hp (le_self_nsmul zero_le hp)]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) ^ p =
    (map (iterateFrobenius R p (k + 1))) ((expand (p ^ (k + 1)) ⋯) f)

Tactic:
simp_rw [← map_frobenius_expand p hp, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

Goal state after:
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_2
R : Type u_3
inst✝² : Field k
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj : Function.Injective ⇑g
int : g.IsIntegral
h : algebraMap k R = g.comp (algebraMap k (MvPolynomial (Fin s) k))
⊢ ∃ s g, Function.Injective ⇑g ∧ g.Finite

Tactic:
exact ⟨s, g, inj, int.to_finite
    (h ▸ RingHom.finiteType_algebraMap.mpr fin).of_comp_finiteType⟩

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

Goal state before:
pp: case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun b ↦ (rename fun i ↦ (b, i)) ((expand p) (W_ ℤ n))) Φ =
    (bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
⊢ C ↑(p ^ (n + 1)) ∣
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℤ (n + 1))) Φ -
      ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)

Tactic:
apply_fun map (Int.castRingHom (ZMod (p ^ (n + 1)))) at key

Goal state after:
case succ
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun b ↦ (rename fun i ↦ (b, i)) ((expand p) (W_ ℤ n))) Φ) =
    (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i ↦ (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))
⊢ C ↑(p ^ (n + 1)) ∣
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℤ (n + 1))) Φ -
      ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)
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
⊢ v 1 = 1

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
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) 1 ≠ 0

Tactic:
v.map_one

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 : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ 1 = 1

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
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) 1 ≠ 0
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
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
set z := mk p fun n => if P n then x.coeff n else y.coeff n

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
⊢ (x + y).coeff n = x.coeff n + y.coeff n
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p : ℕ
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₁
g : S →+* 𝕎 R
g_compat : ∀ (k : ℕ), (truncate k).comp g = f k
x : S
i : ℕ
⊢ (lift f f_compat) x - g x ∈ RingHom.ker (truncate i)

Tactic:
simp only [RingHom.mem_ker, g_compat, ← RingHom.comp_apply, truncate_comp_lift, map_sub, sub_self]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ (fun x ↦ (X + C 1) * x) (trinomial b) = (fun x ↦ (X + C 1) * x) (trinomial c)

Tactic:
simp_rw [ht, eq]

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

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (algebraMap ℤ ℂ) (-↑1) * z ^ 0 + (algebraMap ℤ ℂ) (-↑1) * z ^ 1 + (algebraMap ℤ ℂ) ↑1 * z ^ n = 0
h2 : (algebraMap ℤ ℂ) ↑1 * z ^ 0 + (algebraMap ℤ ℂ) (-↑1) * z ^ (n - 1 + 0) + (algebraMap ℤ ℂ) (-↑1) * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0

Tactic:
Units.val_one,

Goal state after:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (algebraMap ℤ ℂ) (-1) * z ^ 0 + (algebraMap ℤ ℂ) (-1) * z ^ 1 + (algebraMap ℤ ℂ) 1 * z ^ n = 0
h2 : (algebraMap ℤ ℂ) 1 * z ^ 0 + (algebraMap ℤ ℂ) (-1) * z ^ (n - 1 + 0) + (algebraMap ℤ ℂ) (-1) * z ^ n = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 = z + 1 ∧ z + 1 + z ^ 2 = 0

Tactic:
exact ⟨rfl, by linear_combination -h2⟩

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n : ℕ
⊢ (coeff n) ((expand p hp) φ) = if p ∣ n then (coeff (n / p)) φ else 0

Tactic:
by
  split_ifs with h
  · obtain ⟨q, hq⟩ := h
    rw [hq, coeff_expand_mul, Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)]
  exact coeff_expand_of_not_dvd p hp _ h

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
f : M →ₚₗ[R] N
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = f.toFun' S (1 ⊗ₜ[R] x)

Tactic:
ground_apply

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
f : M →ₚₗ[R] N
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] (TensorProduct.lid R N) (f.toFun' R (1 ⊗ₜ[R] x)) = f.toFun' S (1 ⊗ₜ[R] x)
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (1 + X).logOf = log A

Tactic:
by
  rw [logOf_eq, add_sub_cancel_left, X_subst]

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

Goal state before:
pp: 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
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
⊢ u ∈ (rTensor N (Algebra.adjoin R ↑s).val.toLinearMap).range

Tactic:
← subtype_comp_inclusion P _ this,

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
s : Finset S
hs : span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
hu : u ∈ (rTensor N ((Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ inclusion this)).range
⊢ u ∈ (rTensor N (Algebra.adjoin R ↑s).val.toLinearMap).range
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
P : Type u_3
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
Q : Type u_4
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
f✝ : M →ₚₗ[R] N
g✝ : N →ₚₗ[R] P
h : P →ₚₗ[R] Q
g : N →ₚₗ[R] P
f : M →ₚₗ[R] N
S✝ : Type u
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
S'✝ : Type u
inst✝¹ : CommSemiring S'✝
inst✝ : Algebra R S'✝
φ : S✝ →ₐ[R] S'✝
⊢ ⇑(rTensor P φ.toLinearMap) ∘ g.toFun' S✝ ∘ f.toFun' S✝ = (g.toFun' S'✝ ∘ f.toFun' S'✝) ∘ ⇑(rTensor M φ.toLinearMap)

Tactic:
ext; simp only [Function.comp_apply, isCompat_apply']

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 0 < radical z

Tactic:
rw [← radical_natAbs_eq_radical, natCast_pos]

Goal state after:
z : ℤ
⊢ 0 < radical z.natAbs
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
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
q : B ⊗[R] M
ψ : B →ₐ[R] S
h : φ.range ≤ ψ.range
hpq :
  (rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ ψ.range.val.comp (Subalgebra.inclusion h) = (AlgHom.id R S).comp φ.range.val

Tactic:
ext x; simp

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
⊢ (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 huu' : rTensor M (Subalgebra.val _).toLinearMap u =
    rTensor M (Subalgebra.val _).toLinearMap u' := by
    simp only [π] at h
    simp only [hu, hu', ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap,
      val_comp_rangeRestrict, h]

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'
⊢ (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.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
⊢ g.degree = ↑((map (Ideal.Quotient.mk I)) ↑g).order.toNat

Tactic:
convert!
        H.degree_eq_coe_lift_order_map g 1 (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one])
          (by simp)

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
⊢ ((map (Ideal.Quotient.mk I)) ↑g).order.toNat = ((map (Ideal.Quotient.mk I)) ↑g).order.lift ⋯
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝¹ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝ : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this : pS.IsPrime
⊢ p = comap (algebraMap R[X] S) pS

Tactic:
exact (IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj).symm

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

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularRing R
ι : Type u_2
inst✝ : Finite ι
α✝ β✝ : Type u_2
e : α✝ ≃ β✝
H : IsRegularRing (MvPolynomial α✝ R)
⊢ IsRegularRing (MvPolynomial β✝ R)

Tactic:
exact IsRegularRing.of_ringEquiv (renameEquiv _ e).toRingEquiv

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, PrimeSpectrum.comap C '' (zeroLocus {↑i})ᶜ)

Tactic:
← imageOfDf_eq_comap_C_compl_zeroLocus

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, imageOfDf ↑i)
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
⊢ x ∈ I • f.ker

Tactic:
rcases (Submodule.ext_iff.mp (I.subtype_rTensor_range M) x).mpr hx.2 with ⟨y, hy⟩

Goal state after:
case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
⊢ x ∈ I • f.ker
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ a = ↑p ^ m * b

Tactic:
simp_rw [← mul_left_iterate (p : 𝕎 k) m]
    convert! hcm using 2
    ext1 x
    rw [mul_comm, ← WittVector.verschiebung_frobenius x]; rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ (X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree < (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree

Tactic:
rw [this, degree_mul, degree_C, degree_X, add_zero]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 1 < ↑p

p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n

Tactic:
enter [1, 1, 2, 2]
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    ↑p ^ (n + 1) * X (1, n + 1)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inl
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

pp: case inr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
· by_cases hp : x <+: z
    · obtain ⟨z, rfl⟩ := hp
      simp [pullSub, List.take_add]
    · constructor <;> intro ⟨h, _⟩ <;>
        [skip; replace h := by simpa [List.take_take] using h.take x.length] <;>
        cases hp <| List.prefix_iff_eq_take.mpr (h.eq_of_length (by simpa)).symm

Goal state after:
case inr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
hb' : b ≠ ⊥
⊢ (log b (b ^ e * x + y), (b ^ e * x + y) / b ^ log b (b ^ e * x + y)) ::
      CNF b ((b ^ e * x + y) % b ^ log b (b ^ e * x + y)) =
    (e, x) :: CNF b y

Tactic:
rw [log_opow_mul_add hb hx hy, log_eq_zero hxb, add_zero,
      mul_add_div _ (opow_ne_zero _ hb'), Ordinal.div_eq_zero_of_lt hy, add_zero,
      mul_add_mod_self, mod_eq_of_lt hy]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList

Tactic:
exact ofList_subset (List.Subset.refl _)

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

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → x.2 < b

Tactic:
refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o

Goal state after:
case refine_1
b o : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → x.2 < b

case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o

Goal state after:
case refine_1
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b 0))

case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
hpos : 0 < o
hmem : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ x ∈ fixedPoints ⇑f

Tactic:
by simpa [lfpApprox_zero] using hmem

Goal state after:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this✝ : Nonempty α
this : Nonempty β
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this✝ : Nonempty α
this : Nonempty β
⊢ IsClosed (Iic (sSup (f ⁻¹' Iic b)))
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case neg
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
e' : Ordinal.{u_1}
he' : e' ∉ f.support
⊢ f e' < b

Tactic:
· rw [notMem_support_iff.1 he']
        exact hb.pos

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

Goal state before:
pp: x y : ZFSet.{u}
h : x ∉ y
⊢ (insert x y).card = y.card + 1

Tactic:
rw [← lift_inj.{u, u + 1}]
  simpa [← cardinalMk_coe_sort] using! mk_insert (SetLike.mem_coe.not.2 h)

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

Goal state before:
pp: case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝¹
h : succ (A✝¹ a).rank = x✝
⊢ ∃ y, succ (A✝ y).rank = x✝

Tactic:
obtain ⟨b, h'⟩ := αβ a

Goal state after:
case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝¹
h : succ (A✝¹ a).rank = x✝
b : α✝
h' : (A✝¹ a).Equiv (A✝ b)
⊢ ∃ y, succ (A✝ y).rank = x✝
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a < veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

Tactic:
rw [← cmp_eq_lt_iff, cmp_veblenWith hf]
  aesop (add simp lt_asymm)

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

Goal state before:
pp: o : ONote
b : Ordinal.{0}
x✝ : NFBelow 0 b
h₂ : o.NF
⊢ (0 - o).NFBelow b

Tactic:
cases o <;> exact NFBelow.zero

Goal state after: