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

Goal state before:
pp: case e'_5.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ✝ φ ψ : SimpleFunc E E
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ Integrable (⇑φ ∘ X 0) μ

Tactic:
exact (φ.comp (X 0) h').integrable_of_isFiniteMeasure

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

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
i : ℕ
σ : ↑(X.homogeneousCochains.X i).toModuleCat
⊢ ↑((TopModuleCat.Hom.hom ((invariantsFunctor k G).map (X.d (i + 1)))) σ) = (Hom.hom (X.d (i + 1))) ↑σ

Tactic:
dsimp [ContIntertwiningMap.mapInvariants_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : ↑(H1 (Rep.ofAlgebraAutOnUnits K L))
x : ↥(cocycles₁ (Rep.ofAlgebraAutOnUnits K L))
β : Lˣ
hβ : ∀ (g : Gal(L/K)), g • β / β = ↑x g
⊢ IsMulCoboundary₁ x.1

Tactic:
use β

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 0)) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y) =
    (ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z

Tactic:
by ext; simp [← hy, cochainsIso₀]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (ModuleCat.Hom.hom ((cochainsIso₂ A).hom ≫ d₂₃ A)) x y =
    (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom)) x y

Tactic:
change A.ρ y.1 (x _) - x _ + x _ - x _ = _ + _

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)) =
    (A.ρ (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm y 0))
        (x fun i ↦
          ((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm y i.succ) +
      ∑ j,
        (-1) ^ (↑j + 1) •
          x
            (j.contractNth (fun x1 x2 ↦ x1 * x2)
              (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm y))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hx : (ConcreteCategory.hom (d₀₁ A)) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x

Tactic:
refine ⟨⟨x, fun g => ?_⟩, rfl⟩

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hx : (ConcreteCategory.hom (d₀₁ A)) x = 0
g : G
⊢ (A.ρ g) x = x
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ ∀ b ∈ ⋯.toFinset, b ≠ 0 → (coeff b) p = 0

Tactic:
simp [mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s

Tactic:
intro V hV
    obtain ⟨m, hm⟩ := h.right V hV
    use m
    refine Set.Subset.trans ?_ hm
    cases n
    · exfalso
      exact Nat.not_succ_le_zero 0 hn
    rw [← pow_mul, Nat.succ_mul]
    apply Ideal.pow_le_pow_right
    apply Nat.le_add_left

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
h : i < n
⊢ 0 = (transitionMap I M ⋯) (↑x n)

Tactic:
hxn,

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
i : ℕ
h : i < n
⊢ 0 = (transitionMap I M ⋯) 0
Module: Mathlib.RingTheory.Congruence.Star

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star (w✝ + y✝)) (Star.star (x✝ + z✝))

Tactic:
star_add,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : R
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star w✝ + Star.star y✝) (Star.star (x✝ + z✝))
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ contentIdeal 1 = ⊤

Tactic:
by
  rw [← span_singleton_one, ← contentIdeal_C 1, C_1]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
⊢ ⟨val✝, hx⟩ ∈ selmerGroup.subgroupOf selmerGroup

Tactic:
v

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
S : Set (HeightOneSpectrum R)
n : ℕ
val✝ : Kˣ ⧸ (powMonoidHom n).range
hx : val✝ ∈ selmerGroup
hx' : ⟨val✝, hx⟩ ∈ valuation.ker
v : HeightOneSpectrum R
⊢ v ∉ ∅ → (v.valuationOfNeZeroMod n) (selmerGroup.subtype ⟨val✝, hx⟩) = 1
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
⊢ Subsingleton (Ext N M (i + 1))

Tactic:
let g := (AddCommGrpCat.ofHom ((Ext.mk₀ (smulShortComplex M a).f).postcomp N
          (add_zero (i + 1))))
        -- from the (covariant) long exact sequence given by `M.smulShortComplex a`
        -- we obtain scalar multiple by `a` on `Ext N M i` is injective
        have mono_g : Mono g := by
          apply (Ext.covariant_sequence_exact₁' N reg.1.smulShortComplex_shortExact i (i + 1)
            rfl).mono_g ((AddCommGrpCat.isZero_of_iff_subsingleton.mpr ?_).eq_zero_of_src _)
          apply ih (ModuleCat.of R (QuotSMulTop a M)) _ rs' mem.2 reg.2 len i (by omega)
          exact (smul_top_quotSMulTop_ne_top_of_smul_top_ne_top mem.1 smul_lt.ne).lt_top
        let gk := AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex (a ^ k)).f).postcomp N
          (add_zero (i + 1)))
        have mono_gk : Mono gk := by
          simp only [smulShortComplex_f_eq_smul_id, g, gk] at mono_g ⊢
          exact (Ext.postcomp_smul_id_mono_iff (a ^ k) (i + 1)).mpr <|
            ((Ext.postcomp_smul_id_mono_iff a (i + 1)).mp mono_g).pow k
        -- scalar multiple by `aᵏ` on `Ext N M i` is zero since `aᵏ ∈ Ann(N)`, so `Ext N M i` vanish
        have zero_gk : gk = 0 := Ext.postcomp_smul_id_eq_zero_of_mem_annihilator hk (i + 1)
        exact AddCommGrpCat.subsingleton_of_isZero (IsZero.of_mono_eq_zero _ zero_gk)

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

Goal state before:
pp: case mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
h' : hI.DPMorphism hJ
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ } =
    (fun h ↦ ⇑h.toRingHom) h'
⊢ { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ } = h'

Tactic:
cases h'

Goal state after:
case mk.mk
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }
⊢ { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case x
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x✝ : B
hx : x✝ ∈ J
⊢ e.symm x✝ ∈ I

Tactic:
rwa [I.symm_apply_mem_of_equiv_iff, h]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ e.symm x✝ ∈ I

Tactic:
rwa [I.symm_apply_mem_of_equiv_iff, h]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
⊢ (if hx : x + y ∈ I then ⋯.choose else 0) =
    ∑ k ∈ Finset.antidiagonal n, (if hx : x ∈ I then ⋯.choose else 0) * if hx : y ∈ I then ⋯.choose else 0

Tactic:
by
    have hxy : x + y ∈ I := Ideal.add_mem _ hx hy
    simpa only [dif_pos hxy, dif_pos hx, dif_pos hy, ← hf.eq_iff, map_sum, map_mul,
      (Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2, map_add]
      using hJ.dpow_add (hIJ ▸ I.mem_map_of_mem f hx) (hIJ ▸ I.mem_map_of_mem f hy)

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

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
x✝ x : A
hx : x ∈ I • J
y : A
hy : y ∈ I • J
hx' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ I • J
hy' : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ I • J
m : ℕ
hm : m ≠ 0
k : ℕ
a✝ : k ∈ Finset.range (m + 1)
hk0 : ¬k = 0
⊢ hI.dpow k x * hI.dpow (m - k) y ∈ I • J

Tactic:
exact mul_mem_right _ (I • J) (hx' k hk0)

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I • J
⊢ hI.dpow m x ∈ I • J

Tactic:
induction hx using Submodule.smul_induction_on' generalizing m with
    | smul a ha b hb =>
      rw [smul_eq_mul, smul_eq_mul, mul_comm a b, hI.dpow_mul ha, mul_comm]
      exact Submodule.mul_mem_mul (J.pow_mem_of_mem hb m (zero_lt_iff.mpr hm))
        (hI.dpow_mem hm ha)
    | add x hx y hy hx' hy' =>
      rw [hI.dpow_add' (mul_le_left hx) (mul_le_left hy)]
      apply Submodule.sum_mem (I • J)
      intro k _
      by_cases hk0 : k = 0
      · exact hk0 ▸ mul_mem_left (I • J) _ (hy' _ hm)
      · exact mul_mem_right _ (I • J) (hx' k hk0)

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hI : Ideal.span {ε} < I
⊢ I = ⊤

Tactic:
· rcases ideal_trichotomy I with rfl | rfl | rfl <;>
    first | simp at hI | simp

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this : IsScalarTower S (S × U) U
⊢ Etale S U

Tactic:
have : Etale S (S × U) := Etale.of_equiv e

Goal state after:
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Nontrivial R
this✝¹ : Nontrivial S
U : Type u
w✝¹ : CommRing U
w✝ : Algebra S U
e : S ⊗[R] S ≃ₐ[S] S × U
algInst✝ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝ : IsScalarTower S (S × U) U
this : Etale S (S × U)
⊢ Etale S U
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
⊢ a + b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}

Tactic:
apply And.intro (I.add_mem ha.1 hb.1) (fun n ↦ ?_)
    rw [hI.dpow_add ha.1 hb.1, hI'.dpow_add ha.1 hb.1]
    exact Finset.sum_congr rfl (fun k _ ↦ by rw [ha.2, hb.2])

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ dpow hI f 0 (f a) = 1

Tactic:
dpow_apply' hI hIf ha,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow 0 a) = 1
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : f a = x
⊢ dpow hI f 1 (f a) = f a

Tactic:
dpow_apply' hI hIf ha,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : f a = x
⊢ f (hI.dpow 1 a) = f a
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
b : A
hb : b ∈ I
hy : f b ∈ J
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n✝
⊢ f (hI.dpow k.1 a * hI.dpow k.2 b) = dpow hI f k.1 (f a) * dpow hI f k.2 (f b)

Tactic:
dpow_apply' hI hIf ha,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
b : A
hb : b ∈ I
hy : f b ∈ J
k : ℕ × ℕ
x✝ : k ∈ Finset.antidiagonal n✝
⊢ f (hI.dpow k.1 a * hI.dpow k.2 b) = f (hI.dpow k.1 a) * dpow hI f k.2 (f b)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
⊢ (powerSeriesFamily 0 f).hsum.coeff g = (PowerSeries.constantCoeff f • 1).coeff g

Tactic:
by_cases hg : g = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : g = 0
⊢ (powerSeriesFamily 0 f).hsum.coeff g = (PowerSeries.constantCoeff f • 1).coeff g

case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
f : PowerSeries R
g : Γ
hg : ¬g = 0
⊢ (powerSeriesFamily 0 f).hsum.coeff g = (PowerSeries.constantCoeff f • 1).coeff g
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

Tactic:
by_cases hg : g = 0

Goal state after:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (if 0 = 0 then r • (if 0 < x.orderTop then x else 0) ^ 0 else 0).coeff g = ((algebraMap R R⟦Γ⟧) r).coeff g
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0

Tactic:
by_cases hg : g = 0

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0

case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
hg : ¬g = 0
⊢ (coeff 0) (C r) * ((if 0 < x.orderTop then x else 0) ^ 0).coeff g = if g = 0 then r else 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
n : ℕ
x✝ : Γ
⊢ ((powers 0) n).coeff x✝ = ((single 0 1) n).coeff x✝

Tactic:
rw [powers_of_orderTop_pos (by simp)]

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
n : ℕ
x✝ : Γ
⊢ (0 ^ n).coeff x✝ = ((single 0 1) n).coeff x✝
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case inr
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
hle : p ≤ q
h : p ≠ q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
· rw [P.over_def p] at hle h
    exact Algebra.HasGoingUp.exists_ideal_ge_liesOver_of_lt P (lt_of_le_of_ne hle h)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ↔ I ⊓ J = I * J

Tactic:
let f : J ⧸ (I • ⊤ : Submodule R J) →ₗ[R] R ⧸ I :=
    Submodule.mapQ _ _ J.subtype <| by
      simp [← Submodule.map_le_iff_le_comap, Ideal.mul_le_left]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
f : ↥J ⧸ I • ⊤ →ₗ[R] R ⧸ I := (I • ⊤).mapQ I (Submodule.subtype J) ⋯
⊢ Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ↔ I ⊓ J = I * J
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
⊢ ↑H = sInf {N | IsOpen ↑N ∧ ↑H ≤ N}

Tactic:
by
  apply le_antisymm
  · exact le_sInf fun N hN ↦ hN.2
  · intro g hg
    by_contra hg_not
    let U : Set G := (g • H)ᶜ
    have UOpen : IsOpen U :=
      ((Homeomorph.mulLeft g).isClosedMap _ H.isClosed').isOpen_compl
    have einU : 1 ∈ U := by
      refine Set.mem_compl (fun ⟨l, hl, (hgl : g * l = 1)⟩ ↦ ?_)
      rw [← inv_eq_iff_mul_eq_one] at hgl
      exact hg_not <| inv_mem_iff.mp (hgl ▸ hl)
    obtain ⟨N, hN⟩ := exist_openNormalSubgroup_sub_open_nhds_of_one UOpen einU
    let NH : Subgroup G := N ⊔ H
    have hg_not' : g ∉ NH := by
      by_contra hg'
      rcases Subgroup.mem_sup_of_normal_left.mp hg' with ⟨y, hy, z, hz, hyz⟩
      rw [← eq_mul_inv_iff_mul_eq] at hyz
      exact hN (hyz ▸ hy) <| mem_leftCoset g (inv_mem_iff.mpr hz)
    exact hg_not' <|
      Subgroup.mem_sInf.mp hg _ ⟨Subgroup.isOpen_mono le_sup_left N.isOpen, le_sup_right⟩

Goal state after: