mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sdiff.insert
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s✝¹ : Set X
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
s✝ t : Set ι
ht : t.Finite
hV : ⋃ i ∈ t, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
i : ι
s : Set ι
hi : i ∉ s
hs : s.Finite
ih : ∀ (hU : ⋃ i ∈ s, b i ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}), P (⋃ i ∈ s, b i \ ⋃ i ∈ t, b i) ⋯
hU : ⋃ i_1 ∈ insert i s, b i_1 ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (⋃ i_1 ∈ insert i s, b i_1 \ ⋃ i ∈ t, b i) ⋯

Tactic:
| @insert i s hi hs ih =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ l.toList[0] = PrimeSpectrum.comap (algebraMap R S) (RelSeries.toList L)[0]

Tactic:
List.getElem_map_rev (PrimeSpectrum.comap (algebraMap R S)),

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ l.toList[0] = (List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L))[0]
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: 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
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) = 0

Tactic:
← Ideal.mem_bot,

Goal state after:
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
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
⊢ (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) ∈ ⊥
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: 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
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f x) * ↑(f y) = 0

Tactic:
← Ideal.mem_bot,

Goal state after:
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
hI✝ : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
x y : A
⊢ ↑(f x) * ↑(f y) ∈ ⊥
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: ⊢ OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Flat

Tactic:
by
  introv R h
  algebraize_only [f]
  rw [RingHom.Flat]
  apply Module.flat_of_isLocalized_maximal S S (fun P ↦ Localization.AtPrime P)
    (fun P ↦ Algebra.linearMap S _)
  intro P _
  algebraize_only [Localization.localRingHom (Ideal.comap f P) P f rfl]
  have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
  replace h : Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) := h ..
  exact Module.Flat.trans R (Localization.AtPrime <| Ideal.comap f P) (Localization.AtPrime P)

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

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : (Hom.hom f).Flat
hg : Function.Injective ⇑(ConcreteCategory.hom g)
algInst✝¹ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑T := (Hom.hom g).toAlgebra
algebraizeInst✝ : Module.Flat ↑R ↑S
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inl f g))

Tactic:
have : _ = pushout.inl f g := (CommRingCat.isPushout_tensorProduct R S T).inl_isoPushout_hom

Goal state after:
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
hf : (Hom.hom f).Flat
hg : Function.Injective ⇑(ConcreteCategory.hom g)
algInst✝¹ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑R ↑T := (Hom.hom g).toAlgebra
algebraizeInst✝ : Module.Flat ↑R ↑S
this : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ⋯.isoPushout.hom = pushout.inl f g
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushout.inl f g))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Set.range (comap (RingHom.snd R S)) = zeroLocus ↑(RingHom.ker (RingHom.snd R S))

Tactic:
refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨I, hI, rfl⟩; exact Ideal.comap_mono bot_le
  obtain ⟨p, hp, eq⟩ | ⟨p, hp, eq⟩ := p.1.ideal_prod_prime.mp p.2
  · refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
    simpa [eq] using h (show (1, 0) ∈ RingHom.ker (RingHom.snd R S) by simp)
  · exact ⟨⟨p, hp⟩, PrimeSpectrum.ext <| by simpa [Ideal.prod] using eq.symm⟩

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
⊢ IsPGroup p H

Tactic:
by
  refine fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => ?_) (hG g)
  rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]

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 α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : 1 < Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
Finite.one_lt_card_iff_nontrivial

Goal state after:
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 α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℤ
⊢ ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
by
  simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
apply dvd_trans (Monoid.order_dvd_exponent (m i))

Goal state after:
case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ exponent (M i) ∣ univ.lcm fun x ↦ exponent (M x)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsIntegral
s : Set (PrimeSpectrum S)
hs : IsClosed s
y : PrimeSpectrum R
x : PrimeSpectrum S
hx : x ∈ s
e : comap f x ⤳ y
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.IsIntegral R S
q : Ideal S
hq₁ : q ≥ x.asIdeal
hq₂ : q.IsPrime
hq₃ : Ideal.comap (algebraMap R S) q = y.asIdeal
⊢ y ∈ comap f '' s

Tactic:
refine ⟨⟨q, hq₂⟩, ((le_iff_specializes _ ⟨q, hq₂⟩).mp hq₁).mem_closed hs hx,
    PrimeSpectrum.ext hq₃⟩

Goal state after:
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)
⊢ fixedPoints ↥↑P ↑(orbit G P) = {⟨P, ⋯⟩}

Tactic:
Set.eq_singleton_iff_unique_mem

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)
⊢ ⟨P, ⋯⟩ ∈ fixedPoints ↥↑P ↑(orbit G P) ∧ ∀ x ∈ fixedPoints ↥↑P ↑(orbit G P), x = ⟨P, ⋯⟩
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
⊢ ¬p ∣ (↑Q₀).index * (comap f ↑P).index

Tactic:
P.index_comap_of_surjective hf

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
⊢ ¬p ∣ (↑Q₀).index * (↑P).index
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
⊢ torsion G ≤ Subgroup.comap f (torsion H)

Tactic:
by
  intro x
  exact f.isOfFinOrder

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ ↑(mapSurjective hf (hpQ.toSylow hQ)) = ↑P

Tactic:
Sylow.coe_mapSurjective,

Goal state after:
case h
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
hPQ : map f Q ≤ ↑P
hpQ : IsPGroup p ↥Q
hQ : ¬p ∣ Q.index
⊢ map f ↑(hpQ.toSylow hQ) = ↑P
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : {x | a ⋖ x}.Finite
⊢ ∃ b, a ⋖ b ∧ (Set.Ici b).Infinite

Tactic:
by
  by_contra! h
  refine ((hfin.biUnion (t := Set.Ici) (by simpa using h)).subset (fun b hb ↦ ?_)).not_infinite
    (ha.sdiff (Set.finite_singleton a))
  obtain ⟨x, hax, hxb⟩ := ((show a ≤ b from hb.1).lt_of_ne (Ne.symm hb.2)).exists_covby_le
  exact Set.mem_biUnion hax hxb

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_1
ι : 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, ⋯⟩
⊢ ∀ x ∈ range f, IsCompactElement x

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 (range f) = ⟨sSup s, hx✝⟩

Tactic:
· rintro - ⟨⟨y, hy⟩, hy', rfl⟩
    exact isCompactElement (hs _ hy)

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, ⋯⟩
⊢ sSup (range f) = ⟨sSup s, hx✝⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G✝ : Type u_2
G' : Type u_3
a : α
G : Type u_4
inst✝¹ : Group G
inst✝ : IsCyclic G
⊢ IsCyclic (WithZero G)ˣ

Tactic:
apply isCyclic_of_injective (G := (WithZero G)ˣ) (WithZero.unitsWithZeroEquiv).toMonoidHom
  apply Equiv.injective

Goal state after:
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 ↑↑(comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x)) =
    Nat.card (↥(H.subgroupOf (normalizer ↑H)) × ↥(zpowers x))

Tactic:
exact Nat.card_congr
      (preimageMkEquivSubgroupProdSet (H.subgroupOf (normalizer H)) (zpowers x))

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

Goal state before:
pp: case refine_2.mp
ι : 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μ : ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1
⊢ ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤

Tactic:
rw [Finset.sum_cons] at hμ

Goal state after:
case refine_2.mp
ι : 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
⊢ ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Tactic:
refine ⟨H', H'H, ?_⟩

Goal state after:
G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
m : ℕ
hmk : p ^ m ≤ k
hkm : k < p ^ (m + 1)
H' : Subgroup G
H'H : H' ≤ H
H'card : Nat.card ↥H' = p ^ m
⊢ Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
k p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hk : k ≤ Nat.card ↥H
hk₀ : k ≠ 0
⊢ ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'

Tactic:
obtain ⟨m, hmk, hkm⟩ : ∃ s, p ^ s ≤ k ∧ k < p ^ (s + 1) :=
    exists_nat_pow_near (Nat.one_le_iff_ne_zero.2 hk₀) hp.one_lt
  obtain ⟨H', H'H, H'card⟩ := exists_subgroup_le_card_pow_prime_of_le_card hp h (hmk.trans hk)
  refine ⟨H', H'H, ?_⟩
  simpa only [pow_succ', H'card] using And.intro hmk hkm

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
⊢ Nat.card ↥↑P = p ^ (Nat.card G).factorization p

Tactic:
obtain ⟨n, heq : Nat.card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'
  refine Nat.dvd_antisymm ?_ (P.pow_dvd_card_of_pow_dvd_card (Nat.ordProj_dvd _ p))
  rw [heq, ← hp.out.pow_dvd_iff_dvd_ordProj (show Nat.card G ≠ 0 from Nat.card_pos.ne'), ← heq]
  exact P.1.card_subgroup_dvd_card

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : ℕ) (_hi : i + 1 < (toList s).length), (toList s)[i] < (toList s)[i + 1]

Tactic:
s.toList_getElem

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : ℕ) (_hi : i + 1 < (toList s).length), s.toFun ⟨i, ⋯⟩ < s.toFun ⟨i + 1, ⋯⟩
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
⊢ IsSimpleModule R M ↔ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
  · have := IsSimpleModule.nontrivial R M
    have ⟨m, hm⟩ := exists_ne (0 : M)
    exact ⟨_, ker_toSpanSingleton_isMaximal R hm,
      ⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩
  · convert! congr equiv; rwa [isSimpleModule_iff_isCoatom]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionOf R M 0 = ⊤

Tactic:
by simp [torsionOf]

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

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h : ∀ (x : AEval R M a), (f ∘ₗ ↑(of R M a).symm) ((C k * X ^ n) • x) = (C k * X ^ n) • (f ∘ₗ ↑(of R M a).symm) x
m : AEval R M a
⊢ (f ∘ₗ ↑(of R M a).symm) ((C k * X ^ (n + 1)) • m) = (C k * X ^ (n + 1)) • (f ∘ₗ ↑(of R M a).symm) m

Tactic:
LinearMap.comp_apply,

Goal state after:
R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h : ∀ (x : AEval R M a), f (↑(of R M a).symm ((C k * X ^ n) • x)) = (C k * X ^ n) • f (↑(of R M a).symm x)
m : AEval R M a
⊢ f (↑(of R M a).symm ((C k * X ^ (n + 1)) • m)) = (C k * X ^ (n + 1)) • f (↑(of R M a).symm m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ (eval r ∘ₗ comp p) (single R i m) = (eval (Polynomial.eval r p)) (single R i m)

Tactic:
LinearMap.comp_apply,

Goal state after:
case single
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ (eval r) ((comp p) (single R i m)) = (eval (Polynomial.eval r p)) (single R i m)
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
⊢ Submodule.span (↥(reesAlgebra I)) (⋃ i, single R i '' ↑(F.N i)) = F.submodule

Tactic:
by
  rw [← Submodule.span_closure, submodule_closure_single, Submodule.coe_toAddSubmonoid]
  exact Submodule.span_eq (Filtration.submodule F)

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 : 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')
⊢ (fun a₁ b ↦ (b • ↑a₁).coeff (n + 1)) ⟨single R n' m, ⋯⟩ (l ⟨single R n' m, ⋯⟩) ∈ I • F.N n

Tactic:
dsimp only [Subtype.coe_mk]

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')
⊢ (l ⟨single R n' m, ⋯⟩ • single R n' m).coeff (n + 1) ∈ I • F.N n
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Subsingleton I.Cotangent ↔ IsIdempotentElem I

Tactic:
by
  constructor
  · intro H
    refine (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) ?_)
    exact fun x hx => (I.toCotangent_eq_zero ⟨x, hx⟩).mp (Subsingleton.elim _ _)
  · exact fun e =>
      ⟨fun x y =>
        Quotient.inductionOn₂' x y fun x y =>
          I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩

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

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : J.Cotangent
hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J))

Tactic:
rcases J.toCotangent_surjective x with ⟨x', hx'⟩
    have : Function.Surjective (Algebra.ofId A B) := surj
    simp only [← hx', LinearMap.mem_ker, Ideal.mapCotangent_toCotangent,
      Ideal.toCotangent_eq_zero, eqmap, Algebra.ofId_apply] at hx
    rw [← Ideal.map_pow, ← Ideal.mem_comap, Ideal.comap_map_of_surjective' _ surj] at hx
    rcases Submodule.mem_sup.mp hx with ⟨y, hy, z, hz, hyz⟩
    have : y + z ∈ J := by simp [hyz]
    have zmemJ := (Ideal.add_mem_iff_right J (Ideal.pow_le_self (by omega) hy)).mp this
    have xeq : x = J.toCotangent ⟨z, zmemJ⟩ := by simpa [← hx', J.toCotangent_eq, ← hyz] using hy
    rw [xeq]
    exact Submodule.mem_map_of_mem (Submodule.mem_comap.mpr (Ideal.mem_inf.mpr ⟨hz, zmemJ⟩))

Goal state after: