mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: 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
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (rTensor N (A.val.toLinearMap ∘ₗ P.subtype)) u = (rTensor N (A.val.toLinearMap ∘ₗ P'.subtype)) u'

Tactic:
simp only [rTensor_comp, comp_apply]

Goal state after:
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
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
hj₁ : P₁.subtype ∘ₗ j = A.val.toLinearMap ∘ₗ P.subtype
hj'₁ : P₁.subtype ∘ₗ j' = A.val.toLinearMap ∘ₗ P'.subtype
⊢ (rTensor N A.val.toLinearMap) ((rTensor N P.subtype) u) = (rTensor N A.val.toLinearMap) ((rTensor N P'.subtype) u')
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
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j
k' : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j'
⊢ (rTensor N (inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j)) u =
    (rTensor N (inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j')) u'

Tactic:
simp only [rTensor_comp, comp_apply]

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
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
hBA : A ≤ B
hP'₁_le : P'₁ ≤ Subalgebra.toSubmodule B
k : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j
k' : (Subalgebra.inclusion hBA).toLinearMap ∘ₗ P'.subtype = inclusion hP'₁_le ∘ₗ inclusion hP₁_le ∘ₗ j'
⊢ (rTensor N (inclusion hP'₁_le)) ((rTensor N (inclusion hP₁_le)) ((rTensor N j) u)) =
    (rTensor N (inclusion hP'₁_le)) ((rTensor N (inclusion hP₁_le)) ((rTensor N j') u'))
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
⊢ (if i < ((map (Ideal.Quotient.mk I)) g).order.toNat then (coeff i) g else 0) ∈ I

Tactic:
split_ifs with h

Goal state after:
case pos
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
h : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) g ∈ I

case neg
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
h : ¬i < ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ 0 ∈ I
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 (R ⧸ Ideal.span {x}) (QuotSMulTop x M) ↔ Free R M

Tactic:
refine ⟨fun free ↦ ?_, fun free ↦ inferInstance⟩
  have := Module.Finite.of_restrictScalars_finite R (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
  let I := Module.Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
  let b := Module.Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
  let b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := b.1.restrictScalars R
  let f := b'.symm.toLinearMap.comp (Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x})))
  rcases Module.projective_lifting_property (Submodule.mkQ (x • (⊤ : Submodule R M))) f
    (Submodule.mkQ_surjective _) with ⟨g, hg⟩
  have surjf : Function.Surjective f := by
    simpa [f] using! Finsupp.mapRange_surjective _ rfl (Submodule.mkQ_surjective (Ideal.span {x}))
  have lejac : Ideal.span {x} ≤ (⊥ :Ideal R).jacobson := by simpa
  have surjg : Function.Surjective g := by
    apply g.surjective_of_surjective_comp_mkQ (Ideal.span {x}) lejac
    rwa [Submodule.ideal_span_singleton_smul x ⊤, hg]
  have kerf : LinearMap.ker f = x • (⊤ : Submodule R (I →₀ R)) := by
    simp only [LinearEquiv.ker_comp, f]
    rw [Finsupp.ker_mapRange, Submodule.ker_mkQ, ← (Ideal.span {x}).mul_top, ← smul_eq_mul,
      Finsupp.submodule_smul]
    simp [Submodule.ideal_span_singleton_smul]
  have injg : Function.Injective g := by
    rw [← LinearMap.ker_eq_bot]
    have fg : (LinearMap.ker g).FG := Module.FinitePresentation.fg_ker g surjg
    apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (Ideal.span {x}) _ fg _ lejac
    rw [Submodule.ideal_span_singleton_smul]
    intro y hy
    have : y ∈ x • (⊤ : Submodule R (I →₀ R)) := by simp [← kerf, ← hg, LinearMap.mem_ker.mp hy]
    rcases (Submodule.mem_smul_pointwise_iff_exists _ _ _).mp this with ⟨z, _, hz⟩
    simp only [← hz, LinearMap.mem_ker, map_smul] at hy
    have := LinearMap.mem_ker.mpr (IsSMulRegular.right_eq_zero_of_smul reg hy)
    simpa [hz] using Submodule.smul_mem_pointwise_smul z x _ this
  exact Module.Free.of_equiv (LinearEquiv.ofBijective g ⟨injg, surjg⟩)

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

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst✝ : IsPrecomplete I A
i m n✝ n : ℕ
hn : m ≤ n
ih : (coeff i) (H.seq f m) ≡ (coeff i) (H.seq f n) [SMOD I ^ m • ⊤]
⊢ (coeff i) (H.seq f (n + 1) - H.seq f n) ∈ I ^ m

Tactic:
exact Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ toFun S (r • f) = r • toFun S f

Tactic:
by
  ext t
  obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
  simp only [toFun_eq_rTensor_φ_toFun' _ ha, smul_def, Pi.smul_apply, map_smul]

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

Goal state before:
pp: case inr
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
f : A[X] ⧸ Ideal.span {g}
h✝ : Nontrivial A
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun f) =
    f

Tactic:
have hI : I ≠ ⊤ := by
      rintro rfl
      exact not_subsingleton _ ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton

Goal state after:
case inr
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
f : A[X] ⧸ Ideal.span {g}
h✝ : Nontrivial A
hI : I ≠ ⊤
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun f) =
    f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inr
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
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun
        ((Ideal.Quotient.mk (Ideal.span {g})) f)) =
    (Ideal.Quotient.mk (Ideal.span {g})) f

Tactic:
have h1 : g.degree = ((g : A⟦X⟧).map (Ideal.Quotient.mk I)).order.toNat := by
      convert!
        H.degree_eq_coe_lift_order_map g 1 (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one])
          (by simp)
      exact (ENat.lift_eq_toNat_of_lt_top _).symm

Goal state after:
case inr
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
h1 : g.degree = ↑((map (Ideal.Quotient.mk I)) ↑g).order.toNat
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun
        ((Ideal.Quotient.mk (Ideal.span {g})) f)) =
    (Ideal.Quotient.mk (Ideal.span {g})) f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
inst✝ : IsAdicComplete I A
x : A⟦X⟧ ⧸ Ideal.span {g}
⊢ H.algEquivQuotient.symm x = (Ideal.Quotient.mk (Ideal.span {f})) (⋯.mod' ((Ideal.quotientEquivAlgOfEq A ⋯) x))

Tactic:
by
  simp [algEquivQuotient]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
H1 : r.degree < ↑n
f : A[X] := Polynomial.X ^ n - r
⊢ r.degree < (Polynomial.X ^ n).degree

Tactic:
rwa [Polynomial.degree_X_pow]

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

Goal state before:
pp: case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ X ^ n = g * ↑⋯.unit⁻¹ + ↑(Polynomial.X ^ n - f)

Tactic:
simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
⊢ (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯

Tactic:
have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
  have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
  have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
  exact (H''.elim (H.mul H')).1

Goal state after:
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
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
let S := (Localization.AtPrime q)[X]

Goal state after:
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]
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ ∃ n, ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
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,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun

Goal state after:
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
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ ∃ n,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

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

Tactic:
by
  rcases subsingleton_or_nontrivial α
  · rw [Subsingleton.elim a 1, moebius_one, one_mul, one_mul]
  by_cases ha : Squarefree a; swap
  · simp [ha, mt Squarefree.of_mul_left ha]
  by_cases hb : Squarefree b; swap
  · simp [hb, mt Squarefree.of_mul_right hb]
  have hab : Squarefree (a * b) := squarefree_mul_iff.mpr ⟨h, ha, hb⟩
  rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]

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

Goal state before:
pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ IsLUB (range fun n ↦ f ⟨t, ht⟩ (g n)) (sSup (range g))

pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ (range fun n ↦ f ⟨t, ht⟩ (g n)) ⊆ t

Tactic:
· refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩ <;> rintro _ ⟨n, rfl⟩
    · apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
      · exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)
      · use ⟨t, ht⟩
    · exact (hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ (range fun n ↦ f ⟨t, ht⟩ (g n)) ⊆ t
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i

Tactic:
obtain ⟨i, hi⟩ := not_isCofinal_iff.1 hf'

Goal state after:
α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
i : α
hi : ∀ y ∈ range (rangeSplitting f), y < i
⊢ ∃ i, ∀ (j : α), i ≤ j → f j = f i
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: case right
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ o₁ + o₃ = o₂

Tactic:
hsub

Goal state after:
case right
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ o₂ = o₂
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom.mp
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩ → Lists'.atom a✝ = l₂

Tactic:
(rintro ⟨rfl⟩; rfl)

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ Lists'.atom a✝ = l₂ → ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩

Tactic:
(rintro ⟨rfl⟩; rfl)

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

Goal state before:
pp: case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = x + (coeff b y) e

Tactic:
coeff_eq_zero_of_lt hy,

Goal state after:
case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (coeff b (b ^ e * x + y)) e = x + 0
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x e' y : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hy : y ≠ 0
h : ∀ e'_1 ∈ (single e' y + f).support, e'_1 ≤ e
a✝ : single e' y + f = f → eval b (single e x + (single e' y + f)) = b ^ e * x + eval b (single e' y + f)
⊢ e' ∈ (single e' y + f).support

Tactic:
by simp [hy]

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

Goal state before:
pp: x y z : PSet.{?u.3}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
⊢ ∃ b, (x.Func a).Equiv (z.Func b)

Tactic:
obtain ⟨b, hb⟩ := hxy a
    obtain ⟨c, hc⟩ := hyz b
    exact ⟨c, hb.trans hc⟩

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

Goal state before:
pp: case inl
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
    simp [h.cmp_eq_lt, h.cmp_eq_gt, (veblenWith_right_strictMono hf _).cmp_map_eq]

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

Goal state before:
pp: case inr.inr
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
⊢ cmp (veblenWith f o₁ a) (veblenWith f o₂ b) =
    match cmp o₁ o₂ with
    | Ordering.eq => cmp a b
    | Ordering.lt => cmp a (veblenWith f o₂ b)
    | Ordering.gt => cmp (veblenWith f o₁ a) b

Tactic:
conv_lhs => rw [← veblenWith_veblenWith_of_lt hf h]
    simp [h.cmp_eq_lt, h.cmp_eq_gt, (veblenWith_right_strictMono hf _).cmp_map_eq]

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]
  apply rank_mono
  intro z _
  rw [mem_powerset]
  intro _ _
  rw [mem_sUnion]
  exists z

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsTrans (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x) → x.IsOrdinal

Tactic:
by
    rintro ⟨h₁, ⟨h₂⟩⟩
    refine ⟨h₁, fun {y z w} hyz hzw hwx ↦ ?_⟩
    have hzx := h₁.mem_trans hzw hwx
    exact h₂ ⟨y, h₁.mem_trans hyz hzx⟩ ⟨z, hzx⟩ ⟨w, hwx⟩ hyz hzw

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

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ∨ y ⊆ x

Tactic:
by
  obtain h | h := mem_or_subset hx hy
  · exact Or.inl (hy.subset_of_mem h)
  · exact Or.inr h

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsOrdinal ↔ x.IsTransitive ∧ IsWellOrder (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)

Tactic:
use fun h ↦ ⟨h.isTransitive, h.isWellOrder⟩
  rintro ⟨h₁, h₂⟩
  refine isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩
  infer_instance

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

Goal state before:
pp: case refine_2
a : Ordinal.{u}
⊢ a.toZFSet.IsOrdinal

Tactic:
exact isOrdinal_toZFSet a

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst✝ : TopologicalSpace α
a b : α
h_neg : Tendsto (fun x ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun x ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
⊢ Tendsto f (𝓝[≠] c) (𝓝 a)

Tactic:
apply tendsto_nhdsNE_of_tendsto_atTop _ _ h_neg

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst✝ : TopologicalSpace α
a b : α
h_neg : Tendsto (fun x ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun x ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
⊢ Tendsto (fun x ↦ f (c + x⁻¹)) atTop (𝓝 a)