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

Goal state before:
pp: case sdiff
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 U : Set X
hU : U ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
V : Set X
hV : V ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (U \ V) ⋯

Tactic:
have := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _ basis isCompact_basis
    obtain ⟨s, hs, rfl⟩ := (this _).1 ⟨hU.2.isCompact, hU.1⟩
    obtain ⟨t, ht, rfl⟩ := (this _).1 ⟨hV.2.isCompact, hV.1⟩
    simp_rw [iUnion_sdiff]
    induction s, hs using Set.Finite.induction_on with
    | empty => simpa using sdiff (Classical.arbitrary _) {Classical.arbitrary _}
    | @insert i s hi hs ih =>
      simp_rw [biUnion_insert]
      exact union _ _ _
        (.biUnion hs fun i _ ↦ ((isCompact_basis _).isConstructible (basis.isOpen ⟨i, rfl⟩)).sdiff
          <| .biUnion ht fun j _ ↦ (isCompact_basis _).isConstructible (basis.isOpen ⟨_, rfl⟩))
        (sdiff _ _ ht)
        (ih ⟨isOpen_biUnion fun  _ _ ↦ basis.isOpen ⟨_, rfl⟩, .biUnion hs
          fun i _ ↦ (isCompact_basis _).isRetrocompact (basis.isOpen ⟨i, rfl⟩)⟩)

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

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this✝ : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
hl :
  PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R Q) Q (algebraMap R S) ⋯)
      { asIdeal := Pl, isPrime := isPrime✝ } =
    { asIdeal := pl, isPrime := ⋯ }
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
⊢ p = Ideal.under R (Ideal.under S Pl)

Tactic:
replace hl : Pl.under _ = pl := by simpa [PrimeSpectrum.ext_iff] using! hl

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H :
  ∀ (P : Ideal S) [inst : P.IsPrime],
    Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))
p : Ideal R
x✝¹ : p.IsPrime
Q : Ideal S
x✝ : Q.IsPrime
hlt : p < Ideal.under R Q
pl : Ideal (Localization.AtPrime (Ideal.under R Q)) :=
  Ideal.map (algebraMap R (Localization.AtPrime (Ideal.under R Q))) p
this✝ : pl.IsPrime
Pl : Ideal (Localization.AtPrime Q)
isPrime✝ : Pl.IsPrime
this : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
hl : Ideal.under (Localization.AtPrime (Ideal.under R Q)) Pl = pl
⊢ p = Ideal.under R (Ideal.under S Pl)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : (Algebra.TensorProduct.lmul' R).Flat
⊢ (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).Flat

Tactic:
← CommRingCat.flat_ofHom_iff

Goal state after:
R S T A : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra S T
inst✝³ : IsScalarTower R S T
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
h : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.mapOfCompatibleSMul S R T T A).toRingHom)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : s ∈ {s | IsIrreducible s}
⊢ vanishingIdeal s ∈ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s}

Tactic:
exact ⟨closure s, ⟨isClosed_closure, hs.closure⟩, vanishingIdeal_closure s⟩

Goal state after:
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
le : sInf {I | I.IsMaximal} ≤ nilradical R
I : Ideal R
hI : I.IsPrime
⊢ I.IsMaximal

Tactic:
replace le := le.trans (nilradical_le_prime I)

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 : sInf {I | I.IsMaximal} ≤ I
⊢ I.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
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ r • D 1 = 0

Tactic:
D.map_one_eq_zero,

Goal state after:
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
S : Type u_5
T : Type u_6
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ r • 0 = 0
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:
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.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ r ∉ x.asIdeal → ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥

Tactic:
rintro h₁ _ ⟨⟨n, rfl⟩, h₃⟩

Goal state after:
case mpr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : r ∉ x.asIdeal
n : ℕ
h₃ : (fun x ↦ r ^ x) n ∈ ↑x.asIdeal
⊢ (fun x ↦ r ^ x) n ∈ ⊥
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ minimalPeriod (fun x ↦ a +ᵥ x) b • ⟨a, ⋯⟩ +ᵥ b = b

Tactic:
simp_rw [← vadd_iterate]

Goal state after:
n : ℕ
A : Type u_1
R : Type u_2
inst✝³ : AddGroup A
inst✝² : Ring R
α : Type u_3
β : Type u_4
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
⊢ (fun x ↦ ⟨a, ⋯⟩ +ᵥ x)^[minimalPeriod (fun x ↦ a +ᵥ x) b] b = b
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ sᶜ = comap f '' comap f ⁻¹' sᶜ

Tactic:
Set.image_preimage_eq _ h₁

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
h₁ : Function.Surjective (comap f)
h₂ : GeneralizingMap (comap f)
s : Set (PrimeSpectrum R)
hsc : IsClosed (comap f ⁻¹' s)
⊢ sᶜ = sᶜ
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
⊢ IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g ∣ p ^ k

Tactic:
by
  simp_rw [isPGroup_iff_pow_pow_eq_one, orderOf_dvd_iff_pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
hG : (Nat.card G).primeFactors ⊆ p.primeFactors
⊢ (∏ p ∈ (Nat.card G).primeFactors, p) ^ Nat.card G ∣ p ^ Nat.card G

Tactic:
Finset.prod_dvd_prod_of_subset _ _ (·) hG,

Goal state after:
case refine_2
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : p ≠ 0
hG : (Nat.card G).primeFactors ⊆ p.primeFactors
⊢ (∏ i ∈ p.primeFactors, i) ^ Nat.card G ∣ p ^ Nat.card G
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p ↥K
hHK : H ≤ K
a b : ↥H
h : (Subgroup.inclusion hHK) a = (Subgroup.inclusion hHK) b
⊢ ↑a = ↑b

Tactic:
change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p ↥K
hHK : H ≤ K
a b : ↥H
h : (Subgroup.inclusion hHK) a = (Subgroup.inclusion hHK) b
⊢ ↑((Subgroup.inclusion hHK) a) = ↑((Subgroup.inclusion hHK) b)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ Finite (Sylow p G)

Tactic:
apply finite_of_ker_is_pGroup (f := QuotientGroup.mk' P.normalCore)

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ IsPGroup p ↥(QuotientGroup.mk' (↑P).normalCore).ker
Module: Mathlib.GroupTheory.Rank

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

Tactic:
have := Fintype.ofFinite s
  rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
  exact rank_closure_finset_le_card s.toFinset

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card α = p
⊢ IsSimpleGroup α

Tactic:
by
  subst h
  have : Finite α := Nat.finite_of_card_ne_zero hp.1.ne_zero
  have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp hp.1.one_lt
  exact ⟨fun H _ => H.eq_bot_or_eq_top_of_prime_card⟩

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

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
⊢ IsCyclic α

Tactic:
nontriviality α
  obtain ⟨g, hg⟩ := exists_ne (1 : α)
  have : Subgroup.zpowers g = ⊤ :=
    (eq_bot_or_eq_top (Subgroup.zpowers g)).resolve_left (Subgroup.zpowers_ne_bot.2 hg)
  exact ⟨⟨g, (Subgroup.eq_top_iff' _).1 this⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝ : Monoid G
tG : IsMulTorsion G
g : G
⊢ g ^ (orderOf g - 1) * g = 1

Tactic:
rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
      exact (tG g).orderOf_pos

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
⊢ exponent α = Nat.card α

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : IsCyclic α
g : α
hg : orderOf g = Nat.card α
⊢ exponent α = Nat.card α
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, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j = ⊤ ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤

Tactic:
rw [eq_top_iff_one, Submodule.mem_iSup_finset_iff_exists_sum]

Goal state after:
ι : 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 = ⊤
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case inr.inr.hn
M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
h✝¹ : Finite ↥f.ker
h✝ : Finite ↥f.range
this : Finite M
⊢ Monoid.exponent ↥f.range ∣ Monoid.exponent M

Tactic:
exact MonoidHom.exponent_dvd f.rangeRestrict_surjective

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
⊢ IsCyclic M

Tactic:
by
  cases (finite_or_infinite f.ker).symm
  · rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h
    rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h
    rwa [← Subgroup.topEquiv.isCyclic, ← h]
  cases (finite_or_infinite f.range).symm
  · rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h
    rwa [(f.ofInjective (f.ker_eq_bot_iff.mp (f.ker.eq_bot_of_card_eq h))).isCyclic]
  have := f.finite_iff_finite_ker_range.mpr ⟨‹_›, ‹_›⟩
  rw [IsCyclic.iff_exponent_eq_card]
  apply dvd_antisymm Group.exponent_dvd_nat_card
  rw [← f.ker.card_mul_index, Subgroup.index_ker]
  apply h.mul_dvd_of_dvd_of_dvd <;> rw [← IsCyclic.exponent_eq_card]
  · exact Monoid.exponent_dvd_of_monoidHom _ f.ker.subtype_injective
  · exact MonoidHom.exponent_dvd f.rangeRestrict_surjective

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

Goal state before:
pp: case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝² : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM✝ : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
hM : IsCyclic ↥f.ker
e : ↥f.ker ≃* M := ⋯.mpr (((⊤.prodEquiv ⊥).trans MulEquiv.prodUnique).trans Subgroup.topEquiv)
x✝¹ : CommGroup M := IsCyclic.commGroup
x✝ : CommGroup N := IsCyclic.commGroup
⊢ IsCyclic (M × N)

Tactic:
← Nat.card_congr e.toEquiv

Goal state after:
case refine_2
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝² : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM✝ : IsCyclic M
hN : IsCyclic N
f : M × N →* N := MonoidHom.snd M N
h : (Nat.card ↥f.ker).Coprime (Nat.card N)
hM : IsCyclic ↥f.ker
e : ↥f.ker ≃* M := ⋯.mpr (((⊤.prodEquiv ⊥).trans MulEquiv.prodUnique).trans Subgroup.topEquiv)
x✝¹ : CommGroup M := IsCyclic.commGroup
x✝ : CommGroup N := IsCyclic.commGroup
⊢ IsCyclic (M × N)
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mpr.refine_1
ι : 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
i : ι
hi : i = a
⊢ v ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j

Tactic:
simp only [mem_iInf] at hv ⊢

Goal state after:
case refine_2.mpr.refine_1
ι : 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
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ i ∈ t, v ∈ I i
⊢ ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → v ∈ I i_1
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
r : R[X]
x : PolynomialModule R R
⊢ (coeffAddEquiv.trans (AddMonoidAlgebra.coeffAddEquiv.symm.trans (toFinsuppIso R).symm.toAddEquiv)).toFun (r • x) =
    (RingHom.id R[X]) r •
      (coeffAddEquiv.trans (AddMonoidAlgebra.coeffAddEquiv.symm.trans (toFinsuppIso R).symm.toAddEquiv)).toFun x

Tactic:
dsimp
    induction x using induction_linear with
    | zero => simp
    | add _ _ hp hq => simp_all [smul_add, mul_add]
    | single n a =>
    ext i
    simp only [coeffAddEquiv_apply, AddMonoidAlgebra.coeffAddEquiv_symm_apply,
      toFinsuppIso_symm_apply, coeff_ofFinsupp, smul_single_apply, smul_eq_mul, coeff_single,
      AddMonoidAlgebra.ofCoeff_single, ofFinsupp_single]
    split_ifs with hn
    · rw [show i = (i - n) + n by lia, Polynomial.coeff_mul_monomial]
      simp
    · rw [Polynomial.coeff_mul, Finset.sum_eq_zero]
      simp [Polynomial.coeff_monomial]
      lia

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
S : Set (I.Filtration M)
i : ℕ
⊢ I • (⨆ a, ↑a) i ≤ (⨆ a, ↑a) (i + 1)

Tactic:
iSup_apply,

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 F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • ⨆ i_1, ↑i_1 i ≤ (⨆ a, ↑a) (i + 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 F' : I.Filtration M
h : F.Stable
h' : F'.Stable
e : F.N 0 = F'.N 0
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n

Tactic:
obtain ⟨n₁, h₁⟩ := h.exists_forall_le (le_of_eq e)
  obtain ⟨n₂, h₂⟩ := h'.exists_forall_le (le_of_eq e.symm)
  use max n₁ n₂
  intro n
  refine ⟨(F.antitone ?_).trans (h₁ n), (F'.antitone ?_).trans (h₂ n)⟩ <;> simp

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

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ I • ⊤ ≤ Submodule.comap (Submodule.subtype I) (I ^ 2)

Tactic:
← Submodule.map_le_iff_le_comap,

Goal state after:
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) (I • ⊤) ≤ I ^ 2
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
⊢ j✝ = j'✝

Tactic:
obtain ⟨k, w₁, w₂⟩ := w

Goal state after:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
k : ι
w₁ : c₁.Rel i✝ k
w₂ : c₂.Rel k j✝
⊢ j✝ = j'✝
Module: Mathlib.Algebra.Homology.ComplexShape

Goal state before:
pp: ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
⊢ i✝ = i'✝

Tactic:
obtain ⟨k, w₁, w₂⟩ := w

Goal state after:
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
k : ι
w₁ : c₁.Rel i✝ k
w₂ : c₂.Rel k j✝
⊢ i✝ = i'✝
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
desc✝¹ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝¹ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝¹ d') = d'
postcomp_injective✝¹ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
desc✝ : {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} → M'.Derivation φ → (M ⟶ M')
fac✝ : ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), d.postcomp (desc✝ d') = d'
postcomp_injective✝ :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (φ_1 φ' : M ⟶ M'),
    d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
this :
  ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ),
    { desc := desc✝¹, fac := fac✝¹, postcomp_injective := postcomp_injective✝¹ }.desc d' =
      { desc := desc✝, fac := fac✝, postcomp_injective := postcomp_injective✝ }.desc d'
x✝¹ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : x✝¹.Derivation φ
⊢ desc✝¹ x✝ = desc✝ x✝

Tactic:
apply this

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)

Tactic:
by
  rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval,
    Functor.map_id, NatTrans.id_app]

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : (single V c i).obj A ⟶ K
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
exact hfg

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : K ⟶ (single V c i).obj A
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
exact hfg

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
⊢ ∀ (X : Discrete A),
    (MonoidalCategoryStruct.rightUnitor ((Discrete.functor h.F).obj X)).hom =
      MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj X) h.zero.symm.hom ≫
        (h.add X.as (MonoidalCategoryStruct.tensorUnit (Discrete A)).as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.rightUnitor X).hom

Tactic:
by
        rintro ⟨n⟩
        ext X
        simp [h.add_zero_inv_app]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ g.f i = h.f i

Tactic:
← cancel_epi (φ.f i)

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ φ.f i ≫ g.f i = φ.f i ≫ h.f i