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

Goal state before:
pp: case tmul
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
x : ↥l23.ker
m : M
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = x ⊗ₜ[R] m

Tactic:
rcases x with ⟨x, (hx : l23 x = 0)⟩

Goal state after:
case tmul
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: case tmul
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
mem : x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l23).ker
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m

Tactic:
rw [LinearMap.exact_iff.1 ex] at mem

Goal state after:
case tmul
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)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
e : H ⊗[R] M ≃ₗ[R]
  ↥l23.ker ⊗[R] M ⧸ (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id).range :=
  quotientTensorEquiv M (Submodule.inclusion complex).range
m : M
x : N2
hx : l23 x = 0
mem : x ⊗ₜ[R] m ∈ (LinearMap.rTensor M l12).range
⊢ ∃ a, (TensorProduct.map (Submodule.inclusion complex).range.subtype LinearMap.id) a = ⟨x, hx⟩ ⊗ₜ[R] m
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ Nonempty (PrimeSpectrum R) ↔ Nontrivial R

Tactic:
refine ⟨fun ⟨p⟩ ↦ ⟨0, 1, fun h ↦ p.2.ne_top ?_⟩, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
x✝ : Nonempty (PrimeSpectrum R)
p : PrimeSpectrum R
h : 0 = 1
⊢ p.asIdeal = ⊤

case refine_2
R : Type u
inst✝ : CommSemiring R
h : Nontrivial R
⊢ Nonempty (PrimeSpectrum R)
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R
⊢ (∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ ∀ p ∈ {J | I ≤ J ∧ J.IsPrime}, f ∈ p

Tactic:
exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩

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

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

Tactic:
SetLike.mem_coe

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ g ∈ (Ideal.span {f}).radical ↔ g ∈ (Ideal.span {f}).radical
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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ 0 * t ^ N = 0

Tactic:
zero_mul

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')

Tactic:
by
  rw [zeroLocus_inf]
  simp

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False

Tactic:
Ideal.mem_comap,

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : g (r • t) ∉ J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
H : 1 ⊗ₜ[R] (algebraMap R T) r ∈ J
⊢ False
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✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑((TensorProduct.mk A B M) 1)

Tactic:
rw [← Module.FaithfullyFlat.lTensor_injective_iff_injective A B]

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : FaithfullyFlat A B
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ Function.Injective ⇑(lTensor B ((TensorProduct.mk A B M) 1))
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈ Ideal.comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal ↔ x ∈ p.asIdeal

Tactic:
Ideal.mem_comap,

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ f x ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal ↔ x ∈ p.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ f x' - f x = 0

Tactic:
sub_eq_zero

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : f x' = f x
⊢ f x' = f x
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
hV : IsOpen[inst✝¹] V
⊢ f '' V = ⋃ i, f '' (V ∩ range Subtype.val)

Tactic:
← Set.image_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hf : ∀ (i : ι), IsOpenMap (f ∘ Subtype.val)
V : Set α
hV : IsOpen[inst✝¹] V
⊢ f '' V = f '' ⋃ i, V ∩ range Subtype.val
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:
by
    simp only [Set.mem_image, Set.mem_ofPred_eq, forall_exists_index, and_imp]
    rintro _ U h₁ h₂ rfl
    exact hf'.isCompact_preimage_of_isOpen h₁ h₂

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
s t : Set X
hst : s ⊆ t
x✝ : ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U
W : Set X
Wc : IsCompact W
Wo : IsOpen[inst✝¹] W
hKW : t ⊆ W
hWU : W ⊆ U
⊢ ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ⊆ W ∧ W ⊆ U

Tactic:
use W, Wc, Wo, subset_trans hst hKW, hWU

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

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set X⦄,
    (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ⊆ W ∧ W ⊆ U) →
      (∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U) → ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

pp: case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U

Tactic:
· intro s t ⟨W₁, Wc₁, Wo₁, hKW₁, hWU₁⟩ ⟨W₂, Wc₂, Wo₂, hKW₂, hWU₂⟩
    exact ⟨W₁ ∪ W₂, Wc₁.union Wc₂, Wo₁.union Wo₂, Set.union_subset_union hKW₁ hKW₂,
      Set.union_subset hWU₁ hWU₂⟩

Goal state after:
case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ t ⊆ W ∧ W ⊆ U
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
PrespectralSpace.isTopologicalBasis.isOpen_iff

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
⊢ IsCompact (V₁ ∩ V₂)

Tactic:
obtain ⟨t, ht⟩ := hc₁.elim_finite_subcover _ (fun i ↦ (U i).2) (by simp [hU.iSup_set_eq_univ])
    convert!
      t.isCompact_biUnion fun i _ ↦
        h₂ i _ _ Set.inter_subset_left ((U i).2.inter ho₁) (h₁ i hc₁ ho₁) Set.inter_subset_left
          ((U i).2.inter ho₂) (h₁ i hc₂ ho₂)
    apply subset_antisymm
    · rintro x ⟨hx₁, hx₂⟩
      obtain ⟨i, hi, hxi⟩ := Set.mem_iUnion₂.mp (ht hx₁)
      exact Set.mem_iUnion₂.mpr ⟨i, hi, by simpa [*]⟩
    · aesop (add simp Set.subset_def)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
algebraize [f]
  rw [← algebraMap_toAlgebra f, faithfullyFlat_algebraMap_iff, flat_algebraMap_iff]
  exact ⟨fun h ↦ ⟨inferInstance, PrimeSpectrum.comap_surjective_of_faithfullyFlat⟩,
    fun ⟨h, hf⟩ ↦ .of_comap_surjective hf⟩

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : p = q
⊢ b.factorization q ≤ a.factorization q

Tactic:
← h'

Goal state after:
case neg
a b p : ℕ
hp : p ∈ (a.lcm b).factorization.support
q : ℕ
hq : q ∈ (a.lcm b).factorization.support
h : b.factorization p ≤ a.factorization p
h' : p = q
⊢ b.factorization p ≤ a.factorization p
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: ⊢ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.Flat).IsStableUnderCobaseChange

Tactic:
RingHom.isStableUnderCobaseChange_toMorphismProperty_iff

Goal state after:
⊢ RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f ↦ f.Flat
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
by
  rcases eq_or_ne a 0 with rfl | ha
  · simp only [dvd_zero]
  rcases eq_or_ne b 0 with rfl | hb
  · simp [factorizationLCMLeft]
  nth_rewrite 2 [← prod_factorization_pow_eq_self ha]
  rw [prod_of_support_subset (s := (lcm a b).factorization.support)]
  · apply prod_dvd_prod_of_dvd; rintro p -; dsimp only; split_ifs with le
    · rw [factorization_lcm ha hb]; apply pow_dvd_pow; exact sup_le le_rfl le
    · apply one_dvd
  · intro p hp; rw [mem_support_iff] at hp ⊢
    rw [factorization_lcm ha hb]; exact (lt_sup_iff.mpr <| .inl <| Nat.pos_of_ne_zero hp).ne'
  · intros; rw [pow_zero]

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

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z) → ∃ s, zeroLocus s = Z

Tactic:
rintro ⟨s, rfl⟩
    exact ⟨_, rfl⟩

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
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } ∈ {p}
⊢ r ∉ p.asIdeal.primeCompl

Tactic:
Set.mem_singleton_iff

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : R
p : PrimeSpectrum R
h : (basicOpen f).carrier = {p}
r : R
hr : ∀ m ∈ Submonoid.powers f, m ∉ Ideal.span {r}
q : Ideal R
prime : q.IsPrime
le : Ideal.span {r} ≤ q
disj : Disjoint ↑q ↑(Submonoid.powers f)
this : { asIdeal := q, isPrime := prime } = p
⊢ r ∉ p.asIdeal.primeCompl
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 : α
h : x ∈ ⊥
⊢ x ∈ H

Tactic:
rw [Subgroup.mem_bot.1 h]

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 : α
h : x ∈ ⊥
⊢ 1 ∈ 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
x : R
⊢ x ∈ vanishingIdeal (Set.range (comap f)) ↔ x ∈ Ideal.comap f (sInf {J | ⊥ ≤ J ∧ J.IsPrime})

Tactic:
simp only [mem_vanishingIdeal, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
    comap_asIdeal, Ideal.mem_comap, bot_le, true_and, Submodule.mem_sInf, Set.mem_ofPred_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
⊢ (∀ (a : PrimeSpectrum S), f x ∈ a.asIdeal) ↔ ∀ (p : Submodule S S), Ideal.IsPrime p → f x ∈ p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ zeroLocus ↑(I * J) = Set.univ

Tactic:
zeroLocus_mul,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
⊢ zeroLocus ↑I ∪ zeroLocus ↑J = Set.univ
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:
grw [Finset.prod_dvd_prod_of_subset _ _ (·) hG, p.prod_primeFactors_dvd]

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: F : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : Monoid M₁
inst✝² : Monoid M₂
inst✝¹ : FunLike F M₁ M₂
inst✝ : MonoidHomClass F M₁ M₂
f : F
hf : Function.Surjective ⇑f
⊢ exponent M₂ ∣ exponent M₁

Tactic:
by
  refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_
  obtain ⟨m₁, rfl⟩ := hf m₂
  rw [← map_pow, pow_exponent_eq_one, map_one]

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := ⋯
ht : closure ↑t = ⊤
⊢ t.card ≤ s.card

Tactic:
suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
    apply Finset.card_filter_le

Goal state after:
G : Type u_1
inst✝ : Group G
s : Finset G
t : Finset ↥(closure ↑s) := s.preimage Subtype.val ⋯
ht : closure ↑t = ⊤
⊢ Set.InjOn Subtype.val ↑t
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case mk
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
g✝ : G ⧸ torsion G
g : G
hne : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ≠ 1
hfin : IsOfFinOrder (Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g)
m : ℕ
mpos : 0 < m
hm : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ^ m = 1
⊢ Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g = 1

Tactic:
obtain ⟨n, npos, hn⟩ := ((QuotientGroup.eq_one_iff _).mp hm).exists_pow_eq_one

Goal state after:
case mk
G : Type u_1
H : Type u_2
inst✝¹ : CommGroup G
inst✝ : CommGroup H
g✝ : G ⧸ torsion G
g : G
hne : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ≠ 1
hfin : IsOfFinOrder (Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g)
m : ℕ
mpos : 0 < m
hm : Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g ^ m = 1
n : ℕ
npos : 0 < n
hn : (fun x ↦ x ^ m) g ^ n = 1
⊢ Quot.mk (⇑(QuotientGroup.leftRel (torsion G))) g = 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) ≡ Nat.card (G ⧸ H) [MOD p]

Tactic:
← Nat.card_congr (fixedPointsMulLeftCosetsEquivQuotient H)

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≡ Nat.card (G ⧸ H) [MOD p]
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
⊢ False

Tactic:
cases (finite_or_infinite N).symm

Goal state after:
case inl
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Infinite N
⊢ False

case inr
M : Type u_4
N : Type u_5
inst✝³ : AddGroup M
inst✝² : AddGroup N
inst✝¹ : Infinite M
inst✝ : Nontrivial N
hMN : IsAddCyclic (ZMod 0 × ZMod (Nat.card N))
h✝ : Finite N
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝ : Finite M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
cases (finite_or_infinite N).symm

Goal state after:
case refine_1.inr.inl
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Finite M
h✝ : Infinite N
⊢ (Nat.card M).Coprime (Nat.card N)

case refine_1.inr.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Finite M
h✝ : Finite N
⊢ (Nat.card M).Coprime (Nat.card N)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ n ∣ Nat.card G
⊢ Nat.card ↥⊥ = p ^ 0

Tactic:
card_bot,

Goal state after:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
p n : ℕ
inst✝ : Fact (Nat.Prime p)
hdvd : p ^ n ∣ Nat.card G
⊢ 1 = p ^ 0
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
i : Fin s₂.length
⊢ Iso (s₁.toFun ((Exists.choose h).symm i).castSucc, s₁.toFun ((Exists.choose h).symm i).succ)
    (s₂.toFun i.castSucc, s₂.toFun i.succ)

Tactic:
simpa using h.choose_spec (h.choose.symm i)

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
⊢ Equivalent (snoc s₁ x₁ hsat₁) (snoc s₂ x₂ hsat₂)

Tactic:
have he_castSucc (j : Fin s₁.length) :
      e j.castSucc = (hequiv.choose j).castSucc := by
    simp [e, finSuccEquivLast_castSucc, Functor.mapEquiv_apply]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
⊢ Equivalent (snoc s₁ x₁ hsat₁) (snoc s₂ x₂ hsat₂)