mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.FaithfullyFlat A B
p : Ideal A
inst✝ : p.IsPrime
⊢ ∃ P, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, _, hP⟩ := (Ideal.comap_map_eq_self_iff_of_isPrime p).mp <|
    p.comap_map_eq_self_of_faithfullyFlat (B := B)

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.FaithfullyFlat A B
p : Ideal A
inst✝ : p.IsPrime
P : Ideal B
left✝ : P.IsPrime
hP : comap (algebraMap A B) P = p
⊢ ∃ P, P.IsPrime ∧ P.LiesOver p
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
i : ι
p : PrimeSpectrum (R i)
⊢ comap f (comap (Pi.evalRingHom R i) p) ∈ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i))

Tactic:
exact Set.mem_iUnion_of_mem i ⟨p, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a * ↑b = ↑a * ↑b

Tactic:
rw [a.2]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

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

Tactic:
rw [a.2]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ (Ideal.map (algebraMap R A) I).IsPrime

pp: case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.comap (algebraMap R A) (Ideal.map (algebraMap R A) I) = I

Tactic:
· exact IsLocalization.isPrime_of_isPrime_disjoint S A I hI.1 hI'

Goal state after:
case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.comap (algebraMap R A) (Ideal.map (algebraMap R A) I) = I
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
x : α
⊢ x ∈ ↑(U ⇨ V) ↔ x ∈ ↑(Opens.interior (↑U ⇨ ↑V))

Tactic:
BooleanAlgebra.himp_eq,

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
x : α
⊢ x ∈ ↑(U ⇨ V) ↔ x ∈ ↑(Opens.interior (↑V ⊔ (↑U)ᶜ))
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
rintro ⟨sU, hU⟩ x hx

Goal state after:
case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst✝] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp
α : Type u_2
inst✝ : TopologicalSpace α
B : Set (Opens α)
⊢ IsBasis B → ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

Tactic:
intro hB U
    refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩
    rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
    simp_rw [sUnion_eq_biUnion, iUnion, mem_ofPred_eq, iSup_and, iSup_image]
    rfl

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsLocallyClosed s
f : X → Y
hf : IsInducing f
hf' : IsLocallyClosed (range f)
⊢ IsLocallyClosed (f '' s)

