mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
⊢ mgf X μ t ≤ rexp (↑((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2)

Tactic:
obtain ht | ht | ht := lt_trichotomy 0 t
    · exact ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero hm hb hc ht
    · simp [← ht]
    calc
    _ = mgf (-X) μ (-t) := by simp [mgf]
    _ ≤ exp ((‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2) := by
      apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
      · filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
      · simp only [Pi.neg_apply]; rw [integral_neg, hc, neg_zero]
      · rwa [Left.neg_pos_iff]
    _ = exp (((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2) := by ring_nf

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A : Rep k G
g : G
x : ↑A
r : k
⊢ (Hom.hom (A.leftRegularHom x)) (MonoidAlgebra.single g r) = r • (A.ρ g) x

Tactic:
by
  simp [leftRegularHom]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom 0

Tactic:
simp [zero_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom 0

Tactic:
simp [zero_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
⊢ Epi ι

Tactic:
have hφι : φ ≫ ι ≠ 0 := by
        intro habs
        have hιφ : 𝟙 _ = ι ≫ φ := (Injective.comp_factorThru (𝟙 _) ι).symm
        apply_fun (· ≫ ι) at hιφ
        simp_all

Goal state after:
case refine_2
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
W : FDRep k G
f : W ⟶ V
x✝ : Mono f
ι : Abelian.image f ⟶ V := Abelian.image.ι f
hf : Abelian.factorThruImage f ≫ ι ≠ 0
φ : V ⟶ Abelian.image f := Injective.factorThru (𝟙 (Abelian.image f)) ι
hφι : φ ≫ ι ≠ 0
⊢ Epi ι
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Finite G
inst✝² : Group G
inst✝¹ : IsAlgClosed k
inst✝ : NeZero ↑(Nat.card G)
V : FDRep k G
h : Module.finrank k (V ⟶ V) = 1
⊢ Simple V

Tactic:
refine { mono_isIso_iff_nonzero {W} f _ := ⟨fun hf habs ↦ ?_, fun hf ↦ ?_⟩ }
    · rw [habs, isIsoZero_iff_source_target_isZero] at hf
      obtain ⟨g, hg⟩ : ∃ g : V ⟶ V, g ≠ 0 :=
        (Module.finrank_pos_iff_exists_ne_zero (R := k)).mp (by grind)
      exact hg (hf.2.eq_zero_of_src g)
    · suffices Epi f by exact isIso_of_mono_of_epi f
      suffices Epi (Abelian.image.ι f) by
        rw [← Abelian.image.fac f]
        exact epi_comp _ _
      rw [← Abelian.image.fac f] at hf
      set ι := Abelian.image.ι f
      set φ := Injective.factorThru (𝟙 _) ι
      have hφι : φ ≫ ι ≠ 0 := by
        intro habs
        have hιφ : 𝟙 _ = ι ≫ φ := (Injective.comp_factorThru (𝟙 _) ι).symm
        apply_fun (· ≫ ι) at hιφ
        simp_all
      obtain ⟨c, hc⟩ : ∃ c : k, c • _ = 𝟙 V := (finrank_eq_one_iff_of_nonzero' _ hφι).mp h (𝟙 V)
      refine Preadditive.epi_of_cancel_zero _ (fun g hg ↦ ?_)
      apply_fun (· ≫ g) at hc
      simpa [hg] using hc.symm

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : σ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
⊢ ↑σ 1 ∈ X.ρ.invariants

Tactic:
simp only [Nat.reduceAdd, LinearMap.mem_ker, ContinuousLinearMap.coe_coe,
    Subtype.ext_iff, homogeneousCochains.d_apply _] at hσ

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (Hom.hom (X.d 1)) ↑σ = ↑0
⊢ ↑σ 1 ∈ X.ρ.invariants
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
⊢ ∀ (x y : R),
    x ∈ Submodule.span R S →
      y ∈ Submodule.span R S →
        (∃ x_1 ∈ span T, constantCoeff x_1 = x) →
          (∃ x ∈ span T, constantCoeff x = y) → ∃ x_1 ∈ span T, constantCoeff x_1 = x + y

Tactic:
intro r₁ r₂ hr₁ hr₂ ⟨s₁, hs₁mem, hs₁⟩ ⟨s₂, hs₂mem, hs₂⟩

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f : R⟦X⟧
hf : constantCoeff f ∈ span S
r₁ r₂ : R
hr₁ : r₁ ∈ Submodule.span R S
hr₂ : r₂ ∈ Submodule.span R S
s₁ : R⟦X⟧
hs₁mem : s₁ ∈ span T
hs₁ : constantCoeff s₁ = r₁
s₂ : R⟦X⟧
hs₂mem : s₂ ∈ span T
hs₂ : constantCoeff s₂ = r₂
⊢ ∃ x ∈ span T, constantCoeff x = r₁ + r₂
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : optionElim n y = x
h2 : n = x none
⊢ r = (coeff y) ((monomial x.some) r)

Tactic:
simp [← h1]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (Finsupp.cons k x)) (X 0) = (coeff x) (if k = 1 then 1 else 0)

Tactic:
coeff_X,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
⊢ (if Finsupp.cons k x = single 0 1 then 1 else 0) = (coeff x) (if k = 1 then 1 else 0)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ (finSuccEquiv R n) (X 0) = PowerSeries.X

Tactic:
ext k x
  simp_rw [coeff_coeff_finSuccEquiv, PowerSeries.coeff_X, coeff_X, cons_eq_single_zero_iff]
  split_ifs with h1 h2 h3
  · simp [h1.left]
  · tauto
  · rw [coeff_one, if_neg (by tauto)]
  · rw [coeff_zero]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (coeff (Finsupp.cons k x)) (X j.succ) = (coeff x) (if k = 0 then X j else 0)

Tactic:
coeff_X,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
⊢ (if Finsupp.cons k x = single j.succ 1 then 1 else 0) = (coeff x) (if k = 0 then X j else 0)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ 0 = (coeff x) (X j)

Tactic:
coeff_X,

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ 0 = if x = single j 1 then 1 else 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
⊢ MvPowerSeries.subst (fun x ↦ MvPowerSeries.X i) f = subst (MvPowerSeries.X i) f

Tactic:
subst

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
⊢ MvPowerSeries.subst (fun x ↦ MvPowerSeries.X i) f = MvPowerSeries.subst (fun x ↦ MvPowerSeries.X i) f
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst (fun s ↦ a i) f = subst (a i) f

Tactic:
subst

Goal state after:
σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst (fun s ↦ a i) f = MvPowerSeries.subst (fun x ↦ a i) f
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
G : Type u_5
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Group G
⊢ mapDomainOfBialgHom (BialgHom.id R R[G]) = MonoidHom.id G

Tactic:
by
  simp [← mapDomainBialgHom_id]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ mapCycles₂ (g.comp f) (φ ≫ (resFunctor f).map ψ) = mapCycles₂ f φ ≫ mapCycles₂ g ψ

Tactic:
rw [← cyclesMap'_comp, ← mapShortComplexH2_comp]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_11
inst✝² : CommSemiring R
A : Type u_12
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
n : ℤ
⊢ counit (T n) = 1

Tactic:
by
  simp [T, -single_eq_C_mul_T]

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

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
⊢ False

Tactic:
let p' : PrimeSpectrum R := ⟨p, pass.isPrime⟩

Goal state after:
case inr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
p : Ideal R
pass : p ∈ associatedPrimes R M
hp : annihilator R N ≤ p
x✝ : p.IsPrime := IsAssociatedPrime.isPrime pass
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
⊢ False
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
inst✝¹ : Module.Finite R ↑N
h_supp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      (∀ i < n, Subsingleton (Ext N M i)) →
        ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
h_ext : ∀ i < n + 1, Subsingleton (Ext N M i)
⊢ ∃ rs, rs.length = n + 1 ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

Tactic:
rw [Module.support_eq_zeroLocus, PrimeSpectrum.zeroLocus_eq_iff] at h_supp
    -- use `Ext N M 0` vanish to obtain an `M`-regular element `x` in `Ann(N)`
    have : Subsingleton (N ⟶ M) := Ext.addEquiv₀.subsingleton_congr.mp (h_ext 0 n.zero_lt_succ)
    have : Subsingleton (N →ₗ[R] M) := ModuleCat.homAddEquiv.symm.subsingleton
    obtain ⟨x, mem_ann, hx⟩ := subsingleton_linearMap_iff.mp this
    -- take a power of it to make `xᵏ` fall into `I`
    obtain ⟨k, hk⟩ := le_of_le_of_eq Ideal.le_radical h_supp mem_ann
    -- verify that `N` indeed make `M ⧸ xᵏM` satisfy the induction hypothesis
    have h_ext' : ∀ i < n, Subsingleton (Ext N (ModuleCat.of R (QuotSMulTop (x ^ k) M)) i) := by
      intro i hi
      -- the vanishing of `Ext` is obtained from the (covariant) long exact sequence given by
      -- `M.smulShortComplex (x ^ k)`
      have zero1 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext i (by omega))
      have zero2 := AddCommGrpCat.isZero_of_iff_subsingleton.mpr (h_ext (i + 1) (by omega))
      exact AddCommGrpCat.subsingleton_of_isZero <| ShortComplex.Exact.isZero_of_both_zeros
        ((Ext.covariant_sequence_exact₃' N (hx.pow k).smulShortComplex_shortExact) i (i + 1) rfl)
        (zero1.eq_zero_of_src _) (zero2.eq_zero_of_tgt _)
    obtain ⟨rs, len, mem, reg⟩ := ih (ModuleCat.of R (QuotSMulTop (x ^ k) M))
      (smul_top_quotSMulTop_ne_top_of_smul_top_ne_top hk smul_lt.ne).lt_top h_ext'
    use x ^ k :: rs
    simpa [len, hk] using ⟨mem, hx.pow k, reg⟩

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.mem.smul
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m : M
x✝ : DividedPowerAlgebra R M
k : ℕ
i : ι
r : R
x : DividedPowerAlgebra R M
hxmem : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hx : x * dp R k (v i) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ r • (x * dp R k (v i)) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
exact smul_mem _ _ hx

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ k ! * ((m + k).choose k * m !) = k ! * (m ! * (m + k).choose m)

Tactic:
mul_comm _ (m !),

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ k ! * (m ! * (m + k).choose k) = k ! * (m ! * (m + k).choose m)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * x ^ (m + k)) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * x ^ (m + k))

Tactic:
hxmk,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ * 0) = ↑((m + k).choose m) * ((↑(m + k)!)⁻¹ʳ * 0)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ hI.IsSubDPIdeal (span S) ↔ ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S

Tactic:
refine ⟨fun hhI n hn s hs ↦ hhI.dpow_mem n hn (subset_span hs), fun hhI ↦ ?_⟩

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
⊢ hI.IsSubDPIdeal (span S)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * (↑k !)⁻¹ʳ ^ m * x ^ (m * k) = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))

Tactic:
hxmk,

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * (↑k !)⁻¹ʳ ^ m * 0 = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * 0)
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsFiniteSplit R S
n : ℕ
e : S ≃ₐ[R] Fin n → R
⊢ T ⊗[R] S ≃ₐ[T] Fin n → T

Tactic:
exact (TensorProduct.congr AlgEquiv.refl e).trans
    ((TensorProduct.piRight R T T (fun _ : Fin n ↦ R)).trans <|
      AlgEquiv.piCongrRight fun i ↦ TensorProduct.rid R T T)

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: k : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Field k
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra k R
inst✝³ : Algebra R S
T : Type u_4
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : IsFiniteSplit R S
⊢ IsFiniteSplit T (T ⊗[R] S)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Algebra.IsFiniteSplit.nonempty_algEquiv_fun R S
  refine ⟨n, ⟨?_⟩⟩
  exact (TensorProduct.congr AlgEquiv.refl e).trans
    ((TensorProduct.piRight R T T (fun _ : Fin n ↦ R)).trans <|
      AlgEquiv.piCongrRight fun i ↦ TensorProduct.rid R T T)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ F.Xzero) F.Xzero = subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries

Tactic:
subst_comp_subst_apply _ this.const

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] s)) F.toPowerSeries =
    subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ HasSubst ![PowerSeries.X, 0]
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ PowerSeries.subst F.Xzero F.Xzero = subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries

Tactic:
rw [PowerSeries.subst, subst_comp_subst_apply _ this.const]

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] s)) F.toPowerSeries =
    subst ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ HasSubst ![PowerSeries.X, 0]
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: case h₂
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : LinearOrder M
inst✝² : IsOrderedAddMonoid M
inst✝¹ : Module ℚ M
inst✝ : IsOrderedModule ℚ M
strata : HahnEmbedding.ArchimedeanStrata ℚ M
f : (c : FiniteArchimedeanClass M) → ↥(strata.stratum c) →+o ℝ
hf : ∀ (c : FiniteArchimedeanClass M), Function.Injective ⇑(f c)
c : FiniteArchimedeanClass M
⊢ Function.Injective ⇑(f c).toRatLinearMap

Tactic:
simpa using hf c

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun x ↦ F.zeroX) F.zeroX = subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

Tactic:
subst_comp_subst_apply _ this.const

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![0, PowerSeries.X] F.toPowerSeries) (![0, PowerSeries.X] s)) F.toPowerSeries =
    subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ HasSubst ![0, PowerSeries.X]
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ PowerSeries.subst F.zeroX F.zeroX = subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

Tactic:
rw [PowerSeries.subst, subst_comp_subst_apply _ this.const]

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![0, PowerSeries.X] F.toPowerSeries) (![0, PowerSeries.X] s)) F.toPowerSeries =
    subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ HasSubst ![0, PowerSeries.X]
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 ↦ x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 ↦ x1 + x2) i j → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n ↦ x ^ n) a).coeff ((fun x1 x2 ↦ x1 + x2) i j) ≠ 0}
⊢ n + 1 ∈
    (Nat.succ ''
        ⋃ i_1 ∈ ↑(antidiagonal ⋯ hpwo ((fun x1 x2 ↦ x1 + x2) i j)), {a | ((fun n ↦ x ^ n) a).coeff i_1.2 ≠ 0}) ∪
      {0}

Tactic:
refine Set.mem_union_left _ ⟨n, Set.mem_iUnion.2 ⟨⟨j, i⟩, Set.mem_iUnion.2 ⟨?_, hi⟩⟩, rfl⟩

Goal state after:
case pos.refine_2.succ
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
n : ℕ
i : Γ
hi : i ∈ (npowRec n x).support
j : Γ
hj : j ∈ x.support
ys : (fun x1 x2 ↦ x1 + x2) i j ∈ ⋃ n, (x ^ n).support
hy : ∀ z ∈ ⋃ n, (x ^ n).support, z < (fun x1 x2 ↦ x1 + x2) i j → {a | ((fun n ↦ x ^ n) a).coeff z ≠ 0}.Finite
hn : n + 1 ∈ {a | ((fun n ↦ x ^ n) a).coeff ((fun x1 x2 ↦ x1 + x2) i j) ≠ 0}
⊢ (j, i) ∈ ↑(antidiagonal ⋯ hpwo ((fun x1 x2 ↦ x1 + x2) i j))
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra.HasGoingUp R S
p q : Ideal R
inst✝² : q.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hpq : p < q
⊢ ∃ Q, P < Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
obtain ⟨Q, hPQ, hQ, hQq⟩ := P.exists_ideal_ge_liesOver_of_le (p := p) (q := q) hpq.le
  refine ⟨Q, lt_of_le_of_ne hPQ fun h ↦ ?_, hQ, hQq⟩
  subst Q
  simp [P.over_def p, P.over_def q] at hpq

Goal state after: