mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ✝ : res f A ⟶ B
n✝ : ℕ
S : Subgroup G
inst✝ : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
⊢ (quotientToInvariantsFunctor k S ⋙ functor k (G ⧸ S) n).map φ ≫
      map (QuotientGroup.mk' S) (ofHom (Y.ρ.quotientToInvariants_lift S)) n =
    map (QuotientGroup.mk' S) (ofHom (X.ρ.quotientToInvariants_lift S)) n ≫ (functor k G n).map φ

Tactic:
by
    simp only [Functor.comp_map, functor_map, ← cancel_epi (groupCohomology.π _ n),
      HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.homologyπ_naturality,
      ← HomologicalComplex.cyclesMap_comp_assoc, ← cochainsMap_comp]
    congr 1

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
f : R⟦X⟧
hf : f ∈ I
⊢ C (constantCoeff f) ∈ I

Tactic:
rw [← sub_eq_iff_eq_add'.mpr f.eq_X_mul_shift_add_const]

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
f : R⟦X⟧
hf : f ∈ I
⊢ (f - X * mk fun p ↦ (coeff (p + 1)) f) ∈ I
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : k = 0 ∧ x = 0
h2 : k = 0
⊢ r = (coeff x) (C r)

Tactic:
simp [h1.right]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n : ℕ
S : Type u_3
inst✝² : CommRing S
inst✝¹ : IsNoetherianRing S
inst✝ : Finite σ
⊢ IsNoetherianRing (MvPowerSeries σ S)

Tactic:
cases nonempty_fintype σ

Goal state after:
case intro
σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n : ℕ
S : Type u_3
inst✝² : CommRing S
inst✝¹ : IsNoetherianRing S
inst✝ : Finite σ
val✝ : Fintype σ
⊢ IsNoetherianRing (MvPowerSeries σ S)
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
by
  by_cases h : p.coeff n = 0
  · simp [h]
  · apply subset_span
    simpa using coeff_mem_coeffs h

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

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
a✝ : p.contentIdeal ≠ ⊤
⊢ ∃ x, ∃ (_ : C x ∣ p), ¬IsUnit x

Tactic:
use h_prin.generator, h_prin.contentIdeal_generator_dvd

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
a✝ : p.contentIdeal ≠ ⊤
⊢ ¬IsUnit (Submodule.IsPrincipal.generator p.contentIdeal)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
⊢ False

Tactic:
have : LinearIndepOn R id (insert x <| .range (single · 1)) :=
      linearIndepOn_isGroupLikeElem.mono <| by simp [Set.subset_def, hx]

Goal state after:
R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
⊢ False
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
M : Type u_8
N : Type u_9
O : Type u_10
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[G] →ₐc[R] R[H]
⊢ (fun m ↦ single m 1) (mapDomainOfBialgHomFun f 1) = (fun m ↦ single m 1) 1

Tactic:
simp [← one_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {a | ¬∀ (m : M), a • m = 0 → m = 0}

Tactic:
not_forall,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {a | ∃ x, ∃ (_ : a • x = 0), ¬x = 0}
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: 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
f : A →+* B
hf : map f I ≤ J
⊢ 0 ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}

Tactic:
simp only [mem_ofPred_eq, Submodule.zero_mem, map_zero, true_and]

Goal state after:
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
f : A →+* B
hf : map f I ≤ J
⊢ ∀ (n : ℕ), f (hI.dpow n 0) = hJ.dpow n 0
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
⊢ ringCon R M ≤ RingCon.ker (eval₂AlgHom R f).toRingHom

Tactic:
by
    grw [ringCon, RingCon.ringConGen_le]
    exact lift'_imp R M hf_zero hf_smul hf_mul hf_add

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

Goal state before:
pp: case pos.refine_1
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ ∀ s ∈ S, (RingHom.id A) s ∈ I

pp: case pos.refine_2
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ ∀ {n : ℕ}, ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)

Tactic:
· intro s hs
      simp only [RingHom.id_apply, hS]
      exact subset_span hs

Goal state after:
case pos.refine_2
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ ∀ {n : ℕ}, ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : torsionBy R M b = a • torsionBy R M b → IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ torsionBy R M b ≤ a • torsionBy R M b

pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a

Tactic:
· refine le_of_eq_of_le ?_ <| smul_top_inf_eq_smul_of_isSMulRegular_on_quot <|
      ha.of_injective _ <| ker_eq_bot.mp <| ker_liftQ_eq_bot' _ (lsmul R M b) rfl
    rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb]
    exact (inf_eq_right.mpr (ker_le_comap _)).symm

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (QuotSMulTop b M) a
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
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
m✝ n✝ : ℕ
x✝ : A
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ (if (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) ∈ J then hI.dpow m✝ (if x✝ ∈ J then hI.dpow n✝ x✝ else 0) else 0) =
    ↑(m✝.uniformBell n✝) * if x✝ ∈ J then hI.dpow (m✝ * n✝) x✝ else 0

Tactic:
by
    simp [if_pos hx, if_pos (hJ.dpow_mem _ hn hx), hI.dpow_comp hn (hJ.isSubideal hx)]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
| ↑n

Tactic:
rw [← one_mul (n : ℤ)]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
| 1 * ↑n
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ hI.IsSubDPIdeal (sSup ((fun J ↦ J.carrier) '' S))

Tactic:
have h : (⋃ (i : Ideal A) (_ : i ∈ (fun J ↦ J.carrier) '' S), ↑i) ⊆ (I : Set A) := by
        rintro a ⟨-, ⟨J, rfl⟩, haJ⟩
        rw [Set.mem_iUnion, SetLike.mem_coe, exists_prop] at haJ
        obtain ⟨J', hJ'⟩ := (Set.mem_image _ _ _).mp haJ.1
        exact  J'.isSubideal  (hJ'.2 ▸ haJ.2)

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
h : ⋃ i ∈ (fun J ↦ J.carrier) '' S, ↑i ⊆ ↑I
⊢ hI.IsSubDPIdeal (sSup ((fun J ↦ J.carrier) '' S))
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
| ⨅ a ∈ S, ⟨a.carrier, ⋯⟩

Tactic:
iInf

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
| sInf (Set.range fun a ↦ ⨅ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
m : ℕ
a✝ : m ∈ Finset.range (n + 1)
hm0 : ¬m = 0
⊢ hI.dpow m x * hI.dpow (n - m) y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
· exact (span _).mul_mem_right _ (hx_pow m hm0)

Goal state after:
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}
n : ℕ
⊢ hI.dpow n (a + b) = hI'.dpow n (a + b)

Tactic:
rw [hI.dpow_add ha.1 hb.1, hI'.dpow_add ha.1 hb.1]

Goal state after:
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}
n : ℕ
⊢ ∑ k ∈ Finset.antidiagonal n, hI.dpow k.1 a * hI.dpow k.2 b =
    ∑ k ∈ Finset.antidiagonal n, hI'.dpow k.1 a * hI'.dpow k.2 b
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ (algebraMap S (Localization.AtPrime Q)) (φ x) = (algebraMap S (Localization.AtPrime Q)) (ψ x)

Tactic:
← H.localize_algebraMap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ H.localize ((algebraMap S (Localization.AtPrime Q)) x) = (algebraMap S (Localization.AtPrime Q)) (ψ x)
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
⊢ Set.image2 (fun m n ↦ (↑(Algebra.lmul S (S ⊗[R] A)) m) n) ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 i))
      ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 j)) ⊆
    ↑(span S ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 (i + j))))

Tactic:
Set.image2_subset_iff

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
⊢ ∀ x ∈ ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 i)),
    ∀ y ∈ ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 j)),
      (↑(Algebra.lmul S (S ⊗[R] A)) x) y ∈ ↑(span S ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 (i + j))))
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.Xzero)
⊢ F.Xzero = PowerSeries.subst (PowerSeries.subst F.Xzero F.Xzero) F.Xzero.substInv

Tactic:
have aux₀ : PowerSeries.HasSubst F.Xzero :=
        PowerSeries.HasSubst.of_constantCoeff_zero' <| constantCoeff_Xzero F

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : Invertible ((PowerSeries.coeff 1) F.Xzero)
aux₀ : PowerSeries.HasSubst F.Xzero
⊢ F.Xzero = PowerSeries.subst (PowerSeries.subst F.Xzero F.Xzero) F.Xzero.substInv
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Tactic:
have hf₂ : Function.Injective f₂ := hf₂'.injective

Goal state after:
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
⊢ ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case refine_1.left
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝ : Γ × Γ'
hgh : ¬∑ i ∈ (s.coeff x✝.1).support, (s i).coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
⊢ ∃ i, ¬(s i).coeff x✝.1 = 0

Tactic:
have h' := Finset.exists_ne_zero_of_sum_ne_zero hgh.1

Goal state after:
case refine_1.left
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
x✝ : Γ × Γ'
hgh : ¬∑ i ∈ (s.coeff x✝.1).support, (s i).coeff x✝.1 = 0 ∧ ¬t.hsum.coeff x✝.2 = 0 ∧ x✝.1 +ᵥ x✝.2 = g
h' : ∃ a ∈ (s.coeff x✝.1).support, (s a).coeff x✝.1 ≠ 0
⊢ ∃ i, ¬(s i).coeff x✝.1 = 0
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : (Ideal.Quotient.mk ⊥.jacobson) a * (Ideal.Quotient.mk ⊥.jacobson) y = 1
h2 : (Ideal.Quotient.mk ⊥.jacobson) y * (Ideal.Quotient.mk ⊥.jacobson) a = 1
⊢ IsUnit a

Tactic:
rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq,
    Ideal.mem_jacobson_bot] at h1 h2

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a
Module: Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : HopfAlgebra R A
G : Type u_3
inst✝ : Group G
g : G
a : A
⊢ (antipode R) (single g a) = single g⁻¹ ((antipode R) a)

Tactic:
by
  simp [antipode]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ n + 2 ≤ i * (n + 1)

Tactic:
trans 2 * (n + 1)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := ⋯
c : ℕ → R := ⋯
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ n + 2 ≤ 2 * (n + 1)

R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := ⋯
c : ℕ → R := ⋯
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right✝ : i < ((taylor (c n)) f).natDegree + 2
⊢ 2 * (n + 1) ≤ i * (n + 1)
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
h : p.height ≤ n
I : Ideal R
hI : I ≤ p
e₁ : Submodule.spanRank I = ↑p.height
e₂ : I.height = p.height
⊢ ∃ I, p ∈ I.minimalPrimes ∧ Submodule.spanRank I ≤ ↑n

Tactic:
refine ⟨I, Ideal.mem_minimalPrimes_of_height_le hI e₂.ge, e₁.symm ▸ ?_⟩

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
p : Ideal R
inst✝ : p.IsPrime
n : ℕ∞
h : p.height ≤ n
I : Ideal R
hI : I ≤ p
e₁ : Submodule.spanRank I = ↑p.height
e₂ : I.height = p.height
⊢ ↑p.height ≤ ↑n
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ x ∈ (p.toFun 1).asIdeal ∧ n + 1 = p.length ∧ RelSeries.head p = RelSeries.head p ∧ RelSeries.last p = RelSeries.last p

Tactic:
have h1 : 1 = Fin.last p.length := by
      rw [Fin.last, hp, h0, zero_add]
      exact Fin.natCast_eq_mk (Nat.one_lt_succ_succ 0)

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
h1 : 1 = Fin.last p.length
⊢ x ∈ (p.toFun 1).asIdeal ∧ n + 1 = p.length ∧ RelSeries.head p = RelSeries.head p ∧ RelSeries.last p = RelSeries.last p
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: case cons
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
x : R
rs' : List R
ih :
  ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module R M] [Module.Finite R M],
    Sequence.IsRegular M rs' → supportDim R (M ⧸ ofList rs' • ⊤) + ↑rs'.length = supportDim R M
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M (x :: rs')
⊢ supportDim R (M ⧸ ofList (x :: rs') • ⊤) + ↑(x :: rs').length = supportDim R M

Tactic:
| cons x rs' ih =>

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
⊢ (({q ∈ t | x ∈ q}.inf fun q ↦ ⊤) ⊓ {i ∈ t | x ∉ i}.inf fun q ↦ (q.colon Set.univ).radical) =
    {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical

Tactic:
Finset.inf_top,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
x : M
⊢ (⊤ ⊓ {i ∈ t | x ∉ i}.inf fun q ↦ (q.colon Set.univ).radical) =
    {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical