mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x : A
⊢ ∀ (b : A),
    (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (x * b) =
      x • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) b +
        b • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) x

Tactic:
y

Goal state after:
case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (x * y) =
    x • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) y +
      y • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) x
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ((a.lcm b).factorization.prod fun a_1 b_1 ↦
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    (a.lcm b).factorization.prod fun x1 x2 ↦ x1 ^ x2

Tactic:
congr

Goal state after:
case e_g
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (fun a_1 b_1 ↦
      (if b.factorization a_1 ≤ a.factorization a_1 then a_1 ^ b_1 else 1) *
        if b.factorization a_1 ≤ a.factorization a_1 then 1 else a_1 ^ b_1) =
    fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
i✝ : ℕ
a✝ : i✝ ∈ (a.lcm b).factorization.support
⊢ i✝ ^ 0 = 1

Tactic:
rw [pow_zero]

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

Goal state before:
pp: case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), toLinearMap✝¹ (a * b) = a • toLinearMap✝¹ b + b • toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), toLinearMap✝¹ (a * b) = a • toLinearMap✝¹ b + b • toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ n.natAbs • a ^ ↑(n.natAbs - 1) • D a = n.natAbs • a ^ (↑n.natAbs - 1) • D a

Tactic:
congr

Goal state after:
case neg.inl.e_a.e_a.e_a
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
h : n = ↑n.natAbs
⊢ ↑(n.natAbs - 1) = ↑n.natAbs - 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
h : ExponentExists G
h' : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}.Nonempty
⊢ Nat.find h = Nat.find h'

Tactic:
congr

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
⊢ p ∈ comap (Pi.evalRingHom R i) '' ↑(basicOpen f) ↔ p ∈ ↑(basicOpen (Pi.single i f))

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
⊢ p ∈ comap (Pi.evalRingHom R i) '' ↑(basicOpen f) → p ∈ ↑(basicOpen (Pi.single i f))

case refine_2
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
⊢ p ∈ ↑(basicOpen (Pi.single i f)) → p ∈ comap (Pi.evalRingHom R i) '' ↑(basicOpen f)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
f : R i
⊢ IsOpen ((fun a ↦ comap (Pi.evalRingHom R i) a) '' (fun r ↦ ↑(basicOpen r)) f)

Tactic:
PrimeSpectrum.comap_evalRingHom_basicOpen

Goal state after:
case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
f : R i
⊢ IsOpen ↑(basicOpen (Pi.single i f))
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 ↦ x ^ x_1
⊢ IsCyclic G

Tactic:
refine ⟨f x, fun a ↦ ?_⟩

Goal state after:
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 ↦ x ^ x_1
a : G
⊢ ∃ a_1, (fun x_1 ↦ f x ^ x_1) a_1 = a
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
by
          rw [zpow_mul]
          apply H.zpow_mem
          exact mod_cast (Nat.find_spec hex).2

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // (orbitRel G α) y x } = card ↑(orbit G x)

Tactic:
congr

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : exponent (M j) = 0
⊢ exponent ((i : ι) → M i) = 0

Tactic:
rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
  push Not at hj ⊢
  peel hj with n hn _
  obtain ⟨m, hm⟩ := this
  refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
  simpa using congr_fun h j

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
⊢ basicOpen (↑a).1 ≤ basicOpen (↑b).1 ↔ a ≤ b

Tactic:
rw [← inf_eq_left, ← basicOpen_mul]

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
a b : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
⊢ basicOpen ((↑a).1 * (↑b).1) = basicOpen (↑a).1 ↔ a ≤ b
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ exponent ((i : ι) → M i) = univ.lcm fun x ↦ exponent (M x)

Tactic:
refine dvd_antisymm ?_ ?_
  · refine exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_
    ext i
    rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]
    apply dvd_trans (Monoid.order_dvd_exponent (m i))
    exact Finset.dvd_lcm (mem_univ i)
  · apply Finset.lcm_dvd fun i _ ↦ ?_
    exact MonoidHom.exponent_dvd (f := Pi.evalMonoidHom (M ·) i) (Function.surjective_eval i)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case mk.mk
p : ℕ
G : Type u_1
inst✝ : Group G
toSubgroup✝¹ : Subgroup G
isPGroup'✝¹ : IsPGroup p ↥toSubgroup✝¹
is_maximal'✝¹ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝¹ ≤ Q → Q = toSubgroup✝¹
toSubgroup✝ : Subgroup G
isPGroup'✝ : IsPGroup p ↥toSubgroup✝
is_maximal'✝ : ∀ {Q : Subgroup G}, IsPGroup p ↥Q → toSubgroup✝ ≤ Q → Q = toSubgroup✝
h :
  ↑{ toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    ↑{ toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }
⊢ { toSubgroup := toSubgroup✝¹, isPGroup' := isPGroup'✝¹, is_maximal' := is_maximal'✝¹ } =
    { toSubgroup := toSubgroup✝, isPGroup' := isPGroup'✝, is_maximal' := is_maximal'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (map (algebraMap R S) (reflect b.natDegree b * X ^ (1 + c.natDegree))) = 0

Tactic:
Polynomial.map_mul,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (map (algebraMap R S) (reflect b.natDegree b) * map (algebraMap R S) (X ^ (1 + c.natDegree))) = 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ Nat.card ↑(fixedPoints ↥↑P ↑(orbit G P)) = Nat.card ↑{⟨P, ⋯⟩}

Tactic:
congr

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
h : p ∣ Nat.card ↑(orbit G P)
⊢ fixedPoints ↥↑P ↑(orbit G P) = {⟨P, ⋯⟩}
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
x : Multiplicative ℤ
⊢ ∀ ⦃b : Multiplicative ℤ⦄, x < b → (intEquivOfZPowersEqTop g hg) x < (intEquivOfZPowersEqTop g hg) b

Tactic:
y

Goal state after:
G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
x y : Multiplicative ℤ
⊢ x < y → (intEquivOfZPowersEqTop g hg) x < (intEquivOfZPowersEqTop g hg) y
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : g < 1
x : Multiplicative ℤ
⊢ ∀ ⦃b : Multiplicative ℤ⦄, x < b → (intEquivOfZPowersEqTop g hg) b < (intEquivOfZPowersEqTop g hg) x

Tactic:
y

Goal state after:
G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : g < 1
x y : Multiplicative ℤ
⊢ x < y → (intEquivOfZPowersEqTop g hg) y < (intEquivOfZPowersEqTop g hg) x
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
this : DecidableEq ι
⊢ (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤

Tactic:
refine h.cons_induction ?_ ?_ <;> clear t h

Goal state after:
case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, ∑ i ∈ {a}, ↑(μ i) = 1) ↔ (↑{a}).Pairwise fun i j ↦ I i ⊔ I j = ⊤

case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    s.Nonempty →
      ((∃ μ, ∑ i ∈ s, ↑(μ i) = 1) ↔ (↑s).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
        ((∃ μ, ∑ i ∈ Finset.cons a s h, ↑(μ i) = 1) ↔ (↑(Finset.cons a s h)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx : sSup s ≤ a
⊢ ∃ s_1, (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = ⟨sSup s, hx⟩

Tactic:
rw [sSup_le_iff] at hx

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
⊢ ∃ s_1, (∀ x ∈ s_1, IsCompactElement x) ∧ sSup s_1 = ⟨sSup s, hx✝⟩
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ sSup (Subtype.val '' range f) = sSup s

Tactic:
congr

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ Subtype.val '' range f = s
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R ↥m ↔ IsAtom m

Tactic:
by
  rw [← Set.isSimpleOrder_Iic_iff_isAtom, isSimpleModule_iff]
  exact m.mapIic.isSimpleOrder_iff

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
x : M
⊢ ∀ {b : M}, x ∈ {x | ∃ a, a • x = 0} → b ∈ {x | ∃ a, a • x = 0} → x + b ∈ {x | ∃ a, a • x = 0}

Tactic:
y

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
x y : M
⊢ x ∈ {x | ∃ a, a • x = 0} → y ∈ {x | ∃ a, a • x = 0} → x + y ∈ {x | ∃ a, a • x = 0}
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_5
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
x✝ y : PolynomialModule R M✝
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
x : S
⊢ ∀ (y : R[X]) (z : PolynomialModule R M), (x • y) • z = x • y • z

Tactic:
y

Goal state after:
ι : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_5
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
x✝ y✝ : PolynomialModule R M✝
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
x : S
y : R[X]
⊢ ∀ (z : PolynomialModule R M), (x • y) • z = x • y • z
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_5
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
x✝ y✝ : PolynomialModule R M✝
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
x : S
y : R[X]
z : PolynomialModule R M
⊢ (x • y) • z = x • y • z

Tactic:
rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      ((⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n] ∘
          ⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))
        (single R j m) =
    single R (n + 1 + j) (r • m)

Tactic:
Function.comp_apply,

Goal state after:
case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        ((↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m)) =
    single R (n + 1 + j) (r • m)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x : R
⊢ ∀ (y : R),
    (monomial (n + 1)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
      (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
        (monomial (n + 1)) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
y

Goal state after:
case succ.refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
⊢ (monomial (n + 1)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
    (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
      (monomial (n + 1)) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (((coeffEquiv R).toFun m).sum fun i c ↦ r ^ i • s • c) = m.coeff.sum fun a b ↦ s • r ^ a • b

Tactic:
congr

Goal state after:
case refine_2.e_g
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (fun i c ↦ r ^ i • s • c) = fun a b ↦ s • r ^ a • b
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ ⨆ i ∈ S, torsionBy R M (q i) = ⨆ i ∈ S, torsionBySet R M ↑(Ideal.span {q i})

Tactic:
congr

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
⊢ (fun i ↦ ⨆ (_ : i ∈ S), torsionBy R M (q i)) = fun i ↦ ⨆ (_ : i ∈ S), torsionBySet R M ↑(Ideal.span {q i})
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ ⨆ (_ : x✝ ∈ S), torsionBy R M (q x✝) = ⨆ (_ : x✝ ∈ S), torsionBySet R M ↑(Ideal.span {q x✝})

Tactic:
congr

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
x✝ : ι
⊢ (fun h ↦ torsionBy R M (q x✝)) = fun h ↦ torsionBySet R M ↑(Ideal.span {q x✝})
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x x✝ y✝ : M
hx✝ : x✝ ∈ r • P
hy✝ : y✝ ∈ r • P
hx : x✝ ∈ N
hy : y✝ ∈ N
⊢ x✝ + y✝ ∈ N

Tactic:
| add _ _ _ _ hx hy =>

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ { coeff := f.coeff } ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))

Tactic:
← f.coeff.sum_single,

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ { coeff := f.coeff.sum Finsupp.single } ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))