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
x : 𝕎 R
n m : ℕ
h : m < n
⊢ ((⇑verschiebung)^[n] x).coeff m = 0

Tactic:
induction n generalizing m with
  | zero => contradiction
  | succ n ih =>
    rw [iterate_succ_apply']
    cases m with
    | zero => exact verschiebung_coeff_zero _
    | succ m' =>
      rw [verschiebung_coeff_succ, ih]
      simpa using h

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ghost_calc _ _; ghost_simp

Goal state after:
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
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval x.coeff) (frobeniusPoly p n) = x.coeff n ^ p

Tactic:
calc
    aeval (fun k => x.coeff k) (frobeniusPoly p n) =
        aeval (fun k => x.coeff k)
          (MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n)) := ?_
    _ = aeval (fun k => x.coeff k) (X n ^ p : MvPolynomial ℕ (ZMod p)) := ?_
    _ = x.coeff n ^ p := ?_

Goal state after:
case calc_1
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k ↦ x.coeff k) (frobeniusPoly p n) =
    (aeval fun k ↦ x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n))

case calc_2
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k ↦ x.coeff k) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n)) =
    (aeval fun k ↦ x.coeff k) (X n ^ p)

case calc_3
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ (aeval fun k ↦ x.coeff k) (X n ^ p) = x.coeff n ^ 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
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ x * ↑p ^ n * ↑p = x * (↑p ^ n * ↑p)

Tactic:
mul_assoc

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ x * (↑p ^ n * ↑p) = x * (↑p ^ n * ↑p)
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
f : R →+* S
r : R
⊢ (map f) (teichmullerFun p r) = teichmullerFun p (f r)

Tactic:
by
  ext n; cases n
  · rfl
  · exact f.map_zero

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

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

Tactic:
split_ifs with hn

Goal state after:
case pos
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
n : ℕ
hn : P n
⊢ x.coeff n = x.coeff n

case neg
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
n : ℕ
hn : ¬P n
⊢ 0 = x.coeff n
Module: Mathlib.RingTheory.WittVector.InitTail

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

Tactic:
split_ifs with hn

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

case neg
p n✝ : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
n : ℕ
hn : ¬P n
⊢ y.coeff n = y.coeff n
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case empty
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ ∅ ∧ (x r).coeff n ≠ 0}
n : ℕ
⊢ (∑ s ∈ ∅, x s).coeff n = ∑ s ∈ ∅, (x s).coeff n

Tactic:
| empty =>

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ x.coeff i = ∑ s ≤ n, ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ s) (x.coeff s)) * ↑p ^ s).coeff i

Tactic:
Finset.sum_eq_add_sum_sdiff_singleton_of_mem (Finset.mem_Iic.mpr (Nat.lt_succ_iff.mp hi))

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
⊢ x.coeff i =
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i +
      ∑ x_1 ∈ Finset.Iic n \ {i},
        ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: n : ℕ
x : ℝ
⊢ deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))

Tactic:
mul_assoc

Goal state after:
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ dickson 1 1 p = X ^ p

Tactic:
have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1 := by
    simp only [ZMod.castHom_apply, ZMod.cast_one']

Goal state after:
R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = (ZMod.castHom ⋯ R) 1
⊢ dickson 1 1 p = X ^ p
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

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

Tactic:
mul_assoc

Goal state after:
case a
n x : ℕ
a✝ : x ∈ range (n + 1)
⊢ C ((-1) ^ x * ↑(n.choose x)) * ↑((n + x)! / x !) = C ((-1) ^ x * ↑(n.choose x)) * (C ↑((n + x).choose n) * ↑n !)
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).ncard ≤ (↑(roots 0).toFinset).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
roots_zero,

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : (f.rootSet S).ncard ≤ (↑(Multiset.toFinset 0)).ncard + 1
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
hp : Subsingleton ↑(f.rootSet S)
g : G
hg : g ∈ Ideal.inertia G p
hfp : map (algebraMap R (S ⧸ p)) f = 0
⊢ (MulAction.toPermHom G ↑(f.rootSet S)) g = 1 ∨ ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
exact Or.inl (Subsingleton.elim _ _)

Goal state after:
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) u) =
    (lTensor M (↑Q).subtype) u

Tactic:
suffices (Submodule.FG.lTensor.directLimit R M N).toLinearMap.comp
      (Module.DirectLimit.of R {Q : Submodule R N // Q.FG} (fun Q ↦ M ⊗[R] Q.val)
        (fun _ _ hPQ ↦ lTensor M (inclusion hPQ)) Q)
      = lTensor M (Submodule.subtype Q.val) by
    exact DFunLike.congr_fun this u
  ext p n
  simp [Submodule.FG.lTensor.directLimit, Submodule.FG.directLimit]

Goal state after:
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
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h✝ :
  (rTensor N (P ⊔ P').subtype) ((rTensor N (inclusion ⋯)) t) =
    (rTensor N (P ⊔ P').subtype) ((rTensor N (inclusion ⋯)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (rTensor N (inclusion hQ_le)) ((rTensor N (inclusion ⋯)) t) =
    (rTensor N (inclusion hQ_le)) ((rTensor N (inclusion ⋯)) t')
⊢ ∃ Q, ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hP'Q)) t'

Tactic:
use Q, le_trans le_sup_left hQ_le, le_trans le_sup_right hQ_le, hQ

Goal state after:
case right
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
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h✝ :
  (rTensor N (P ⊔ P').subtype) ((rTensor N (inclusion ⋯)) t) =
    (rTensor N (P ⊔ P').subtype) ((rTensor N (inclusion ⋯)) t')
Q : Submodule R M
hQ_le : P ⊔ P' ≤ Q
hQ : Q.FG
h :
  (rTensor N (inclusion hQ_le)) ((rTensor N (inclusion ⋯)) t) =
    (rTensor N (inclusion hQ_le)) ((rTensor N (inclusion ⋯)) t')
⊢ (rTensor N (inclusion ⋯)) t = (rTensor N (inclusion ⋯)) 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
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
⊢ (ψ.range.val.comp h').comp ↑(quotientKerEquivRangeₐ φ) =
    (((ψ.range.val.comp ↑(quotientKerEquivRangeₐ ψ)).comp ↑(quotientKerEquivRangeₐ ψ).symm).comp h').comp
      ↑(quotientKerEquivRangeₐ φ)

Tactic:
simp [AlgHom.comp_assoc]

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
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
⊢ ∃ s, (rTensor M φ.toLinearMap) s = t

Tactic:
by
    obtain ⟨p, hp⟩ := h_surj ((Subalgebra.inclusion hφ).toLinearMap.rTensor M u)
    use p
    rw [← hu, ← Subalgebra.val_comp_inclusion hφ, comp_toLinearMap, rTensor_comp,
      LinearMap.comp_apply, ← hp, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]
    simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : p = q
ht1 : (maximalIdeal R).height ≤ p.height
⊢ span (⇑(algebraMap R (Localization.AtPrime p)) '' Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)

Tactic:
IsScalarTower.algebraMap_eq R R[X] (Localization.AtPrime p),

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : p = q
ht1 : (maximalIdeal R).height ≤ p.height
⊢ span
      (⇑((algebraMap R[X] (Localization.AtPrime p)).comp (algebraMap R R[X])) ''
        Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)
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
N : Submodule R M
inst✝¹ : IsSimpleModule R ↥N
s : Set (Submodule R M)
inst✝ : IsSemisimpleModule R M
hs : sSup s = ⊤
this : Nontrivial ↥N
w✝ : Submodule R M
compl : IsCompl N w✝
m : Submodule R M
hm : m ∈ s
ne : N.projectionOnto w✝ compl ∘ₗ m.subtype ≠ 0
S : Submodule R ↥m
e : ↥N ≃ₗ[R] ↥S
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
exact ⟨m, hm, _, m.map_subtype_le S, ⟨e.trans (S.equivMapOfInjective _ m.subtype_injective)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Nontrivial M ∧
    ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
hM1 : Nontrivial M
hM2 : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
p : Submodule R M
h : Function.Injective ⇑p.mkQ
x : M
hx : x ∈ p
⊢ p.mkQ x = p.mkQ 0

Tactic:
by simp [hx]

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

Goal state before:
pp: case inr.refine_2
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
· cases topOrderOrNoTopOrder α with
    | inl => use ⊤; simpa using! hf.strictMono.id_le ⊤
    | inr h =>
      rw [noTopOrder_iff_noMaxOrder] at h
      suffices BddAbove (.range fun n ↦ f^[n] a) from
        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
      refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
      simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a)

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ f (lfpApprox f x a) ≤ x ⊔ ⨆ b_1, ⨆ (_ : b_1 < b), f (lfpApprox f x b_1)

Tactic:
exact le_sup_of_le_right <| le_iSup₂_of_le a h le_rfl

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

Goal state before:
pp: case refine_2.inr.inr
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)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF.ne_zero ho, map_cons, pairwise_cons]

Goal state after:
case refine_2.inr.inr
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)))
hb : 1 < b
hbo : b ≤ o
⊢ (∀ a' ∈ map Prod.fst (CNF b (o % b ^ log b o)), (log b o, o / b ^ log b o).1 > a') ∧
    List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ Decidable (a ∈ b.cons' l₂)

Tactic:
by
      haveI :=
        have : sizeOf (⟨_, b⟩ : Lists α) < 1 + 1 + sizeOf b + sizeOf l₂ := by simp [sizeof_pos]
        Equiv.decidable a ⟨_, b⟩
      haveI :=
        have :
          SizeOf.sizeOf a + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf a + SizeOf.sizeOf (Lists'.cons' b l₂) := by
          decreasing_tactic
        mem.decidable a l₂
      refine decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) ?_
      rw [← Lists'.mem_cons]; rfl

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

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

Tactic:
revert h

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h : Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
revert h

Goal state after:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
⊢ (match Ordering.eq, e₁, e₂ with
    | Ordering.lt, a, b => a < b
    | Ordering.eq, a, b => a = b
    | Ordering.gt, a, b => b < a) →
    (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
      (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
intro IHe; dsimp at IHe; subst IHe
      unfold _root_.cmp; cases nh : cmpUsing (· < ·) (n₁ : ℕ) n₂ <;>
      rw [cmpUsing, ite_eq_iff, not_lt] at nh
      case lt =>
        rcases nh with nh | nh
        · exact oadd_lt_oadd_2 h₁ nh.left
        · rw [ite_eq_iff] at nh; rcases nh.right with nh | nh <;> cases nh <;> contradiction
      case gt =>
        rcases nh with nh | nh
        · cases nh; contradiction
        · obtain ⟨_, nh⟩ := nh
          rw [ite_eq_iff] at nh; rcases nh with nh | nh
          · exact oadd_lt_oadd_2 h₂ nh.left
          · cases nh; contradiction
      rcases nh with nh | nh
      · cases nh; contradiction
      obtain ⟨nhl, nhr⟩ := nh
      rw [ite_eq_iff] at nhr
      rcases nhr with nhr | nhr
      · cases nhr; contradiction
      obtain rfl := Subtype.ext (nhl.eq_of_not_lt nhr.1)
      have IHa := @cmp_compares _ _ h₁.snd h₂.snd
      revert IHa; cases cmp a₁ a₂ <;> intro IHa <;> dsimp at IHa
      case lt => exact oadd_lt_oadd_3 IHa
      case gt => exact oadd_lt_oadd_3 IHa
      subst IHa; exact rfl

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

Goal state before:
pp: a : Ordinal.{u}
h : a < ω ^ a
⊢ a.invVeblen₁ = 0

Tactic:
rwa [← nonpos_iff_eq_zero, ← lt_veblen_iff_invVeblen₁_le, veblen_zero]

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

Goal state before:
pp: x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ (⋂₀ x) x_1

Tactic:
sInter_apply

Goal state after:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ mk (Quotient.out x) ∈ mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)) ↔
    mk (Quotient.out x) ∈ s

Tactic:
mk_mem_iff,

Goal state after:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x ↦ Quotient.out ↑((equivShrink ↑s).symm x)) ↔
    mk (Quotient.out x) ∈ s
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : ↥x),
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a b →
      Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b c → Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a c
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
⊢ y ∈ w

Tactic:
have hzx := h₁.mem_trans hzw hwx

Goal state after:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : ↥x),
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a b →
      Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b c → Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a c
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
hzx : z ∈ x
⊢ y ∈ w
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toPSet.Type = o.ToType

Tactic:
by
  rw [toPSet]
  rfl

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

Goal state before:
pp: case refine_1
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ∈ o.toZFSet
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ o.toZFSet

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx

Goal state after:
case refine_1
o : Ordinal.{u_1}
y : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
hy : y ∈ a.toZFSet
⊢ y ∈ o.toZFSet
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
z y x : ZFSet.{u_1}
hz : z ∈ y
hy : y ∈ x
hx : x ∈ o.toZFSet
⊢ z ∈ x

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx

Goal state after:
case refine_2
o : Ordinal.{u_1}
z y : ZFSet.{u_1}
hz : z ∈ y
a : Ordinal.{u_1}
ha : a < o
hy : y ∈ a.toZFSet
hx : a.toZFSet ∈ o.toZFSet
⊢ z ∈ a.toZFSet
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 + 1)) + a₁.repr = ω ^ e₁.repr * ↑↑n₁ * (↑x + 1) + a₁.repr

Tactic:
mul_assoc

Goal state after:
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 + 1)) + a₁.repr = ω ^ e₁.repr * (↑↑n₁ * (↑x + 1)) + a₁.repr