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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
c : ↥E ⊗[R] M →₀ R
b : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → ↥E
a : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → M
hy : ∀ ⦃a_1 : ↥E ⊗[R] M⦄ (a_2 : a_1 ∈ ↑c.support), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : ↥E ⊗[R] M⦄ → a ∈ c.support → R := fun a ha ↦ ⋯.choose
hr : ∀ ⦃i : ↥E ⊗[R] M⦄ (hi : i ∈ c.support), b hi = r hi • ⟨l23 (l12 n1), ⋯⟩
i : ↥E ⊗[R] M
hi : i ∈ c.support
⊢ (LinearMap.rTensor M E.subtype) (c (⟨l23 (l12 n1), ⋯⟩ ⊗ₜ[R] (r hi • a hi)) • ⟨l23 (l12 n1), ⋯⟩ ⊗ₜ[R] (r hi • a hi)) =
    (LinearMap.rTensor M E.subtype) 0

Tactic:
map_smul,

Goal state after:
R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
n1 : N1
hn1 : l23 (l12 n1) ≠ 0
E : Submodule R N3 := R ∙ l23 (l12 n1)
hE : Nontrivial ↥E
eq1 : ∀ (m : M), l23 (l12 n1) ⊗ₜ[R] m = 0
c : ↥E ⊗[R] M →₀ R
b : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → ↥E
a : ⦃a : ↥E ⊗[R] M⦄ → a ∈ ↑c.support → M
hy : ∀ ⦃a_1 : ↥E ⊗[R] M⦄ (a_2 : a_1 ∈ ↑c.support), b a_2 ⊗ₜ[R] a a_2 = a_1
r : ⦃a : ↥E ⊗[R] M⦄ → a ∈ c.support → R := fun a ha ↦ ⋯.choose
hr : ∀ ⦃i : ↥E ⊗[R] M⦄ (hi : i ∈ c.support), b hi = r hi • ⟨l23 (l12 n1), ⋯⟩
i : ↥E ⊗[R] M
hi : i ∈ c.support
⊢ c (⟨l23 (l12 n1), ⋯⟩ ⊗ₜ[R] (r hi • a hi)) • (LinearMap.rTensor M E.subtype) (⟨l23 (l12 n1), ⋯⟩ ⊗ₜ[R] (r hi • a hi)) =
    (LinearMap.rTensor M E.subtype) 0
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
⊢ IsAlgebraic R a

Tactic:
have := NoZeroDivisors.of_faithfulSMul R S

Goal state after:
case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : (aeval a) p = 0
hRS : FaithfulSMul R S
this : NoZeroDivisors R
⊢ IsAlgebraic R a
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ (AlgHom.restrictScalars R (aeval a)) (r • p✝) = 0

Tactic:
map_smul,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Ring A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
inst✝ : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p✝ : S[X]
hp : p✝ ≠ 0
eval0 : (aeval a) p✝ = 0
hRS : FaithfulSMul R S
this✝¹ : NoZeroDivisors R
this✝ : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p✝.coeff p✝.support, IsIntegral R (r • z)
p : (↥(integralClosure R S).toSubring)[X] := (r • p✝).toSubring (integralClosure R S).toSubring ⋯
⊢ r • (AlgHom.restrictScalars R (aeval a)) p✝ = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
x : S
inst✝ : Away x Sₘ
p : R[X]
hpm : p.Monic
n : ℕ
hn : x ^ n * eval₂ (algebraMap R S) x p = 0
⊢ eval₂ (algebraMap R S) x (X ^ n * p) = 0

Tactic:
by simpa

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
alg : ∀ x ∈ s \ t, IsAlgebraic (↥(adjoin R t)) x
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
⊢ IsAlgebraic (↥(adjoin R t)) a

Tactic:
set Rt := adjoin R t

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : NoZeroDivisors S
s t : Set S
a : A
Rs : Subalgebra R S := adjoin R s
ha : IsAlgebraic (↥Rs) a
Rt : Subalgebra R S := adjoin R t
alg : ∀ x ∈ s \ t, IsAlgebraic (↥Rt) x
⊢ IsAlgebraic (↥Rt) a
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ y * ↑z' = y' * ↑⟨(algebraMap R S) z, hz0'⟩

Tactic:
yz_eq

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
K : Type u_4
L : Type u_5
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra R K
inst✝⁶ : Algebra R L
inst✝⁵ : Algebra S L
inst✝⁴ : Algebra.IsAlgebraic R S
inst✝³ : IsFractionRing S L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective ⇑(algebraMap R L)
h : ↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b)
y' : S
z' : ↥S⁰
hx : (algebraMap S L) a * mk' L y' z' ∈ ↑(Ideal.span {(algebraMap S L) a})
y : S
z : R
hz0 : z ≠ 0
yz_eq : y' * (algebraMap R S) z = y * ↑z'
injRS : Function.Injective ⇑(algebraMap R S)
hz0' : (algebraMap R S) z ∈ S⁰
⊢ y * ↑z' = y * ↑z'
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
h : ∀ (x : S), ∃ r s, IsUnit (f s) ∧ f s * x = f r
I : Ideal S
hI : I ≠ ⊤
x : S
r s : R
hr : IsUnit (f s)
hr' : f s * x = f r
⊢ 1 * f s * x = 1 * f r

Tactic:
by simpa

Goal state after:
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✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
⊢ m • ⊤ ≠ ⊤

Tactic:
obtain ⟨m', hm'⟩ := h ⟨m, hm.isPrime⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
⊢ m • ⊤ ≠ ⊤
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case mp.mk
α : 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 }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen[inst✝] carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : ↑{ carrier := carrier✝, is_open' := is_open'✝ } = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }

Tactic:
dsimp at H₂

Goal state after:
case mp.mk
α : 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 }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen[inst✝] carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : carrier✝ = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: case hb
α : Type u_2
inst✝ : TopologicalSpace α
ι : Type u_5
b : ι → Opens α
hb : IsBasis (range b)
hb' : ∀ (i : ι), IsCompact ↑(b i)
U : Set α
⊢ IsTopologicalBasis (range fun i ↦ (b i).carrier)

Tactic:
convert! (config := { transparency := .default }) hb
    ext
    simp

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
← SetLike.coe_set_eq

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
s : Opens α
H : ∀ (ι : Type u_2) (s_1 : ι → Opens α), s ≤ iSup s_1 → ∃ t, s ≤ t.sup s_1
ι : Type u_2
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst✝] (U i)
hU' : ↑s ⊆ ⋃ i, U i
⊢ s ≤ ⨆ i, { carrier := U i, is_open' := ⋯ }

Tactic:
by simpa

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 Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
⊢ ∀ U ∈ Set.preimage f '' {U | IsOpen[inst✝¹] U ∧ IsCompact U}, IsCompact U

Tactic:
simp only [Set.mem_image, Set.mem_ofPred_eq, forall_exists_index, and_imp]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
⊢ ∀ (U : Set X) (x : Set Y), IsOpen[inst✝¹] x → IsCompact x → f ⁻¹' x = U → IsCompact U
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
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : ↑U.toOpens ⊆ ⋃ i ∈ I, ↑i.toOpens
s : Set (CompactOpens X)
hsI : s ⊆ ↑I
hs : s.Finite
hU : ↑U ⊆ ⋃ i ∈ s, ↑i.toOpens
⊢ (hs.toFinset.sup fun i ↦ i) ∈ ↑I

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
hf : ∅.Finite
ho : ∀ t ∈ ∅, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ ∅, IsCompact t
⊢ IsCompact (⋂₀ ∅)

Tactic:
simp [CompactSpace.isCompact_univ]

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

Tactic:
refine ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, ?_⟩

Goal state after:
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
r : R
⊢ D (r • 1) = 0

Tactic:
map_smul,

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
r : R
⊢ r • D 1 = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ ⨆ i ∈ s, basicOpen i = ⊤ ↔ Ideal.span s = ⊤

Tactic:
conv_rhs => rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]
  simp

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
⊢ g ^ (k % ↑(Nat.find hex)) * g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
rw [← zpow_add, Int.emod_add_mul_ediv, hk]

Goal state after:
α : 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
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
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
⊢ IsClosed (comap f '' zeroLocus ↑I)

