mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inl
b : ℕ
⊢ factorizationLCMRight 0 b ∣ b

pp: case inr
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight b ∣ b

Tactic:
· simp [factorizationLCMRight]

Goal state after:
case inr
a b : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight b ∣ b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Tactic:
or_iff_not_imp_left,

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → ¬x ≤ I → y ≤ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
S_empty : ⋂ i, S i = ∅
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
⊢ ∃ u, ⋂ i ∈ u, S i = ∅

Tactic:
hI,

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
ι✝ : Type u
S : ι✝ → Set (PrimeSpectrum R)
S_closed : ∀ (i : ι✝), IsClosed (S i)
I : ι✝ → Ideal R
hI : ∀ (i : ι✝), S i = zeroLocus ↑(I i)
S_empty : ⋂ i, zeroLocus ↑(I i) = ∅
⊢ ∃ u, ⋂ i ∈ u, zeroLocus ↑(I i) = ∅
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ {I | I.IsMaximal}
hMI : id M ≤ I
⊢ I.IsMaximal

Tactic:
← hM.eq_of_le hI.1 hMI

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
M : Ideal R
hM : M ∈ {I | I.IsMaximal}
hMI : id M ≤ I
⊢ M.IsMaximal
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: 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
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
⊢ (↑e.symm).compDer ((↑e).compDer.toFun D) = D

Tactic:
by ext a; exact e.symm_apply_apply (D a)

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
⊢ PrimeSpectrum (R × S) ≃ₜ PrimeSpectrum R ⊕ PrimeSpectrum S

Tactic:
by
  refine ((primeSpectrumProd R S).symm.toHomeomorphOfIsInducing ?_).symm
  refine (IsClosedEmbedding.of_continuous_injective_isClosedMap ?_
    (Equiv.injective _) ?_).isInducing
  · rw [continuous_sum_dom]
    simp only [Function.comp_def, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
    exact ⟨continuous_comap _, continuous_comap _⟩
  · simp_rw [isClosedMap_sum, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
    exact ⟨isClosedEmbedding_comap_fst.isClosedMap, isClosedEmbedding_comap_snd.isClosedMap⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • b • D a + a • a • D b = a • a • D b + a • b • D a

Tactic:
add_comm

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • a • D b + a • b • D a = a • a • D b + a • b • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ p.asIdeal.primeCompl

Tactic:
← this

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ { asIdeal := q, isPrime := prime }.asIdeal.primeCompl
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
simpa

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
⊢ H = ⊥ ∨ H = ⊤

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero hp.1.ne_zero

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
hp : Fact (Nat.Prime (Nat.card G))
this : Finite G
⊢ H = ⊥ ∨ H = ⊤
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : ¬n % exponent G = 0
⊢ False

Tactic:
← Ne,

Goal state after:
case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
hG : ∀ (g : G), g ^ n = 1
h : n % exponent G ≠ 0
⊢ False
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
e f : R
mul : e * f = 0
add : e + f = 1
p : PrimeSpectrum R
this : e ∉ p.asIdeal ↔ f ∈ p.asIdeal
⊢ p ∈ ↑(basicOpen e) ↔ p ∈ zeroLocus {f}

Tactic:
simpa

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k

Tactic:
simp_rw [isPGroup_iff_orderOf_dvd_pow, Nat.dvd_prime_pow Fact.out]
  exact forall_congr' fun g ↦ ⟨by grind, .imp <| by grind⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ a * (a * b) * b = a ^ 2 * b ^ 2

Tactic:
by simp [pow_two, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : Monoid G
inst✝ : IsCancelMul G
a b : G
h : ∀ (g : G), g ^ 2 = 1
⊢ (a * b) ^ 2 = a * (b * a) * b

Tactic:
by simp [pow_two, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
h1 : ¬Nat.card ↥H = 0
h2 : ¬H.index = 0
⊢ Nat.card ↥H * H.index ≠ 0

Tactic:
exact mul_ne_zero h1 h2

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
⊢ rank ↥(closure ↑s) ≤ s.card

Tactic:
by
  classical
  let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
    rw [Finset.coe_preimage]
    exact closure_preimage_eq_top (s : Set G)
  apply (rank_le ht).trans
  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le
  apply Subtype.coe_injective.injOn

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ IsLocalHom f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

Tactic:
rw [this, PrimeSpectrum.ext_iff]

Goal state after:
R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
this : IsLocalHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R ↔
    (PrimeSpectrum.comap f (closedPoint S)).asIdeal = (closedPoint R).asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U

Tactic:
· rintro rfl
    exact TopologicalSpace.Opens.mem_top _

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

Goal state before:
pp: case inr
A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Nonempty (A ≃+o ℤ)

Tactic:
exact this (g := -g) (by simpa using! neg_surjective.comp hs) (by grind) (by grind)

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

Goal state before:
pp: G : Type u_4
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
⊢ IsCyclic G ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
by
  rw [← isAddCyclic_additive_iff, LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int,
    OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : ¬zpowers x = ⊥
⊢ False

Tactic:
← Ne,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : zpowers x ≠ ⊥
⊢ False
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
g : G ⧸ torsion G
hne : g ≠ 1
hfin : IsOfFinOrder g
⊢ g = 1

Tactic:
obtain ⟨g⟩ := g

Goal state after:
case mk
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
g✝ : G ⧸ torsion G
g : G
hne : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ≠ 1
hfin : IsOfFinOrder (Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g)
⊢ Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)

Tactic:
have : Function.Injective (MulAut.conj (n * g)).toMonoidHom := (MulAut.conj (n * g)).injective

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
⊢ Nat.card ↥(Subgroup.map (normalizer ↑H).subtype (comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x))) =
    p ^ (n + 1)

Tactic:
by
    show Nat.card (Subgroup.map (normalizer (H : Set G)).subtype
      (comap (mk' (H.subgroupOf (normalizer H))) (Subgroup.zpowers x))) = p ^ (n + 1)
    suffices Nat.card (Subtype.val ''
      ((zpowers x).comap (mk' (H.subgroupOf (normalizer H))) : Set (normalizer H))) = p ^ (n + 1)
      by convert! this using 2
    rw [Nat.card_image_of_injective Subtype.val_injective
        ((zpowers x).comap (mk' (H.subgroupOf (normalizer H))) : Set (normalizer (H : Set G))),
      pow_succ, ← hH, Nat.card_congr hequiv, ← hx, ← Nat.card_zpowers, ← Nat.card_prod]
    exact Nat.card_congr
      (preimageMkEquivSubgroupProdSet (H.subgroupOf (normalizer H)) (zpowers x))

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Fintype G
p k : ℕ
hp : Nat.Prime p
h : p ^ k ∣ Nat.card G
this : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ k
g : G
hg✝ : g ∈ (↑H \ {1}).toFinset
hg : g ∈ H
hg1 : g ≠ 1
⊢ ⟨g, hg⟩ ≠ 1

Tactic:
simpa

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h : ϕ • ↑P = Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G) ϕ) ↑P
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P

Tactic:
← pointwise_smul_def,

Goal state after:
G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h : ↑(ϕ • P) = Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G) ϕ) ↑P
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : 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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1

Tactic:
add_comm

Goal state after:
ι : 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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ (eraseLast s).last ≤ last s

Tactic:
simp [eraseLast, last, s.strictMono.le_iff_le, Fin.le_iff_val_le_val]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : ι → Submodule R M
hp : ∀ (i : ι), IsSemisimpleModule R ↥(p i)
hp' : ⨆ i, p i = ⊤
⊢ ⨆ i ∈ Set.univ, p i = ⊤

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
⊢ (eraseLast s).head ≤ x

Tactic:
simpa

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

Goal state before:
pp: case refine_2.mpr.refine_3
ι : 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 + v = 1
⊢ ↑⟨v, ⋯⟩ + ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = 1

Tactic:
add_comm

Goal state after:
case refine_2.mpr.refine_3
ι : 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 + v = 1
⊢ ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) + ↑⟨v, ⋯⟩ = 1
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 : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
e : n' ≤ n
this : I ^ (1 + n - n') • F.N n' ≤ I • F.N n
⊢ (↑(l ⟨single R n' m, ⋯⟩)).coeff (n + 1 - n') • m ∈ I • F.N n

Tactic:
add_comm

Goal state after:
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
n₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
e : n' ≤ n
this : I ^ (n + 1 - n') • F.N n' ≤ I • F.N n
⊢ (↑(l ⟨single R n' m, ⋯⟩)).coeff (n + 1 - n') • m ∈ I • F.N n
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_1
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
⊢ ∀ i ≤ n,
    single R i '' ↑(F.N i) ⊆
      ↑((fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) m)

Tactic:
intro i hi

Goal state after:
case mp.refine_1
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ single R i '' ↑(F.N i) ⊆
    ↑((fun n₀ ↦ Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) m)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
this :
  Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
⊢ (Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))).FG

Tactic:
← this

Goal state after:
case mpr
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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
this :
  Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
⊢ (Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s)).FG
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : ↑(M.obj U)
⊢ (ConcreteCategory.hom (M.map (i ≫ j))) x = (ConcreteCategory.hom (M.map j)) ((ConcreteCategory.hom (M.map i)) x)

Tactic:
rw [M.map_comp]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : ↑(M.obj U)
⊢ (ConcreteCategory.hom
        (M.map i ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).map (M.map j) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map i)) (RingCat.Hom.hom (R.map j))
                    (RingCat.Hom.hom (R.map (i ≫ j))) ⋯).inv.app
              (M.obj W)))
      x =
    (ConcreteCategory.hom (M.map j)) ((ConcreteCategory.hom (M.map i)) x)
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Tactic:
have := congr_app (associativity F m₁ m₂ m₃) X

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
this :
  (μ F m₁ m₂ ▷ F.obj m₃ ≫ μ F (m₁ ⊗ m₂) m₃ ≫ F.map (α_ m₁ m₂ m₃).hom).app X =
    ((α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫ F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  (Discrete.natTrans fun X ↦ (fun i ↦ f i) X.as).app { as := i } ≫
      colimit.ι (Discrete.functor fun i ↦ Y i) { as := i } =
    (Discrete.natTrans fun X ↦ (fun i ↦ g i) X.as).app { as := i } ≫
      colimit.ι (Discrete.functor fun i ↦ Y i) { as := i }
⊢ f i ≫ colimit.ι (Discrete.functor Y) { as := i } = g i ≫ colimit.ι (Discrete.functor Y) { as := i }

Tactic:
simpa

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
this : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 = x
⊢ x ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
← this

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : (TensorProduct.lmul' R) x = 0
this : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 = x
⊢ x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)