mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : ¬FaithfulSMul R S
⊢ 0 = finrank R T

Tactic:
Module.finrank_eq_zero_of_not_faithfulSMul

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : ¬FaithfulSMul R S
⊢ 0 = 0

case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_4
inst✝⁵ : CommRing T
inst✝⁴ : IsDomain T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul S T
h : ¬FaithfulSMul R S
⊢ ¬FaithfulSMul R T
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
a : A
h : (a • 1) ⊗ₜ[R] m = 0
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 1

Tactic:
smul_eq_mul,

Goal state after:
case mp
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : FaithfullyFlat R A
m : M
f : R →ₗ[R] M := (LinearMap.lsmul R M).flip m
a : A
h : (a * 1) ⊗ₜ[R] m = 0
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor A f)) a) 1 = ((AlgebraTensorModule.curry 0) a) 1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - (↑a - ↑a * ↑b) = 1 - ↑a + (↑b - (↑b - ↑b * ↑a))

Tactic:
sub_sub_cancel,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - (↑a - ↑a * ↑b) = 1 - ↑a + ↑b * ↑a
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_4
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : v.IsMaximal
⊢ (algebraMap R K) y = (algebraMap R K) y * ((algebraMap R K) 1)⁻¹

Tactic:
rw [map_one, inv_one, mul_one]

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsOpen[inst✝] (range f) ↔ ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
· simp_rw [range_restrictPreimage]
    exact hU.isOpen_iff_coe_preimage

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ IsCompactElement s ↔
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i

Tactic:
CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
⊢ (∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1) ↔
    ∀ {ι : Type u_2} (U : ι → Set α), (∀ (i : ι), IsOpen[inst✝] (U i)) → ↑s ⊆ ⋃ i, U i → ∃ t, ↑s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Nontrivial (NonemptyCompacts α) ↔ Nontrivial α

Tactic:
simp_rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ IsGenericPoint (f x) (closure (f '' S))

Tactic:
rw [isGenericPoint_def, ← h.def, ← image_singleton, closure_image_closure hf]

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Set.range (comap (algebraMap R S)) = ↑(basicOpen r)

Tactic:
rw [localization_comap_range S (Submonoid.powers r)]

Goal state after:
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ {p | Disjoint ↑(Submonoid.powers r) ↑p.asIdeal} = ↑(basicOpen r)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h.h
G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
n✝ : ℕ
p✝ : 0 < n✝
this : ∀ (g : G), g ^ n✝ = 1
⊢ g ^ n✝ = 1

Tactic:
exact this g

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G ≠ 0 ↔ ExponentExists G

Tactic:
exponent

Goal state after:
G : Type u
inst✝ : Monoid G
⊢ (if h : ExponentExists G then Nat.find h else 0) ≠ 0 ↔ ExponentExists G
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
G_cyclic : IsCyclic G
k : ℕ
k_pos : k ≠ 0
k_lt_card_G : k < Nat.card G
⊢ ∃ a, a ^ k ≠ 1

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt k_lt_card_G)
  rcases G_cyclic with ⟨a, ha⟩
  use a
  contrapose! k_lt_card_G
  convert! orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G
  rw [← Nat.card_zpowers, eq_comm, card_eq_iff_eq_top, eq_top_iff]
  exact fun x _ ↦ ha x

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ Fintype.card α / n.gcd (Fintype.card α) * n.gcd (Fintype.card α) ∣ m * n.gcd (Fintype.card α)

Tactic:
conv_lhs =>
        rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
          ← orderOf_eq_card_of_forall_mem_zpowers hg]

Goal state after:
case a
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
x : α
hx : x ∈ {a | a ^ n = 1}
m : ℕ
hm : g ^ m = x
⊢ orderOf g ∣ m * n.gcd (Fintype.card α)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card ↥(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α)))) ≤ n

Tactic:
rw [Fintype.card_zpowers, orderOf_pow g, orderOf_eq_card_of_forall_mem_zpowers hg,
        Nat.card_eq_fintype_card]

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
m : ℕ
hm : Fintype.card α = n.gcd (Fintype.card α) * m
hm0 : 0 < m
⊢ Fintype.card α / (Fintype.card α).gcd (Fintype.card α / n.gcd (Fintype.card α)) ≤ n
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
⊢ False

Tactic:
obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)

Goal state after:
case refine_1
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
he : exponent G ≠ 0
h : ¬(Set.range orderOf).Finite
t : G
het : exponent G < orderOf t
⊢ False
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite : (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : t.prod id = 0
h : exponent G = 0
⊢ False

Tactic:
exact htpos.ne' this

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : a.val ≡ b.val [MOD Nat.card G]
⊢ a = b

Tactic:
← ZMod.natCast_eq_natCast_iff

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : ↑a.val = ↑b.val
⊢ a = b
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inl.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)

Tactic:
exact Or.inr ⟨p ^ n, by rw [pow_succ']⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
h : p₁.Coprime p₂
⊢ Disjoint H₁ H₂

Tactic:
by
  refine Subgroup.disjoint_def.mpr fun {g} hg₁ hg₂ ↦ ?_
  have ⟨k₁, hk₁⟩ := hH₁ ⟨g, hg₁⟩
  have hg₁ := Subgroup.orderOf_mk g _ ▸ orderOf_dvd_of_pow_eq_one hk₁
  have ⟨k₂, hk₂⟩ := hH₂ ⟨g, hg₂⟩
  have hg₂ := Subgroup.orderOf_mk g _ ▸ orderOf_dvd_of_pow_eq_one hk₂
  exact orderOf_eq_one_iff.mp <| Nat.eq_one_of_dvd_coprimes (h.pow k₁ k₂) hg₁ hg₂

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
hQ : IsPGroup p ↥Q
⊢ P ≤ Q → Q = P

Tactic:
hPQ

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
P : Subgroup G
hP1 : IsPGroup p ↥P
hP2 : ¬p ∣ P.index
Q : Subgroup G
hQ : IsPGroup p ↥Q
hPQ : P ≤ Q
⊢ Q = P
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 (reflect b.natDegree (map (algebraMap R S) b) * map (algebraMap R S) X ^ (1 + c.natDegree)) = 0

Tactic:
map_X,

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 (reflect b.natDegree (map (algebraMap R S) b) * X ^ (1 + c.natDegree)) = 0
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ a ^ (d / m) ∈ {a | orderOf a = m}

Tactic:
rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ closure ↑t = ⊤

Tactic:
rw [Finset.coe_preimage]

Goal state after:
G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
⊢ closure (Subtype.val ⁻¹' ↑s) = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
n : ℕ
hn : n < orderOf g
⊢ n ≠ 0 → (orderOf g).Coprime n

Tactic:
hn0

Goal state after:
case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
n : ℕ
hn : n < orderOf g
hn0 : n ≠ 0
⊢ (orderOf g).Coprime n
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
⊢ ¬p ∣ (↑P).index

Tactic:
intro h
  rw [P.index_eq_card] at h
  obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card' (G := G ⧸ (P : Subgroup G)) p h
  have h := IsPGroup.of_card (((Nat.card_zpowers x).trans hx).trans (pow_one p).symm)
  let Q := (zpowers x).comap (QuotientGroup.mk' (P : Subgroup G))
  have hQ : IsPGroup p Q := by
    apply h.comap_of_ker_isPGroup
    rw [QuotientGroup.ker_mk']
    exact P.2
  replace hp := mt orderOf_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)
  rw [← zpowers_eq_bot, ← Ne, ← bot_lt_iff_ne_bot, ←
    comap_lt_comap_of_surjective (QuotientGroup.mk'_surjective _), MonoidHom.comap_bot,
    QuotientGroup.ker_mk'] at hp
  exact hp.ne' (P.3 hQ hp.le)

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
⊢ False

Tactic:
let f := (ZMod.castHom (dvd_zero _) (ZMod 2)).toAddMonoidHom

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod 0)
h✝ : Infinite N
f : ZMod 0 →+ ZMod 2 := (ZMod.castHom ⋯ (ZMod 2)).toAddMonoidHom
⊢ False
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: M : Type u_4
inst✝² : AddCommGroup M
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Module R M
simple : IsSimpleModule R M
⊢ (Module.annihilator R M).IsMaximal

Tactic:
by
  have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple
  rwa [e.annihilator_eq, I.annihilator_quotient]

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

Goal state before:
pp: ι✝ : Type u_1
R : Type u_2
S : Type u_3
inst✝⁹ : Ring R
inst✝⁸ : Ring S
M✝ : Type u_4
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
m : Submodule R M✝
N : Type u_5
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι : Type u_7
inst✝³ : Finite ι
M : ι → Type u_6
inst✝² : (i : ι) → AddCommGroup (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), IsSemisimpleModule R (M i)
⊢ ⨆ i, (single R M i).range = ⊤

Tactic:
simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : IsSemisimpleRing R
I : Ideal R
⊢ ∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}

Tactic:
obtain ⟨J, h⟩ := exists_isCompl I
  obtain ⟨f, idem, rfl⟩ := I.isIdempotentElemEquiv.symm (I.isComplEquivProj ⟨J, h⟩)
  exact ⟨f 1, LinearMap.isIdempotentElem_map_one_iff.mpr idem, by
    rw [LinearMap.range_eq_map, ← Ideal.span_one, ← Ideal.submodule_span_eq, LinearMap.map_span,
      Set.image_one, Ideal.submodule_span_eq]⟩

Goal state after:
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
inst✝ : IsSemisimpleModule R M
f✝ : End (End R M) M
s : Finset M
x : ↥s →₀ M := Finsupp.equivFunOnFinite.symm fun x ↦ ↑x
w✝ : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w✝
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := (R ∙ x).projection w✝ h
f : End (End R (↥s →₀ M)) (↥s →₀ M) := (End.ringHomEndFinsupp ↥s) f✝
this : f (p • x) = f x
⊢ f x ∈ R ∙ x

Tactic:
← this,

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
f✝ : End (End R M) M
s : Finset M
x : ↥s →₀ M := Finsupp.equivFunOnFinite.symm fun x ↦ ↑x
w✝ : Submodule R (↥s →₀ M)
h : IsCompl (R ∙ x) w✝
p : (↥s →₀ M) →ₗ[R] ↥s →₀ M := (R ∙ x).projection w✝ h
f : End (End R (↥s →₀ M)) (↥s →₀ M) := (End.ringHomEndFinsupp ↥s) f✝
this : f (p • x) = f x
⊢ f (p • x) ∈ R ∙ x
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ↑(if hi : j = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ j), ⋯⟩) = u * ↑(μ j)

Tactic:
rw [dif_neg]

Goal state after:
case refine_2.mpr.refine_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ¬j = a
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1

Tactic:
· rintro ⟨hs, Hb⟩
    obtain ⟨μ, hμ⟩ := ih.mpr hs
    have := sup_iInf_eq_top fun b hb => Hb b hb (ne_of_mem_of_not_mem hb hat).symm
    rw [eq_top_iff_one, Submodule.mem_sup] at this
    obtain ⟨u, hu, v, hv, huv⟩ := this
    refine ⟨fun i => if hi : i = a then ⟨v, ?_⟩ else ⟨u * μ i, ?_⟩, ?_⟩
    · simp only [mem_iInf] at hv ⊢
      intro j hj ij
      rw [Finset.mem_cons, ← hi] at hj
      exact hv _ (hj.resolve_left ij)
    · have := Submodule.coe_mem (μ i)
      simp only [mem_iInf] at this ⊢
      intro j hj ij
      rcases Finset.mem_cons.mp hj with (rfl | hj)
      · exact mul_mem_right _ _ hu
      · exact mul_mem_left _ _ (this _ hj ij)
    · dsimp only
      rw [Finset.sum_cons, dif_pos rfl, add_comm]
      rw [← mul_one u] at huv
      rw [← huv, ← hμ, Finset.mul_sum]
      congr 1
      apply Finset.sum_congr rfl
      intro j hj
      rw [dif_neg]
      rintro rfl
      exact hat hj

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : i = 0
⊢ 1 ∈ I ^ i

pp: case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i

Tactic:
· subst h
      simp

Goal state after:
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : i = 0
⊢ (algebraMap R R) r ∈ I ^ i

pp: case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i

Tactic:
· subst h
      simp

Goal state after:
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
h : ¬i = 0
⊢ 0 ∈ I ^ i
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_1
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
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial (1 + n)) (r • s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
smul_eq_mul,

Goal state after:
case succ.refine_1
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
r : R
hr : r ∈ I
s : R
hs : s ∈ I ^ n
⊢ (monomial (1 + n)) (r * s) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) 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
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
⊢ torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i) = ⊥