Tactic:
by
  obtain ⟨t, ht, rfl⟩ := hf.isLocallyClosed_iff.mp hs
  rw [image_preimage_eq_inter_range]
  exact ht.inter hf'

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i) = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
X : Type u_6
Y : Type u_7
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : Continuous[inst✝², inst✝¹] f
ι : Type u_4
U : ι → Opens Y
hU : range f ⊆ ↑(iSup U)
V : ι → Type u_5
inst✝ : (i : ι) → TopologicalSpace (V i)
iV : (i : ι) → V i → X
hiV : ∀ (i : ι), Continuous[inst✝ i, inst✝²] (iV i)
hV : ∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)
hV' : ∀ (i : ι), IsEmbedding (f ∘ iV i)
this :
  ∀ {X : Type u_6} {Y : Type u_7} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f →
      ∀ {ι : Type u_4} (U : ι → Opens Y),
        range f ⊆ ↑(iSup U) →
          ∀ (V : ι → Type u_5) [inst_2 : (i : ι) → TopologicalSpace (V i)] (iV : (i : ι) → V i → X),
            (∀ (i : ι), Continuous (iV i)) →
              (∀ (i : ι), f ⁻¹' ↑(U i) ⊆ range (iV i)) →
                (∀ (i : ι), IsEmbedding (f ∘ iV i)) → iSup U = ⊤ → IsEmbedding f
hU' : ¬iSup U = ⊤
f₀ : X → ↑(range f) := fun x ↦ ⟨f x, ⋯⟩
⊢ ⊤ ≤ ⨆ i, (Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (U i)
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
S : Set (Closeds α)
⊢ ↑(sSup S) = closure[inst✝] (⋃₀ (SetLike.coe '' S))

Tactic:
by rfl

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
⊢ ?m.62

Tactic:
refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
x : Y
hx : x ∈ U
⊢ x ∈ ⋃ i, f '' ↑↑i
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace α
inst✝ : T2Space α
s t : CompactOpens α
⊢ IsOpen { carrier := ↑s ⇨ ↑t, isCompact' := ⋯ }.carrier

Tactic:
by simpa [himp_eq] using t.isOpen.union s.isCompact.isClosed.isOpen_compl

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

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

Tactic:
by
  apply IsStableUnderBaseChange.mk respectsIso
  introv h
  rw [flat_algebraMap_iff] at h ⊢
  infer_instance

Goal state after:
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 : CommRingCat.flat (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)
⊢ CommRingCat.of S ⟶ CommRingCat.of (T ⊗[S] A)

Tactic:
exact CommRingCat.ofHom
      (RingHom.comp (Algebra.TensorProduct.includeLeft (S := R)).toRingHom (algebraMap S T))

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✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ zeroLocus ↑{ asIdeal := vanishingIdeal S, isPrime := ⋯ }.asIdeal = S

Tactic:
zeroLocus_vanishingIdeal_eq_closure,

Goal state after:
R : Type u
S✝ : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ closure S = S
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ x ∈ Set.range (comap (algebraMap R S))

Tactic:
· use ⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩
    ext1
    exact IsLocalization.under_map_of_isPrime_disjoint M S x.2 h

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ (zeroLocus {f})ᶜ ⊆ (zeroLocus {g})ᶜ ↔ f ∈ (Ideal.span {g}).radical

Tactic:
Set.compl_subset_compl,

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ zeroLocus {g} ⊆ zeroLocus {f} ↔ f ∈ (Ideal.span {g}).radical
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
n : ℤ
⊢ D ↑n = 0

Tactic:
by
  rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
nc : ¬IsCyclic α
⊢ Nontrivial α

Tactic:
by
  contrapose! nc
  exact isCyclic_of_subsingleton

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ IsCyclic α ↔ ∃ g, orderOf g = Nat.card α

Tactic:
simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]

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

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

Tactic:
exact hx

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
x y : PrimeSpectrum R
h : x ⤳ y
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)

Tactic:
rw [← PrimeSpectrum.le_iff_specializes, ← asIdeal_le_asIdeal, ← SetLike.coe_subset_coe, ←
        Set.compl_subset_compl] at h

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : (↑y.asIdeal)ᶜ ⊆ (↑x.asIdeal)ᶜ
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
g : G
k : ℕ
⊢ zpowers (g ^ k) ≤ zpowers g

Tactic:
exact zpowers_le_of_mem <| npow_mem_zpowers g k

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsPGroup 1 G ↔ Subsingleton G

Tactic:
by
  refine ⟨?_, fun h ↦ .of_subsingleton 1 G⟩
  simpa [isPGroup_iff_pow_pow_eq_one] using subsingleton_of_forall_eq 1

Goal state after:
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
Monoid.exponent_dvd_iff_forall_pow_eq_one,

Goal state after:
G : Type u
inst✝ : Group G
n : ℤ
⊢ (∀ (g : G), g ^ n.natAbs = 1) ↔ ∀ (g : G), g ^ n = 1
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 : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
this : (↑(P.subtype ⋯)).Normal
⊢ ¬p ∣ (↑P).relIndex (normalizer ↑P) * Nat.card (Sylow p G)

Tactic:
have : (P.subtype le_normalizer).FiniteIndex := ⟨hP⟩

Goal state after:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
this✝ : (↑(P.subtype ⋯)).Normal
this : (↑(P.subtype ⋯)).FiniteIndex
⊢ ¬p ∣ (↑P).relIndex (normalizer ↑P) * Nat.card (Sylow p G)
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), ∃ μ, ↑(μ a) = 1

Tactic:
refine fun a => ⟨fun i => if h : i = a then ⟨1, ?_⟩ else 0, ?_⟩

Goal state after:
case refine_1.refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a i : ι
h : i = a
⊢ 1 ∈ ⨅ j ∈ {a}, ⨅ (_ : j ≠ i), I j

case refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
⊢ ↑((fun i ↦ if h : i = a then ⟨1, ⋯⟩ else 0) a) = 1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM : IsCyclic M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
have hN := isCyclic_right_of_prod M N

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Group M
inst✝² : Group N
cyc : IsCyclic (M × N)
inst✝¹ : Finite M
inst✝ : Finite N
hM : IsCyclic M
hN : IsCyclic N
⊢ (Nat.card M).Coprime (Nat.card N)
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
this : ↑(μ a) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose h), I j

Tactic:
rw [mem_iInf] at this ⊢

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μ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
this : ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i
⊢ ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ t), ⨅ (_ : i ≠ Exists.choose h), I i
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
| s.length.succ - Nat.succ 0

Tactic:
Nat.add_one_sub_one

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
| s.length
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
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
refine isSemisimpleModule_of_isSemisimpleModule_submodule
    ((comap_equiv_self_of_inj_of_le (injective_subtype _) ?_).isSemisimpleModule_iff.mpr <| hp · ·)
    (biSup_comap_subtype_eq_top ..)

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
x1✝ : ι
x2✝ : x1✝ ∈ s
⊢ p x1✝ ≤ (⨆ i ∈ s, p i).subtype.range
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : torsionOf R M m = ⊥
contra : m = 0
⊢ False

Tactic:
contra,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : torsionOf R M 0 = ⊥
contra : m = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.Module.Basic

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

Tactic:
rw [Function.iterate_zero, zero_add]
    exact congr(ofCoeff R $(Finsupp.smul_single r j m))

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

Goal state before:
pp: case single.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'
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (map R' f) (p✝ • single R i m) = Polynomial.map (algebraMap R R') p✝ • (map R' f) (single R i m)
e₂ : (map R' f) (q✝ • single R i m) = Polynomial.map (algebraMap R R') q✝ • (map R' f) (single R i m)
⊢ Polynomial.map (algebraMap R R') p✝ • (map R' f) (single R i m) +
      Polynomial.map (algebraMap R R') q✝ • (map R' f) (single R i m) =
    Polynomial.map (algebraMap R R') (p✝ + q✝) • (map R' f) (single R i m)

Tactic:
Polynomial.map_add,

Goal state after:
case single.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'
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (map R' f) (p✝ • single R i m) = Polynomial.map (algebraMap R R') p✝ • (map R' f) (single R i m)
e₂ : (map R' f) (q✝ • single R i m) = Polynomial.map (algebraMap R R') q✝ • (map R' f) (single R i m)
⊢ Polynomial.map (algebraMap R R') p✝ • (map R' f) (single R i m) +
      Polynomial.map (algebraMap R R') q✝ • (map R' f) (single R i m) =
    (Polynomial.map (algebraMap R R') p✝ + Polynomial.map (algebraMap R R') q✝) • (map R' f) (single R i m)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
⊢ Set.range s ⊆ ↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj))))

Tactic:
Set.range_subset_iff

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : (x : M) → Decidable (x = 0)
p : R
hM : IsTorsion' M ↥(Submonoid.powers p)
d : ℕ
hd : d ≠ 0
s : Fin d → M
hs : span R (Set.range s) = ⊤
oj : Option (Fin d) := List.argmax (fun i ↦ pOrder hM (s i)) (List.finRange d)
hoj : oj.isSome = true
⊢ ∀ (y : Fin d), s y ∈ ↑(torsionBy R M (p ^ pOrder hM (s (oj.get hoj))))
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • (mk (R ∙ a * b)) x = 0
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h

Goal state after:
case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (a * b) = a • x
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A
hx : x ∈ ↑(RingHom.ker f.toRingHom)
⊢ (Quotient.mk (RingHom.ker f.toRingHom ^ 2)).toSemilinearMap x ∈ RingHom.ker f.kerSquareLift.toRingHom

Tactic:
exact hx

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X
naturality :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    M₁.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom = (app X).hom ≫ M₂.map f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ M₂.map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).inv = (app X).inv ≫ M₁.map f

Tactic:
rw [← cancel_epi (app X).hom, ← reassoc_of% (naturality f), Iso.map_hom_inv_id,
          Category.comp_id, Iso.hom_inv_id_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (-f.app Y) = (-f.app X) ≫ M₂.map h

Tactic:
by
        ext x
        simp [← naturality_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y + g.app Y) =
    (f.app X + g.app X) ≫ M₂.map h

Tactic:
by
        ext x
        simp [← naturality_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
f g : M₁ ⟶ M₂
X Y : Cᵒᵖ
h : X ⟶ Y
⊢ M₁.map h ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map h))).map (f.app Y - g.app Y) =
    (f.app X - g.app X) ≫ M₂.map h

Tactic:
by
        ext x
        simp [← naturality_apply]

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:
← NatTrans.comp_app,

Goal state after:
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) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)