mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
hn : ¬n = 0
⊢ Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ^ n) =
    Submodule.restrictScalars R (restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici n) ⋯)
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
⊢ I.FG

Tactic:
refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
⊢ span ↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) ≤ I

case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
⊢ y ∈ span ↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = (ConcreteCategory.hom (H1π A)) y ↔ ↑x - ↑y ∈ boundaries₁ A

Tactic:
by
  rw [← sub_eq_zero, ← map_sub, H1π_eq_zero_iff]
  rfl

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
a✝ : G × G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (chainsMap₂ f φ ≫ d₂₁ B) ∘ₗ lsingle a✝) x✝ =
    (ModuleCat.Hom.hom (d₂₁ A ≫ chainsMap₁ f φ) ∘ₗ lsingle a✝) x✝

Tactic:
simpa [d₂₁, map_add, map_sub, ← map_inv] using congr(single _ $((hom_comm_apply φ _ _).symm))

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((truncTotal n) (toAdicCompletionInv σ R f)) = ↑f n

Tactic:
rw [← Ideal.Quotient.mk_out (f.val n), Ideal.Quotient.mk_eq_mk_iff_sub_mem]
  simp only [smul_eq_mul, Ideal.mul_top, MvPolynomial.mem_pow_idealOfVars_iff',
    MvPolynomial.coeff_sub]
  intro x h
  rw [coeff_truncTotal _ h, coeff_toAdicCompletionInv, ← MvPolynomial.coeff_sub]
  apply (MvPolynomial.mem_pow_idealOfVars_iff' (degree x + 1) _).mp
  · nth_rw 1 [← Ideal.mul_top (MvPolynomial.idealOfVars σ R ^ (degree x + 1)),
      ← smul_eq_mul, ← Ideal.Quotient.eq]
    simp only [Submodule.mapQ_eq_factor, Submodule.factor_eq_factor, Ideal.Quotient.mk_out]
    rw [← AdicCompletion.transitionMap_ideal_mk _ (Nat.lt_iff_add_one_le.mp h), eq_comm]
    convert! f.prop h; simp
  simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
inst✝ : IsAdicComplete I S
f : (n : ℕ) → R →+* S ⧸ I ^ n
hf : ∀ {m n : ℕ} (hle : m ≤ n), (factorPow I hle).comp (f n) = f m
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ n)).comp F = f n
n : ℕ
m : R
⊢ (Ideal.Quotient.mk (I ^ n)) (F m) = (Ideal.Quotient.mk (I ^ n)) ((liftRingHom I f ⋯) m)

Tactic:
simp [← hF n]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → R →+* S ⧸ I ^ a n
hf : ∀ {m : ℕ}, (factorPow I ⋯).comp (f (m + 1)) = f m
inst✝ : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ a n)).comp F = f n
n : ℕ
m : R
⊢ (Ideal.Quotient.mk (I ^ a n)) (F m) = (Ideal.Quotient.mk (I ^ a n)) ((liftRingHom I ha f ⋯) m)

Tactic:
simp [← hF n]

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

Goal state before:
pp: case inr
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
w : G
hw : w ∈ ↑((v.sum fun a b ↦ single ((s ↑a)⁻¹ * a) ((A.ρ (s ↑a)⁻¹) b)) + v.sum fun a ↦ single (s ↑a)).support
hr : w ∈ (v.sum fun a ↦ single (s ↑a)).support
⊢ w ∈ ↑S

Tactic:
simp_all [mapDomain]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ ∑ x ∈ s, ∑ x_1 ∈ s, c x • c x_1 • x ⊗ₜ[R] x_1 = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y

Tactic:
mul_smul

Goal state after:
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✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra R A
inst✝³ : Bialgebra R B
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
⊢ (LinearMap.mul R A[M]).compr₂ comul = (LinearMap.mul R (A[M] ⊗[R] A[M])).compl₁₂ comul comul

Tactic:
by
    ext a b c d
    simp only [Function.comp_apply, LinearMap.coe_comp, LinearMap.compr₂_apply,
      LinearMap.mul_apply', single_mul_single, comul_single, Bialgebra.comul_mul,
      ← (Coalgebra.Repr.arbitrary R b).eq, ← (Coalgebra.Repr.arbitrary R d).eq, Finset.sum_mul_sum,
      Algebra.TensorProduct.tmul_mul_tmul, map_sum, TensorProduct.map_tmul, lsingle_apply,
      LinearMap.compl₁₂_apply, LinearMap.coe_sum, Finset.sum_apply,
      Finset.sum_comm (s := (Coalgebra.Repr.arbitrary R b).index)]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ ↑(v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x)) = ↑1

Tactic:
valuationOfNeZero_eq,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Rˣ
⊢ (valuation K v) ↑((Units.map ↑(algebraMap R K)) x) = ↑1
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if n = 0 then 1 else 0) = if n = 0 then x✝¹ ^ n else 0

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
hn : n = 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x✝¹ ^ n else 0

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
hn : ¬n = 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x✝¹ ^ n else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : n = 0
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case empty
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
⊢ dpow n 0 = ↑(#(∅.sym n))

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

case neg
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : ¬n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))
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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : n = 0
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)

case neg
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
f : A →+* B
hIJ : map f I ≤ J
H : ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
hn : ¬n = 0
⊢ ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map (AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup

Tactic:
← map_map,

Goal state after:
case cons
R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
f : M →+ M₂
as : List R
bs : List S
hf : Surjective ⇑f
r : R
s : S
l₁✝ : List R
l₂✝ : List S
a✝ : List.Forall₂ (fun r s ↦ ∀ (x : M), f (r • x) = s • f x) l₁✝ l₂✝
ih : AddSubgroup.map f (Ideal.ofList l₁✝ • ⊤).toAddSubgroup = (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
h : f.comp ((toAddMonoidEnd R M) r) = AddMonoidHom.comp ((toAddMonoidEnd S M₂) s) f
⊢ AddSubgroup.map ((toAddMonoidEnd S M₂) s) (AddSubgroup.map f ⊤) ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup =
    AddSubgroup.map ((toAddMonoidEnd S M₂) s) ⊤ ⊔ (Ideal.ofList l₂✝ • ⊤).toAddSubgroup
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
a✝ : MvPolynomial (ℕ × N) R
⊢ (∃ a b, X (a, b) = a✝) → a✝ ∈ ↑(Subalgebra.comap (RingCon.mkₐ R (ringCon R N)) (Subalgebra.map (map R f) ⊤))

Tactic:
rintro ⟨n, m, rfl⟩

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
n : ℕ
m : N
⊢ X (n, m) ∈ ↑(Subalgebra.comap (RingCon.mkₐ R (ringCon R N)) (Subalgebra.map (map R f) ⊤))
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
inst✝ : Nontrivial M
h : ⊤ = Ideal.ofList [] • ⊤
⊢ False

Tactic:
by
    rw [Ideal.ofList_nil, bot_smul, eq_comm, subsingleton_iff_bot_eq_top] at h
    exact not_subsingleton M ((Submodule.subsingleton_iff _).mp h)

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

Goal state before:
pp: case hc
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 m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ (if hx : x ∈ I then ⋯.choose else 0) ∈ I

Tactic:
rw [dif_pos hx]
      exact (Exists.choose_spec (hmem m hx)).1 hm

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ 1

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : n = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ 1

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ 1
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
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
z x y : A
hxI : x ∈ Submodule.span A S
hyI : y ∈ Submodule.span A S
hx : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ span S
hy : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ span S
m✝ : ℕ
hm : m✝ ≠ 0
m : ℕ
a✝ : m ∈ range (m✝ + 1)
hm0 : ¬m = 0
⊢ hI.dpow m x * hI.dpow (m✝ - m) y ∈ span S

Tactic:
· exact mul_mem_right _ (span S) (hx _ hm0)

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ((↑(AlgHom.ulift.{?u.31, u₁, u₂, u_1, u_2, u_2} (TensorProduct.lmul' R))).comp
        ↑↑(TensorProduct.uliftEquiv R (ULift.{u₁, u_1} R) S S).symm).Flat ↔
    (RingHom.ulift.{u₁, u₂, u_2, u_2} (TensorProduct.lmul' R).toRingHom).Flat

Tactic:
exact RingHom.Flat.comp_iff_of_bijective_right (Equiv.bijective _)

Goal state after:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u₃
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst✝ : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
⊢ (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₁} R)).Flat

Tactic:
have heq : TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T) (ULift R) =
        AlgHom.comp ((TensorProduct.lmul' (S := ULift.{max u₁ u₂ u₃} T)
          (ULift.{max u₁ u₂ u₃} S)).restrictScalars (ULift.{max u₁ u₂ u₃} R))
          (TensorProduct.mapOfCompatibleSMul ..) := by
      ext <;> simp
    rw [heq]
    refine .comp ?_ ?_
    · exact (flat_lmul' (ULift R) (ULift S)).mapOfCompatibleSMul
        (ULift.{max u₁ u₂ u₃} T) (ULift.{max u₁ u₂ u₃} T)
    · exact WeaklyEtale.flat_lmul' (ULift S) (ULift T)

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.extendScalars.h1CotangentEquivOfSurjective ⋯) ∘ₗ ↑P.h1CotangentExtendScalarsEquiv.symm) ∘ₗ
      Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

Tactic:
h1CotangentExtendScalarsEquiv_symm_toLinearMap,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (↑P.cotangentExtendScalarsEquiv ∘ₗ
        ↑(P.extendScalars.h1CotangentEquivOfSurjective ⋯) ∘ₗ H1Cotangent.map (defaultHom P.Ring S P.extendScalars)) ∘ₗ
      Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
⊢ hI.dpow n 0 = hI'.dpow n 0

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n = 0
⊢ hI.dpow n 0 = hI'.dpow n 0

case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : ¬n = 0
⊢ hI.dpow n 0 = hI'.dpow n 0
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 x = x

Tactic:
rw [← hax, dpow_apply' hI hIf ha, hI.dpow_one ha]

Goal state after:
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 : ι
⊢ ∀ 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))))

Tactic:
rintro - ⟨x, hx, rfl⟩ - ⟨y, hy, rfl⟩

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 : A
hx : x ∈ ↑(𝒜 i)
y : A
hy : y ∈ ↑(𝒜 j)
⊢ (↑(Algebra.lmul S (S ⊗[R] A)) (((TensorProduct.mk R S A) 1) x)) (((TensorProduct.mk R S A) 1) y) ∈
    ↑(span S ↑(Submodule.map ((TensorProduct.mk R S A) 1) (𝒜 (i + j))))
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «1».«0»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![X 1, X 2] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![f₁, f₂] ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [subst]

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

Goal state before:
pp: case «1».«1»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![X 1, X 2] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![f₁, f₂] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [subst]

Goal state after:
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 : Γ
hg : ¬g = 0
n : ℕ
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0

Tactic:
by_cases hn : n = 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
n : ℕ
hn : n = 0
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0

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
n : ℕ
hn : ¬n = 0
⊢ ((powerSeriesFamily 0 f) n).coeff g = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] (![X 1, X 0] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![g, f] ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [subst]

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
F : FormalGroup R
inst✝ : F.IsComm
f g : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
hg : PowerSeries.HasSubst g
⊢ subst ![f, g] (![X 1, X 0] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![g, f] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [subst]

Goal state after: