mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x✝ y✝ : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x✝ y✝
x y : FreeAddMonoid (R × ((i : ι) → s i))
⊢ (FreeAddMonoid.lift φ) (x + y) = (FreeAddMonoid.lift φ) (y + x)

Tactic:
map_add,

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x✝ y✝ : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x✝ y✝
x y : FreeAddMonoid (R × ((i : ι) → s i))
⊢ (FreeAddMonoid.lift φ) x + (FreeAddMonoid.lift φ) y = (FreeAddMonoid.lift φ) y + (FreeAddMonoid.lift φ) x
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx : (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0)) = x
hy : (cast R M ⋯) (mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = y
⊢ (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0 + y ⊗ₜ[R] (tprod R) Fin.elim0)) = x + y

Tactic:
map_add,

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx : (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0)) = x
hy : (cast R M ⋯) (mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = y
⊢ (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0) + mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = x + y
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx : (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0)) = x
hy : (cast R M ⋯) (mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = y
⊢ (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0) + mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = x + y

Tactic:
map_add,

Goal state after:
case add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : ⨂[R] (i : Fin n), M
hx : (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0)) = x
hy : (cast R M ⋯) (mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = y
⊢ (cast R M ⋯) (mulEquiv (x ⊗ₜ[R] (tprod R) Fin.elim0)) + (cast R M ⋯) (mulEquiv (y ⊗ₜ[R] (tprod R) Fin.elim0)) = x + y
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹) • v n✝ = 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ x ∈ s, f x • v x + (∑ i ∈ s, f i * ((-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹)) • v ↑n = 0

Tactic:
← mul_assoc,

Goal state after:
case insert.specialize_2
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
hfv : ∑ x ∈ s, f x • v x + ((-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹) • v n✝ = 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ x ∈ s, f x • v x + (∑ x ∈ s, (f x * -if x = ↑n then 0 else a' x) * ↑hj.unit⁻¹) • v ↑n = 0
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x✝ x y : ⨂[R] (i : ι), s i
hx : (lift (constOfIsEmpty R s 1)) x • (tprod R) isEmptyElim = x
hy : (lift (constOfIsEmpty R s 1)) y • (tprod R) isEmptyElim = y
⊢ (lift (constOfIsEmpty R s 1)) (x + y) • (tprod R) isEmptyElim = x + y

Tactic:
map_add,

Goal state after:
case refine_2
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁰ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁹ : (i : ι) → AddCommMonoid (s i)
inst✝⁸ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
E : Type u_9
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
F : Type u_10
inst✝³ : AddCommMonoid F
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x✝ x y : ⨂[R] (i : ι), s i
hx : (lift (constOfIsEmpty R s 1)) x • (tprod R) isEmptyElim = x
hy : (lift (constOfIsEmpty R s 1)) y • (tprod R) isEmptyElim = y
⊢ ((lift (constOfIsEmpty R s 1)) x + (lift (constOfIsEmpty R s 1)) y) • (tprod R) isEmptyElim = x + y
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
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K * Ideal.span {z} ≤ ann
⊢ I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I

Tactic:
← mul_assoc,

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
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K * Ideal.span {z} ≤ ann
⊢ I ^ (n - 1) * J * Ideal.span {z} ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ associatedPrimes R M = ∅

Tactic:
ext; simp only [Set.mem_empty_iff_false, iff_false]
  apply not_isAssociatedPrime_of_subsingleton

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
⊢ x ∣ T.gcd fun x ↦ normalize b * id x

Tactic:
Finset.dvd_gcd_iff

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
⊢ ∀ b_1 ∈ T, x ∣ normalize b * id b_1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_2
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
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I

Tactic:
use Units.mapEquiv (FractionalIdeal.ringEquivOfRingEquiv _ _ f).symm.toMulEquiv I
    refine ⟨?_, by simp [← Units.val_inj]⟩
    · use Units.map (IsFractionRing.ringEquivOfRingEquiv f (K := K)
        (L := L)).symm.toRingHom u
      simp only [IsFractionRing.ringEquivOfRingEquiv_symm, RingEquiv.toRingHom_eq_coe,
        Units.coe_map, MonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.toMulEquiv_eq_coe,
        RingEquiv.coe_toMulEquiv_symm, Units.coe_mapEquiv]
      rw [← FractionalIdeal.ringEquivOfRingEquiv_spanSingleton,
        ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]
      rfl

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
⊢ p ∈ freeLocus A (A ⊗[R] M)

Tactic:
mem_freeLocus_iff_tensor _ Aₚ

Goal state after:
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
⊢ Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ comap includeRight.toRingHom q ∈ comap (algebraMap R S) ⁻¹' {p}

Tactic:
by
    simp only [AlgHom.toRingHom_eq_coe, Set.mem_preimage, ← comap_comp_apply,
      AlgHom.comp_algebraMap_of_tower]
    exact (residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩

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
⊢ Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))

Tactic:
let algebra : Algebra Rₚ Aₚ := (Localization.localRingHom
    (comap (algebraMap R A) p).asIdeal p.asIdeal (algebraMap R A) rfl).toAlgebra

Goal state after:
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
⊢ Free Aₚ (Aₚ ⊗[A] (A ⊗[R] M))
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
⊢ (fun q ↦
        {
          asIdeal :=
            RingHom.ker
              (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                  (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
          isPrime := ⋯ })
      ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q) =
    q

Tactic:
ext x
    obtain ⟨r, hr, s, e⟩ := Ideal.Fiber.exists_smul_eq_one_tmul _ x
    have := @PrimeSpectrum.isPrime -- times out if removed
    rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), iff_comm,
      ← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e]
    · simp
    · rw [← Ideal.mem_comap, ← PrimeSpectrum.comap_asIdeal]
      convert! hr
      exact (residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩
    · simpa [-Algebra.algebraMap_self, -AlgHom.commutes, -AlgHom.map_algebraMap,
        -Ideal.ResidueField.map_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm

Tactic:
refine (Topology.IsEmbedding.of_comp_iff .subtypeVal).mp ?_

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Topology.IsEmbedding (Subtype.val ∘ ⇑(preimageOrderIsoFiber R S p).symm)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * (a⁻¹ * b⁻¹) = 1

Tactic:
← mul_assoc,

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ = 1
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑(mul' R A ∘ₗ lTensor A (↑I).subtype)

Tactic:
classical
  rw [← Set.image2_mul, ← Finset.coe_image₂, mem_span_finset] at one_mem
  set S := T.image₂ (· * ·) T'
  obtain ⟨r, hr⟩ := one_mem
  choose a ha b hb eq using fun i : S ↦ Finset.mem_image₂.mp i.2
  let f : I →ₗ[R] S → R := .pi fun i ↦ (LinearEquiv.ofInjective
      (Algebra.linearMap R A) (FaithfulSMul.algebraMap_injective R A)).symm.comp <|
    restrict (mulRight R (r i • a i)) fun x hx ↦ by
      rw [← one_eq_range, ← I.mul_inv]; exact mul_mem_mul hx (I⁻¹.1.smul_mem _ <| hT <| ha i)
  have hf (x : I.1) (i : S) : algebraMap R A (f x i) = x * r i • a i := by
    dsimp [f, ← Algebra.linearMap_apply]
    exact LinearEquiv.ofInjective_symm_apply ..
  let g : (S → R) →ₗ[R] I := .lsum _ _ ℕ fun i ↦ .toSpanSingleton _ _ ⟨b i, hT' <| hb i⟩
  have hgf : g ∘ₗ f = .id := LinearMap.ext fun x ↦ Subtype.ext <| by
    simp only [g, lsum_apply, comp_apply, LinearMap.sum_apply, toSpanSingleton_apply, proj_apply]
    simp_rw [coe_sum, coe_smul, Algebra.smul_def, hf, mul_assoc, ← Finset.mul_sum,
      Algebra.smul_mul_assoc, eq, (Finset.sum_coe_sort ..).trans hr.2, mul_one, id_apply]
  set m := mul' R A ∘ₗ I.1.subtype.lTensor A
  have eq : (piScalarRight R R A S).toLinearMap ∘ₗ f.lTensor A =
      (.pi fun i : S ↦ mulRight R (r i • a i)) ∘ₗ m := by
    ext; simp [(Algebra.smul_def ..).trans (Algebra.commutes ..), hf, m, mul_assoc]
  have := (piScalarRight R R A S).injective.comp <| injective_of_comp_eq_id
    (f.lTensor A) (g.lTensor A) <| by rw [← lTensor_comp, hgf, lTensor_id]
  rw [← LinearEquiv.coe_toLinearMap, ← coe_comp, eq, coe_comp] at this
  refine ⟨.of_split f g hgf, .of_comp this, range_eq_top.mp ?_⟩
  rw [show m = mulMap ⊤ I ∘ₗ (topEquiv.symm.rTensor I.1).toLinearMap by ext; rfl, range_comp,
    LinearEquiv.range, map_top, mulMap_range, top_mul_eq_top_of_mul_eq_one I.inv_mul]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inr
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h✝ : Infinite F
β α : E
⊢ ∃ α_1, F⟮α, β⟯ = F⟮α_1⟯

Tactic:
exact primitive_element_inf_aux_of_finite_intermediateField F α β

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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ¬∃ i, e ∈ I i
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))

Tactic:
not_exists

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ M.Dep (insert e (⋃ i, I i))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E ∧ ⋃ i, I i ⊆ M.E

Tactic:
iUnion_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
X I : ι → Set α
hI : ∀ (i : ι), M.IsBasis (I i) (X i)
h_ind : M.Indep (⋃ i, I i)
e : α
he' : ∀ (x : ι), e ∉ I x
i : ι
hes : e ∈ X i
⊢ e ∈ M.E ∧ ∀ (i : ι), I i ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
this : Nonempty ↑Xs
⊢ M.IsBasis I (⋃ i, ↑i)

Tactic:
exact IsBasis.isBasis_iUnion _ fun X ↦ h X X.prop

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ * (submoduleAlgebra e * submoduleAlgebra f) =
    ⊤ *
      (R ∙
        ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
                tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
            1))
⊢ IsUnit
    (R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1))

Tactic:
← mul_assoc,

Goal state after:
case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  ⊤ * submoduleAlgebra e * submoduleAlgebra f =
    ⊤ *
      (R ∙
        ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
                tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
            1))
⊢ IsUnit
    (R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1))
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ P K ∧ K ⊆ X) J

Tactic:
obtain ⟨Y, ⟨hY, hIY, hYX⟩, hY'⟩ :=
    Finite.exists_maximalFor' ncard _ hfin ⟨I, hI, rfl.subset, hIX⟩

Goal state after:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) j → Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ P K ∧ K ⊆ X) J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N <r M
⊢ N ≠ M

Tactic:
by
  rintro rfl; rw [← ofMatroid_lt_iff] at h; simp at h

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

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

Tactic:
and_iff_left (show X ⊆ R from hX)

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
nth_rw 2 [← insert_eq_of_mem he]

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) (insert e C)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
⊢ e ∈ M.loops

Tactic:
← closure_empty,

Goal state after:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
⊢ e ∈ M.closure ∅
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∪ M.loops) = M.closure X

Tactic:
← closure_empty,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (X ∪ M.closure ∅) = M.closure X