Tactic:
← this,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
T : Finset ι
hT : T ⊆ S
i : ι
hi : i ∈ S
hiT : i ∉ T
this : torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = torsionBySet R M ↑(p i) ⊓ torsionBySet R M ↑(⨅ i ∈ T, p i)
⊢ torsionBySet R M ↑(p i ⊔ ⨅ i ∈ T, p i) = ⊥
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R 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'
f✝ : M →ₗ[R] M'
r : R
f g : PolynomialModule R M
e₁ : (eval ((algebraMap R R') r)) ((map R' f✝) f) = f✝ ((eval r) f)
e₂ : (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) g)
⊢ f✝ ((eval r) f) + (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) f) + f✝ ((eval r) g)

Tactic:
e₂

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

Goal state before:
pp: case add
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
f g : PolynomialModule S S
e₁ : (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
e₂ : (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g)
⊢ (eval x) ((map R (Algebra.linearMap S R)) f) + (aeval x) (equivPolynomial g) =
    (eval x) ((map R (Algebra.linearMap S R)) f) + (eval x) ((map R (Algebra.linearMap S R)) g)

Tactic:
e₂

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

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
x✝ y✝ : PolynomialModule R M
e₁ : (eval r ∘ₗ comp p) x✝ = (eval (Polynomial.eval r p)) x✝
e₂ : (eval r ∘ₗ comp p) y✝ = (eval (Polynomial.eval r p)) y✝
⊢ (eval (Polynomial.eval r p)) x✝ + (eval r ∘ₗ comp p) y✝ =
    (eval (Polynomial.eval r p)) x✝ + (eval (Polynomial.eval r p)) y✝

Tactic:
e₂

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
q : ι → R
hq : (↑S).Pairwise (IsCoprime on q)
hM : IsTorsionBySet R M ↑(⨅ a ∈ S, Ideal.span {q a})
x✝ : ↥S
⊢ torsionBy R M (q ↑x✝) = torsionBySet R M ↑(Ideal.span {q ↑x✝})

Tactic:
exact (torsionBySet_span_singleton_eq _ (R := R) (M := M)).symm

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I✝ : Ideal R
F F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I ^ (i + 1) • N ≤ I ^ i • N

Tactic:
rw [add_comm, pow_add, mul_smul]; exact Submodule.smul_le_right

Goal state after: