mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ s.attach.prod x ∈ annihilator R M

Tactic:
rw [← Submodule.annihilator_top, ← hs, Submodule.mem_annihilator_span]

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
⊢ ∀ (n : ↑↑s), s.attach.prod x • ↑n = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = ↑(y • n)

Tactic:
SetLike.val_smul,

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = y • ↑n
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
κ : Type u_1
ι : Type u_2
m : Basis κ R ↥M
n : Basis ι R ↥N
H : Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))
⊢ M.LinearDisjoint N

Tactic:
let i0 := (finsuppTensorFinsupp' R κ ι).symm
  let i1 := TensorProduct.congr m.repr n.repr
  let i := mulMap M N ∘ₗ (i0.trans i1.symm).toLinearMap
  have : i = Finsupp.linearCombination R fun i : κ × ι ↦ (m i.1 * n i.2 : S) := by
    ext x
    simp [i, i0, i1, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
  simp_rw [← this, i, LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.injective_comp] at H
  exact ⟨H⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
⊢ Function.Injective ⇑(mulMap 1 N)

Tactic:
← Algebra.toSubmodule_bot,

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
⊢ Function.Injective ⇑((Subalgebra.toSubmodule ⊥).mulMap N)
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ Function.Injective ⇑(M.mulMap 1)

Tactic:
← Algebra.toSubmodule_bot,

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ Function.Injective ⇑(M.mulMap (Subalgebra.toSubmodule ⊥))
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))

Tactic:
have h1 : Function.Injective i1 := Module.Flat.lTensor_preserves_injective_linearMap _ hn

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] (κ →₀ R) ⊗[R] ↥N := LinearMap.lTensor (κ →₀ R) (Finsupp.linearCombination R n)
i2 : (κ →₀ R) ⊗[R] ↥N →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.rTensor (↥N) (Finsupp.linearCombination R m)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0
h1 : Function.Injective ⇑i1
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
⊢ ∀ y ∈ K, I ≤ N.colon {y • x}

Tactic:
intro y hy p hp

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
y : R
hy : y ∈ K
p : R
hp : p ∈ I
⊢ p ∈ N.colon {y • x}
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
⊢ ∃ x', I = N.colon {x'}

Tactic:
have step1 : ∀ y ∈ K, I ≤ colon N {y • x} := by
    intro y hy p hp
    rw [mem_colon_singleton, smul_smul, ← mem_colon_singleton]
    apply hJ
    simpa [K, ← mul_assoc, mul_pow_sub_one hn0] using mul_mem_mul hp hy

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
⊢ ∃ x', I = N.colon {x'}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : f y = a ^ k • x
b : R
n : ℕ
hb : b ^ n • x = 0
⊢ f (b ^ n • y) = f 0

Tactic:
rw [map_smul, h, smul_comm, hb, smul_zero, map_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ False

Tactic:
have h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal := e ▸ p₁.asIdeal.mul_mem_left (1 ⊗ₜ[R] (r • t)) hxp₁

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
⊢ False
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J) →
    ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J') →
    ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J

Tactic:
· rintro ⟨x, rfl⟩
    rw [Units.val_mul, hI, coe_toPrincipalIdeal, mul_comm,
      spanSingleton_mul_coeIdeal_eq_coeIdeal] at hJ
    exact ⟨_, _, sec_fst_ne_zero x.ne_zero,
      sec_snd_ne_zero (R := R) le_rfl (x : FractionRing R), hJ⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I J : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' J' : Ideal R
hI : ↑I = ↑I'
hJ : ↑J = ↑J'
⊢ (∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J') →
    ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑((canonicalEquiv R⁰ K K').trans (canonicalEquiv R⁰ K' (FractionRing R)))) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)

Tactic:
FractionalIdeal.canonicalEquiv_trans_canonicalEquiv

Goal state after:
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I)
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ mk0 I = mk0 J ↔ ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J

Tactic:
refine (ClassGroup.equiv K).injective.eq_iff.symm.trans ?_

Goal state after:
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (equiv K) (mk0 I) = (equiv K) (mk0 J) ↔ ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x},
      ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Tactic:
tfae_have 5 → 1
  | h, s => by
    refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_
    rcases h x with ⟨U, hU, hxU, eq⟩
    exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
tfae_5_to_1 : (∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x) → IsLocallyConstant f
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x},
      ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ Subtype.val ⁻¹' C₁ ∪ Subtype.val ⁻¹' C₂ = univ

Tactic:
by simpa [eq_univ_iff_forall] using! h₀

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

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime (comap (algebraMap R A) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom (comap (algebraMap R A) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
⊢ algebraMap R Aₚ = (algebraMap Rₚ Aₚ).comp (algebraMap R Rₚ)

Tactic:
simp [Rₚ, Aₚ, algebra, RingHom.algebraMap_toAlgebra, Localization.localRingHom,
        ← IsScalarTower.algebraMap_eq]

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = map ⁅H, H⁆.subtype ⊤

Tactic:
← MonoidHom.range_eq_map,

Goal state after:
case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ ⁅H.subtype.range, H.subtype.range⁆ = map ⁅H, H⁆.subtype ⊤
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ ⁅H.subtype.range, H.subtype.range⁆ = map ⁅H, H⁆.subtype ⊤

Tactic:
← MonoidHom.range_eq_map,

Goal state after:
case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆.subtype.range
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ U, IsOpen U ∧ ⟨x, hx⟩ ∈ U ∧ ∀ x' ∈ U, rankAtStalk M ↑x' = rankAtStalk M ↑⟨x, hx⟩

Tactic:
refine ⟨Subtype.val ⁻¹' basicOpen f, (basicOpen f).2.preimage continuous_subtype_val, hf, ?_⟩

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∀ x' ∈ Subtype.val ⁻¹' ↑(basicOpen f), rankAtStalk M ↑x' = rankAtStalk M ↑⟨x, hx⟩
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩

Tactic:
have hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl := by
    simpa [Submonoid.powers_le, Ideal.primeCompl]

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : p ∈ freeLocus R M
hp : ⟨p, hp''⟩ ∈ Subtype.val ⁻¹' ↑(basicOpen f)
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
⊢ rankAtStalk M ↑⟨p, hp''⟩ = rankAtStalk M ↑⟨x, hx⟩
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
⊢ TensorProduct.comm R M M = LinearEquiv.refl R (M ⊗[R] M)

Tactic:
let ff (P : Ideal R) [P.IsMaximal] := TensorProduct.map (f P) (f P)

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
⊢ TensorProduct.comm R M M = LinearEquiv.refl R (M ⊗[R] M)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hB : M.IsBase B
hI : M.Indep I
hBI : B ⊆ I
B' : Set α
hB' : M.IsBase B'
hB'I : I ⊆ B'
⊢ I ⊆ B

Tactic:
hB.eq_of_subset_isBase hB' (hBI.trans hB'I)

Goal state after:
α : Type u_1
M : Matroid α
B I : Set α
hB : M.IsBase B
hI : M.Indep I
hBI : B ⊆ I
B' : Set α
hB' : M.IsBase B'
hB'I : I ⊆ B'
⊢ I ⊆ B'
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ insert f B \ {e} ⊆ B'

Tactic:
rw [sdiff_subset_iff, insert_subset_iff, union_comm, ← sdiff_subset_iff, h,
    and_iff_left rfl.subset]

Goal state after:
α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f B \ {e})
hne : f ≠ e
⊢ f ∈ B' ∪ {e}
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ↔ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X ∩ M.E) I

Tactic:
maximal_iff_maximal_of_imp_of_forall

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ Maximal ?m.25 I ↔ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X ∩ M.E) I

case hPQ
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, ?m.25 x → M.Indep x ∧ x ⊆ X

case h
α : Type u_1
M : Matroid α
I X : Set α
⊢ ∀ ⦃x : Set α⦄, M.Indep x ∧ x ⊆ X → ∃ y, x ⊆ y ∧ ?m.25 y

α : Type u_1
M : Matroid α
I X : Set α
⊢ Set α → Prop
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
I : Set α
M : Matroid α
h : I = ∅
⊢ M.IsBasis I ∅

Tactic:
by (rw [h]; exact M.empty_indep.isBasis_self)

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hY : Y ⊆ M.E
⊢ ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis X (hXY.trans hY)
  obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)
  exact ⟨_, _, hI, hJ, hIJ⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R

Tactic:
by
  rw [isBasis_iff_isBasis'_subset_ground, isBasis'_restrict_iff, restrict_ground_eq,
    and_congr_left_iff, ← isBasis'_iff_isBasis_inter_ground]
  intro hXR
  rw [inter_eq_self_of_subset_left hXR, and_iff_left_iff_imp]
  exact fun h ↦ h.subset.trans hXR

Goal state after:
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ B, IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun x ↦ ∃ B, IsBase B ∧ x ⊆ B) X

Tactic:
obtain ⟨B, hB, hfin⟩ := exists_finite_base

Goal state after:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty (fun x ↦ ∃ B, IsBase B ∧ x ⊆ B) X
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
IsBase : Set α → Prop
exists_finite_base : ∃ B, IsBase B ∧ B.Finite
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
⊢ (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).RankFinite

Tactic:
obtain ⟨B, hB, hfin⟩ := exists_finite_base

Goal state after:
α : Type u_1
E : Set α
IsBase : Set α → Prop
isBase_exchange : ExchangeProperty IsBase
subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E
B : Set α
hB : IsBase B
hfin : B.Finite
⊢ (Matroid.ofExistsFiniteIsBase E IsBase ⋯ isBase_exchange subset_ground).RankFinite