Tactic:
refine (isClosed_iff_zeroLocus _).mpr ⟨I.comap f, le_antisymm ?_ fun p hp ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
⊢ comap f '' zeroLocus ↑I ⊆ zeroLocus ↑(Ideal.comap f I)

case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I
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
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
hk₆ : (k % ↑(Nat.find hex)).natAbs = 0
this : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) = x
⊢ ↑((fun x ↦ ⟨g ^ Nat.find hex, ⋯⟩ ^ x) (k / ↑(Nat.find hex))) = ↑⟨x, hx⟩

Tactic:
simpa [zpow_mul]

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
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
hk₆ : (k % ↑(Nat.find hex)).natAbs = 0
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) = x

Tactic:
Int.mul_ediv_cancel'
                  (Int.dvd_of_emod_eq_zero (Int.natAbs_eq_zero.mp hk₆)),

Goal state after:
α : 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
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
hk₆ : (k % ↑(Nat.find hex)).natAbs = 0
⊢ g ^ k = x
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:
by simpa

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1

Tactic:
refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩

Goal state after:
case refine_1
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
⊢ 0 < Finset.univ.lcm orderOf

case refine_2
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
_inst : Fintype G := Fintype.ofFinite G
g : G
⊢ g ^ Finset.univ.lcm orderOf = 1
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_3
inst✝ : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
⊢ Nonempty ↑(fixedPoints G α)

Tactic:
rw [← Finite.card_pos_iff, pos_iff_ne_zero]
      contrapose hpα
      rw [← Nat.modEq_zero_iff_dvd, ← hpα]
      exact hG.card_modEq_card_fixedPoints α

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)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ fixedPoints (ConjAct G) G → ∃ b ∈ fixedPoints (ConjAct G) G, a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
ConjAct.fixedPoints_eq_center

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)
Module: Mathlib.GroupTheory.Exponent

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

Tactic:
by
  simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : ↥(centralizer ↑(zpowers x))
hh : ((↑h * g) • P).subtype ⋯ = P.subtype h1
⊢ g⁻¹ * x * g = (↑h * g)⁻¹ * ↑h * x * g

Tactic:
mul_inv_rev,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : ↥(centralizer ↑(zpowers x))
hh : ((↑h * g) • P).subtype ⋯ = P.subtype h1
⊢ g⁻¹ * x * g = g⁻¹ * (↑h)⁻¹ * ↑h * x * g
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : (n⁻¹ * x)⁻¹ * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H

Tactic:
mul_inv_rev,

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n⁻¹⁻¹ * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
⊢ ∃ t, f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
    obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
    refine ⟨(↑) '' u, ?_, ?_⟩
    · replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
      simp_rw [hu, Iic.coe_sSup]
    · rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
hn : p ^ n ≤ Nat.card G
⊢ ∃ H, Nat.card ↥H = p ^ n

Tactic:
by
  have : Fact p.Prime := ⟨hp⟩
  have : Finite G := Nat.finite_of_card_ne_zero <| by linarith [Nat.one_le_pow n p hp.pos]
  obtain ⟨m, hm⟩ := h.exists_card_eq
  refine exists_subgroup_card_pow_prime _ ?_
  rw [hm] at hn ⊢
  exact pow_dvd_pow _ <| (Nat.pow_le_pow_iff_right hp.one_lt).1 hn

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:
by simpa

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

Goal state before:
pp: case a4
ι : 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
⊢ I a ⊔ I b = ⊤

Tactic:
case a4 =>
      rw [eq_top_iff_one, Submodule.mem_sup]
      rw [add_comm] at hμ
      refine ⟨_, ?_, _, ?_, hμ⟩
      · refine sum_mem _ fun x hx => ?_
        have := Submodule.coe_mem (μ x)
        simp only [mem_iInf] at this
        apply this _ (Finset.mem_cons_self _ _)
        rintro rfl
        exact hat hx
      · have := Submodule.coe_mem (μ a)
        simp only [mem_iInf] at this
        exact this _ (Finset.subset_cons _ hb) ab.symm

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

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
⊢ (∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)) ↔ ∀ (x : R), x ≠ 0 → IsUnit x

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩

Goal state after:
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
⊢ IsUnit x