mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsRegular M as

Tactic:
isRegular_iff,

Goal state after:
case a
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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsWeaklyRegular M as ∧ ⊤ ≠ Ideal.ofList as • ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case b
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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsRegular M₂ bs

Tactic:
isRegular_iff,

Goal state after:
case b
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₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
| IsWeaklyRegular M₂ bs ∧ ⊤ ≠ Ideal.ofList bs • ⊤
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
r : R
rs : List R
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs

Tactic:
isRegular_iff,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ Ideal.ofList (r :: rs) • ⊤ ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs
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
r : R
rs : List R
⊢ IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ Ideal.ofList (r :: rs) • ⊤ ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs

Tactic:
isRegular_iff,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ Ideal.ofList (r :: rs) • ⊤ ↔
    IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs ∧ ⊤ ≠ Ideal.ofList rs • ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsRegular M (r :: rs)

Tactic:
isRegular_iff,

Goal state after:
case a
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ Ideal.ofList (r :: rs) • ⊤
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)

Tactic:
isRegular_iff,

Goal state after:
case b
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
| IsSMulRegular M r ∧
    IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) ∧
      ⊤ ≠ Ideal.ofList (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs) • ⊤
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ #s = #s - 1 + 1

Tactic:
grind

Goal state after:
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
⊢ ⊤ ≤ Subalgebra.map (map R f) ⊤

Tactic:
← (AlgHom.range_eq_top (RingCon.mkₐ R (ringCon R N))).mpr mkAlgHom_surjective,

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
⊢ (RingCon.mkₐ R (ringCon R N)).range ≤ Subalgebra.map (map R f) ⊤
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
x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow 1 (e.symm x✝)) = x✝

Tactic:
rw [dpow_one, RingEquiv.apply_symm_apply]
    rwa [I.symm_apply_mem_of_equiv_iff, h]

Goal state after:
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✝ : IsArtinian R M
r : R
rs : List R
h : IsRegular M (r :: rs)
⊢ r :: rs = []

Tactic:
isRegular_iff,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsWeaklyRegular M (r :: rs) ∧ ⊤ ≠ Ideal.ofList (r :: rs) • ⊤
⊢ r :: rs = []
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:
dif_pos hx

Goal state after:
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
⊢ ⋯.choose ∈ I
Module: Mathlib.RingTheory.DividedPowers.Padic

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

Tactic:
rw [hx0]
    simp [inverse_eq_inv', coe_zero, ne_eq, hn, not_false_eq_true, zero_pow, mul_zero,
      norm_zero, inv_nonneg, cast_nonneg]

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)!
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
by
  by_cases! hkm : m + k < n
  · exact dpow_mul_of_add_lt hn_fac hkm hx
  · have hxmk : x ^ (m + k) = 0 := Ideal.pow_eq_zero_of_mem hnI hkm hx
    rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∉ Ideal.span {↑p}
⊢ 0 = 0

Tactic:
rfl

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ hJ.IsSubDPIdeal (Ideal.map f K)

Tactic:
Ideal.map,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
K : Ideal A
hK : hI.IsSubDPIdeal K
⊢ hJ.IsSubDPIdeal (span (⇑f '' ↑K))
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J J' : hI.SubDPIdeal
⊢ ⟨(J ⊔ J').carrier, ⋯⟩ = ⟨J.carrier, ⋯⟩ ⊔ ⟨J'.carrier, ⋯⟩

Tactic:
rfl

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 J' : hI.SubDPIdeal
⊢ ⟨(J ⊓ J').carrier, ⋯⟩ = ⟨J.carrier, ⋯⟩ ⊓ ⟨J'.carrier, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
this : ∀ (J : hI.SubDPIdeal), ↑(⨆ (_ : J ∈ S), ⟨J.carrier, ⋯⟩) = ⨆ (_ : J ∈ S), ↑⟨J.carrier, ⋯⟩
⊢ ⨆ a ∈ S, ↑a = ⨆ i ∈ S, i.carrier

Tactic:
rfl

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ⊤.carrier ⊓ J.carrier = I ⊓ ↑⟨J.carrier, ⋯⟩

Tactic:
rfl

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
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
⊢ ⊤.carrier = I

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : IsNilpotent a
hb : IsNilpotent b
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
isNilpotent_iff_eps_dvd

Goal state after:
case inr.inr
K : Type u_2
inst✝ : DivisionRing K
a b : K[ε]
ha : ε ∣ a
hb : ε ∣ b
⊢ ∃ c, a * c = b ∨ b * c = a
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
this✝¹ : Etale S U
this✝ : Module.Finite S U
this : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n + 1
p : PrimeSpectrum S
⊢ Module.rankAtStalk U p = n

Tactic:
grind

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
x : ↥P.ker
⊢ (↑P.cotangentExtendScalarsEquiv.symm (Cotangent.mk x)).val = ((Cotangent.map P.toExtendScalars) (Cotangent.mk x)).val

Tactic:
rfl

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.h1CotangentEquivCotangent ∘ₗ Algebra.H1Cotangent.map R P.Ring S S =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

Tactic:
by
  rw [h1CotangentEquivCotangent, LinearEquiv.coe_trans, LinearEquiv.coe_trans,
    h1CotangentExtendScalarsEquiv_symm_toLinearMap, h1CotangentEquivOfSurjective_toLinearMap,
    LinearMap.comp_assoc, LinearMap.comp_assoc, Algebra.H1Cotangent.map,
    ← (H1Cotangent.map P.extendScalars.defaultHom).restrictScalars_self, ← H1Cotangent.map_comp,
    eq_comm, ← LinearEquiv.toLinearMap_symm_comp_eq, cotangentExtendScalarsEquiv_symm_toLinearMap,
    ← LinearMap.comp_assoc, Cotangent.map_comp_h1Cotangentι, LinearMap.restrictScalars_self,
    LinearMap.comp_assoc, ← (H1Cotangent.map P.toExtendScalars).restrictScalars_self,
    ← H1Cotangent.map_comp, H1Cotangent.map_eq]

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
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.IsDPMorphism hJ f
⊢ hI.IsSubDPIdeal (RingHom.ker f ⊓ I)

Tactic:
by
  rw [isSubDPIdeal_inf_iff]
  simp only [isDPMorphism_def] at hf
  intro n a b ha hb
  simp only [RingHom.sub_mem_ker_iff, ← hf.2 a ha, ← hf.2 b hb]
  exact congr_arg _

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
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'

Tactic:
Ideal.map,

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.IsDPMorphism hK f
hIK' : hI.IsDPMorphism hK' f
⊢ span (⇑f '' ↑I) ≤ hK.dpEqualizer hK'
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case hnc
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 : ℕ
x : B
hx' : x ∉ J
⊢ ¬∃ a, f ↑a = x

Tactic:
rintro ⟨⟨a, ha⟩, rfl⟩

Goal state after:
case hnc
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, ha⟩ ∉ J
⊢ False
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
G : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulSemiringAction G S
inst✝⁶ : SMulCommClass G R S
Q : Ideal S
inst✝⁵ : Finite G
inst✝⁴ : Algebra.IsInvariant R S G
inst✝³ : Q.IsPrime
inst✝² : Finite (S ⧸ Q)
Q' : Ideal S
inst✝¹ : Q'.IsPrime
inst✝ : Finite (S ⧸ Q')
H : Ideal.under R Q = Ideal.under R Q'
hP : (Ideal.under R Q).IsPrime
h₂ : Ideal.under R Q = Ideal.under R Q'
⊢ arithFrobAt R G Q = ⋯.choose ⟨Q, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
G : Type u_3
inst✝⁸ : Group G
inst✝⁷ : MulSemiringAction G S
inst✝⁶ : SMulCommClass G R S
Q : Ideal S
inst✝⁵ : Finite G
inst✝⁴ : Algebra.IsInvariant R S G
inst✝³ : Q.IsPrime
inst✝² : Finite (S ⧸ Q)
Q' : Ideal S
inst✝¹ : Q'.IsPrime
inst✝ : Finite (S ⧸ Q')
H : Ideal.under R Q = Ideal.under R Q'
hP : (Ideal.under R Q').IsPrime
h₁ : Ideal.under R Q' = Ideal.under R Q
⊢ arithFrobAt R G Q' = ⋯.choose ⟨Q', ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
k : ℕ
A : Type w
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
N : G(k, A ⊗[R] M; A)
⊢ (map f N).toSubmodule = (baseChangeMkQ B N.toSubmodule).ker

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst✝² : Algebra A B := ⋯
algInst✝¹ : Algebra B C := ⋯
algInst✝ : Algebra A C := ⋯
⊢ algebraMap A C = (algebraMap B C).comp (algebraMap A B)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ f ↑(u ^ (n✝ + 1))⁻¹ = ↑((Units.map ↑f) (u ^ (n✝ + 1)))⁻¹

Tactic:
rfl

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

Goal state before:
pp: case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : (invOneSubPow S d).inv = (1 - X) ^ d
⊢ (invOneSubPow S (d + 1)).inv = (1 - X) ^ (d + 1)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
σ : Type u_5
F : FormalGroup R
x y : F.Point σ
⊢ ↑(x + y) = subst ![↑x, ↑y] F.toPowerSeries

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
⊢ n ≠ 0

Tactic:
exact Nat.ne_zero_of_lt hn

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
⊢ (g ∈ Function.support fun g ↦ ∑ᶠ (i : α), (s i).coeff g) → g ∈ ⋃ a, (s a).support

Tactic:
contrapose
      rw [Set.mem_iUnion, not_exists, Function.mem_support, Classical.not_not]
      simp_rw [mem_support, Classical.not_not]
      intro h
      rw [finsum_congr h, finsum_zero]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inl
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
ι : Type ?u.21
inst✝ : DecidableEq ι
x : R⟦Γ⟧
a : ι
this : (Pi.single a x a).support.IsPWO
⊢ (Pi.single a x a).support ⊆ (Pi.single a x a).support

Tactic:
rfl

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : ¬d 0 = 0
⊢ 1 = d 0 → (coeff d) F.toPowerSeries = 0

Tactic:
grind

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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ ![0, 0] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
hd₀ : ¬d 1 = 0
⊢ 1 = d 1 → (coeff d) F.toPowerSeries = 0

Tactic:
grind

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

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
⊢ ∑ ij ∈ Finset.antidiagonal ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 =
    ∑ x ∈ HasAntidiagonal.antidiagonal n, f.coeff x.1 * g.coeff x.2

Tactic:
refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
      sum_filter_ne_zero _

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝ : Semiring R
f g : R⟦ℕ⟧
n : ℕ
⊢ {x ∈ Finset.antidiagonal ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ HasAntidiagonal.antidiagonal n | f.coeff x.1 * g.coeff x.2 ≠ 0}
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a b : A
⊢ ↑{ val := ↑1, inv := (antipode R) ↑1, val_inv := ⋯, inv_val := ⋯ } = ↑1

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a✝ b✝ : A
a b : GroupLike R A
⊢ ↑{ val := ↑(a * b), inv := (antipode R) ↑(a * b), val_inv := ⋯, inv_val := ⋯ } =
    ↑({ val := ↑a, inv := (antipode R) ↑a, val_inv := ⋯, inv_val := ⋯ } *
        { val := ↑b, inv := (antipode R) ↑b, val_inv := ⋯, inv_val := ⋯ })

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case zero
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')⁻¹ʳ
⊢ c 0 ≡ a₀ [SMOD I]

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (f.toLinearMap ∘ₗ antipode R) * toConv ((toConv LinearMap.id).ofConv ∘ₗ f.toLinearMap)).ofConv =
    (toConv (f.toLinearMap ∘ₗ antipode R) * toConv f.toLinearMap).ofConv

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv (f.toLinearMap ∘ₗ antipode R) * toConv f.toLinearMap).ofConv =
    (toConv ((↑f).toLinearMap ∘ₗ (toConv (antipode R)).ofConv) *
        toConv ((↑f).toLinearMap ∘ₗ (toConv LinearMap.id).ofConv)).ofConv

Tactic:
rfl

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

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ⤳ q
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q

Tactic:
← PrimeSpectrum.le_iff_specializes

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ≤ q
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv ((toConv LinearMap.id).ofConv ∘ₗ f.toLinearMap) * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv =
    (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : HopfAlgebra R A
inst✝ : HopfAlgebraStruct R B
f : A →ₐc[R] B
hf : Function.Surjective ⇑f
hS : antipode R ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ antipode R
⊢ (toConv f.toLinearMap * toConv (f.toLinearMap ∘ₗ antipode R)).ofConv =
    (toConv ((↑f).toLinearMap ∘ₗ (toConv LinearMap.id).ofConv) *
        toConv ((↑f).toLinearMap ∘ₗ (toConv (antipode R)).ofConv)).ofConv

Tactic:
rfl

Goal state after: