mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: 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]
hf : (map (algebraMap R S) f).Splits
inst✝ : MulAction.IsPretransitive G ↑(f.rootSet S)
h : ∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1
hG : ⨆ m, Ideal.inertia G m.asIdeal = ⊤
⊢ Function.Surjective ⇑(MulAction.toPermHom G ↑(f.rootSet S))

Tactic:
by
  classical
  apply surjective_of_isSwap_of_isPretransitive'
      (⋃ m : MaximalSpectrum S, m.asIdeal.inertia G)
  · intro σ hσ
    obtain ⟨m, hm⟩ := Set.mem_iUnion.mp hσ
    exact hf.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia m.asIdeal (h m) σ hm
  · simpa [Subgroup.closure_iUnion]

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
x✝² : CommSemiring S
x✝¹ : Algebra R S
x✝ : S ⊗[R] M
⊢ (0 • f).toFun' S x✝ = toFun' 0 S x✝

Tactic:
simp only [smul_def, _root_.zero_smul, zero_def, Pi.zero_apply]

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 t' : ↥P ⊗[R] N
h✝ :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t =
    (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t'
Q : { P // P.FG }
hPQ : ⟨P, hP⟩ ≤ Q
h : (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'

Tactic:
use Q.val, Subtype.coe_le_coe.mpr hPQ, Q.property

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

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (log A) = log A'

Tactic:
ext n

Goal state after:
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
n : ℕ
⊢ (coeff n) ((map f) (log A)) = (coeff n) (log A')
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: ⊢ largeSchroderSeries = 1 + X * largeSchroderSeries + X * largeSchroderSeries ^ 2

Tactic:
ext n

Goal state after:
n : ℕ
⊢ (coeff n) largeSchroderSeries = (coeff n) (1 + X * largeSchroderSeries + X * largeSchroderSeries ^ 2)
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (d⁄dX A) (log A) = mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n)

Tactic:
ext n

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff n) ((d⁄dX A) (log A)) = (coeff n) (mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n))
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
pp : ∀ p ∈ n.primeFactors, 1 ≤ p
⊢ 1 < radical n ↔ 1 < n

Tactic:
rw [radical_eq_prod_primeFactors, ← @nonempty_primeFactors n, Finset.one_lt_prod_iff_of_one_le pp]

Goal state after:
n : ℕ
pp : ∀ p ∈ n.primeFactors, 1 ≤ p
⊢ (∃ x ∈ n.primeFactors, 1 < x) ↔ n.primeFactors.Nonempty
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ f + f' = g * (q + q') + ↑(r + r')

Tactic:
rw [H.eq_mul_add, H'.eq_mul_add, Polynomial.coe_add]; ring

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
f : A⟦X⟧
inst✝ : IsAdicComplete I A
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I

Tactic:
rcases eq_or_ne I ⊤ with rfl | hI
  · have := ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
    rw [Subsingleton.elim f 0, Subsingleton.elim (H.div 0) 0, Subsingleton.elim (H.mod 0) 0]
    exact g.isWeierstrassDivisionAt_zero _
  constructor
  · exact degree_trunc_lt _ _
  · rw [mod, add_comm, ← sub_eq_iff_eq_add]
    ext i
    rw [Polynomial.coeff_coe, coeff_trunc]
    split_ifs with hi
    · rfl
    refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
    rw [SModEq.zero, smul_eq_mul, Ideal.mul_top, show f - g * H.div f =
      f - g * (H.seq f k) - g * (H.div f - (H.seq f k)) by ring, map_sub]
    exact Ideal.sub_mem _ (H.coeff_seq_mem f k (not_lt.1 hi)) <|
      coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (H.coeff_div_sub_seq_mem f k) i

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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p✝ : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p✝⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
p : Fin s.card
⊢ (fun n ↦ ↑(s'.equivFin.symm n)) ∘ j = fun i ↦ h ↑(s.equivFin.symm i)

Tactic:
ext n

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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p✝ : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p✝⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
p n : Fin s.card
⊢ ((fun n ↦ ↑(s'.equivFin.symm n)) ∘ j) n = h ↑(s.equivFin.symm n)
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case hpq
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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (rTensor M (rename j).toLinearMap) p
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ h'.comp (φ R s).rangeRestrict = (φ R s').rangeRestrict.comp (rename j)

Tactic:
ext n

Goal state after:
case hpq
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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := ⋯
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := ⋯
j : Fin s.card → Fin s'.card := ⋯
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := ⋯
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
n : Fin s.card
⊢ ↑((h'.comp (φ R s).rangeRestrict) (X n)) = ↑(((φ R s').rangeRestrict.comp (rename j)) (X n))
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✝ : IsAdicComplete I A
f : A⟦X⟧ ⧸ Ideal.span {g}
⊢ (Ideal.Quotient.mk (Ideal.span {g})) ↑(H.mod' f) = f

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
  rw [mod'_mk_eq_mod, Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
  use H.div f
  rw [eq_sub_iff_add_eq, mul_comm, (H.isWeierstrassDivisionAt_div_mod f).2.symm]

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

Goal state before:
pp: case refine_2
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
⊢ m = sSup (Subtype.val '' OrderIso.setIsotypicComponents.symm ⟨m, h⟩)

pp: case refine_3
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
⊢ (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant

Tactic:
· convert! Subtype.ext_iff.mp (OrderIso.setIsotypicComponents.right_inv ⟨m, h⟩).symm
    simp [sSup_image, OrderIso.setIsotypicComponents, OrderIso.symm]

Goal state after:
case refine_3
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
⊢ (∃ s ⊆ isotypicComponents R M, m = sSup s) → m.IsFullyInvariant
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
classical exact ⟨n, hn, _, _, _, ⟨e⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
surjRS : Function.Surjective ⇑(algebraMap R S)
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
⊢ Ideal.comap (algebraMap R R') (RingHom.ker (algebraMap R' S')) =
    RingHom.ker (algebraMap R R') ⊔ RingHom.ker (algebraMap R S)

Tactic:
by
  rw [RingHom.comap_ker, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ S,
      ← RingHom.comap_ker]
  simp [eqmap, Ideal.comap_map_of_surjective' _ surjRS]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I ^ 2 = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker

Tactic:
rw [pow_two] at sq
  have {x : R} (h : x ∈ I * J) : f (J.toCotangent ⟨x, Ideal.mul_le_right h⟩) = 0 := by
    induction h using Submodule.mul_induction_on' with
    | mem_mul_mem y hy z hz =>
      rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_right (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]
    | add y ymem z zmem hy hz =>
      have : (⟨y + z, Ideal.mul_le_right (add_mem ymem zmem)⟩ : J) =
        ⟨y, Ideal.mul_le_right ymem⟩ + ⟨z, Ideal.mul_le_right zmem⟩ := rfl
      rw [this, map_add, map_add, hy, hz, add_zero]
  intro x hx
  rcases Submodule.mem_map.mp hx with ⟨x', hx', eq⟩
  simpa [← eq] using this hx'

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
⊢ A * { coeff := inverseCoeff a A } = 1

Tactic:
ext n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
⊢ (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
⊢ (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n

Tactic:
induction n with

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) = coeff 1 (n + 1)
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this✝³ : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
IP✝ : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) (RingHom.ker (algebraMap R R'))
Gen : Generators R' S' S :=
  { val := ⇑(algebraMap S S'), σ' := fun s' ↦ MvPolynomial.X (Classical.choose ⋯), aeval_val_σ' := ⋯,
    algebraMap_eq := ⋯ }
P' : Extension R' S' := Gen.toExtension
this✝² : FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
this✝¹ : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
this✝ : IsScalarTower R P.Ring P'.Ring :=
  IsScalarTower.of_algebraMap_eq fun x ↦ Eq.symm (MvPolynomial.map_C (algebraMap R R') x)
algInst✝ : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
scalarTowerInst✝ : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap P.Ring S'))
this : IsScalarTower P.Ring P'.Ring S'
J : Ideal P.Ring := RingHom.ker (algebraMap P.Ring S)
J' : Ideal P'.Ring := RingHom.ker (algebraMap P'.Ring S')
I : Ideal R := RingHom.ker (algebraMap R R')
IS : Ideal S := Ideal.map (algebraMap R S) I
kerS : RingHom.ker (algebraMap S S') = IS
IP : Ideal P.Ring := Ideal.map (algebraMap R P.Ring) I
kerP : RingHom.ker (algebraMap P.Ring P'.Ring) = IP
surjPP' : Function.Surjective ⇑(algebraMap P.Ring P'.Ring)
ISeq : IS = Ideal.map (algebraMap P.Ring S) IP
surjP : Function.Surjective ⇑(algebraMap P.Ring S)
surjP' : Function.Surjective ⇑(algebraMap P'.Ring S')
σ : TensorProduct P'.Ring S' Ω[P'.Ring⁄R'] →ₗ[P'.Ring] (RingHom.ker (algebraMap P'.Ring S')).Cotangent
hσ : σ ∘ₗ KaehlerDifferential.kerCotangentToTensor R' P'.Ring S' = LinearMap.id
infeq : IP ⊓ J = IP * J
⊢ RingHom.ker (algebraMap S S') = Ideal.map (algebraMap P.Ring S) (RingHom.ker (algebraMap P.Ring P'.Ring))

Tactic:
by simp [kerP, ← ISeq, eqmap, IS, I]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ False

Tactic:
apply solution_nonzero p ha₁ ha₂

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ frobenius (frobeniusRotation p ha₁ ha₂) * a₁ = frobeniusRotation p ha₁ ha₂ * a₂

Tactic:
ext n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
⊢ (frobenius (frobeniusRotation p ha₁ ha₂) * a₁).coeff n = (frobeniusRotation p ha₁ ha₂ * a₂).coeff n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ (aeval (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]))
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
      (y.coeff (n + 1) *
          (aeval (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]))
            ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        x.coeff (n + 1) *
          (aeval (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]))
            ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)))) =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)

Tactic:
← sub_sub

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ (aeval (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]))
          (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) -
        y.coeff (n + 1) *
          (aeval (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]))
            ((rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) -
      x.coeff (n + 1) *
        (aeval (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]))
          ((rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) =
    (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2
b o : Ordinal.{u_1}
⊢ ∀ (o : Ordinal.{u_1}),
    o ≠ 0 →
      foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o →
        foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
· intro o ho IH
    rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
⊢ lfpApprox f x i ≤ a

Tactic:
induction i using WellFoundedLT.induction with | ind i IH
  rw [lfpApprox]
  apply sup_le hxa
  rw [iSup₂_le_iff, ← ha.eq]
  exact fun y hy ↦ f.mono (IH y hy)

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

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ eval b (single e₁ x + f₁ + f₂) = eval b (single e₁ x + f₁) + eval b f₂

Tactic:
| single_add e₁ x f₁ hf₁ hx IH =>

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

Goal state before:
pp: case refine_2.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ enumOrd s '' Set.Iio a ⊆ s

Tactic:
apply (Set.image_subset_range ..).trans_eq

Goal state after:
case refine_2.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
⊢ Set.range (enumOrd s) = s
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr.inl
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₂ ≤ ↑n₁
nh : ↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

pp: case inr.inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₂ ≤ ↑n₁
nh : ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
· exact oadd_lt_oadd_2 h₂ nh.left

Goal state after:
case inr.inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₂ ≤ ↑n₁
nh : ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.ZFC.Cardinal

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

Tactic:
by
  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.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (o + 1) = enumOrd (Function.fixedPoints (veblenWith f o))

Tactic:
veblenWith_of_ne_zero f (add_pos_of_right zero_lt_one _).ne',

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ (derivFamily fun x ↦ veblenWith f ↑x) = enumOrd (Function.fixedPoints (veblenWith f o))
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
hyx : y ⊆ x
z✝ : ZFSet.{u}
⊢ z✝ ∈ x ∩ y ↔ z✝ ∈ y

Tactic:
simpa using @hyx _

Goal state after: