mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
⊢ (Extension.H1Cotangent.map
        (((Generators.self R S').defaultHom (Generators.self R S)).toExtensionHom.comp
          ((Generators.self R S).defaultHom (Generators.self R S')).toExtensionHom))
      x =
    x

Tactic:
Extension.H1Cotangent.map_eq,

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
⊢ (Extension.H1Cotangent.map ?g) x = x

case g
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := ⋯
this✝³ : Algebra S' S := ⋯
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S
⊢ (Generators.self R S).toExtension.Hom (Generators.self R S).toExtension
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S'
⊢ (Extension.H1Cotangent.map
        (((Generators.self R S).defaultHom (Generators.self R S')).toExtensionHom.comp
          ((Generators.self R S').defaultHom (Generators.self R S)).toExtensionHom))
      x =
    x

Tactic:
Extension.H1Cotangent.map_eq,

Goal state after:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := e.toRingEquiv.toRingHom.toAlgebra
this✝³ : Algebra S' S := e.symm.toRingEquiv.toRingHom.toAlgebra
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S'
⊢ (Extension.H1Cotangent.map ?g) x = x

case g
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
ι : Type w
ι' : Type u_1
P : Generators R S ι
S' : Type u_2
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S'
T : Type w
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : Algebra S' T
inst✝ : IsScalarTower R S' T
e : S ≃ₐ[R] S'
this✝⁴ : Algebra S S' := ⋯
this✝³ : Algebra S' S := ⋯
this✝² : IsScalarTower R S S'
this✝¹ : IsScalarTower R S' S
this✝ : IsScalarTower S S' S
this : IsScalarTower S' S S'
x : H1Cotangent R S'
⊢ (Generators.self R S').toExtension.Hom (Generators.self R S').toExtension
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case h
R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
x : M
r : ↑↑t
S : Submonoid R := Submonoid.powers ↑r
n₁ : ℕ
hn₁ : (f r) (↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • x ∈
    Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
Submonoid.smul_def

Goal state after:
case h
R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
x : M
r : ↑↑t
S : Submonoid R := Submonoid.powers ↑r
n₁ : ℕ
hn₁ : (f r) (↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • x) ∈ Submodule.span R ↑(s₁ r)
n₂ : ℕ
hn₂ :
  ↑⟨(fun x ↦ ↑r ^ x) n₂, ⋯⟩ • ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • x ∈
    Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S (f r) (s₁ r))
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
⊢ (baseChange A N).spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := N.exists_span_set_card_eq_spanRank

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ (baseChange A N).spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:

Tactic:
_ = (-1) ^ (i : ℕ) • f (v i) (i.removeNth v) + (-1) ^ (j : ℕ) • f (v j) (j.removeNth v) := by
        refine Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_
        rcases exists_succAbove_eq hki.symm with ⟨i, rfl⟩
        rcases exists_succAbove_eq hkj.symm with ⟨j, rfl⟩
        rw [(f (v k)).map_eq_zero_of_eq _ hvij (ne_of_apply_ne _ hij), smul_zero]
      _ = 0 := by
        rw [hvij, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq] <;> assumption

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (toTensorPower R M n) ((ιMulti R n) v) = ∑ σ, Perm.sign σ • (tprod R) fun i ↦ v (σ i)

Tactic:
by
  dsimp [toTensorPower]
  simp only [alternatingMapLinearEquiv_apply_ιMulti,
    MultilinearMap.alternatization_apply, MultilinearMap.domDomCongr_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.span R (Set.range f) = ⊤

Tactic:
← map_tensorProduct_mk_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.map ((TensorProduct.mk R k M) 1) (Submodule.span R (Set.range f)) = ⊤
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
x : M₂ ⊗[R] N₁
hx : (LinearMap.lTensor M₃ g₁) ((LinearMap.rTensor N₁ f₂) x) = 0
this✝ : (LinearMap.rTensor N₂ f₂) ((LinearMap.lTensor M₂ g₁) x) = 0
z : M₁ ⊗[R] N₁
hy : (LinearMap.rTensor N₂ f₁) ((LinearMap.lTensor M₁ g₁) z) = (LinearMap.lTensor M₂ g₁) x
this : (LinearMap.lTensor M₁ g₂) ((LinearMap.lTensor M₁ g₁) z) = 0
⊢ (LinearMap.lTensor M₂ g₁) ((LinearMap.rTensor N₁ f₁) z) = (LinearMap.lTensor M₂ g₁) x

Tactic:
simp only [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.lTensor_comp_rTensor,
      LinearMap.rTensor_comp_lTensor]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: case add
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
a b : ↥M ⊗[R] ↥N
ha : (M.mulMap N) a ∈ M * N
hb : (M.mulMap N) b ∈ M * N
⊢ (M.mulMap N) (a + b) ∈ M * N

Tactic:
rw [map_add]; exact add_mem ha hb

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: case smul_tprod.e_a.e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ (Fin.append Fin.elim0 a ∘ Fin.cast ⋯) i = a i

Tactic:
rw [Fin.elim0_append]

Goal state after:
case smul_tprod.e_a.e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
i : Fin n
⊢ ((a ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) i = a i
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝¹ : Finite ι
this✝ : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
hi : Surjective ⇑i
this : Module.Finite R ↥i.ker
iequiv : (ι →₀ R) ≃ₗ[R] M := LinearEquiv.ofBijective i ⋯
j : ι
⊢ { repr := iequiv.symm } j = v j

Tactic:
simp [iequiv, i]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
I : Ideal R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
hI : I.IsPrime
x : M
hx : I = (⊥.colon {x}).radical
⊢ False

Tactic:
apply hI.ne_top

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
I : Ideal R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
hI : I.IsPrime
x : M
hx : I = (⊥.colon {x}).radical
⊢ I = ⊤
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case refine_2.refine_3
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ (liftQ { asIdeal := ⊥.colon {N₁.mkQ x}, isPrime := hx }.asIdeal
        ((N₁.submoduleOf N₂).mkQ ∘ₗ toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩) ⋯).range =
    ⊤

Tactic:
range_liftQ,

Goal state after:
case refine_2.refine_3
A : Type u
inst✝² : CommRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
⊢ ((N₁.submoduleOf N₂).mkQ ∘ₗ toSpanSingleton A ↥N₂ ⟨x, hxN₂⟩).range = ⊤
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
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
⊢ False

Tactic:
have h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal := e ▸ p₂.asIdeal.primeCompl.mul_mem ht 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
h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal
⊢ False
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
h₁ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
⊢ False

Tactic:
have h₃ : t ∉ p₂.asIdeal.comap g := fun h ↦ h₂ (Ideal.mul_mem_left _ _ h)

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] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal
h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal
h₃ : t ∉ Ideal.comap g p₂.asIdeal
⊢ False
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)ˣ
⊢ (mk K') ((Units.map ↑(canonicalEquiv R⁰ K K')) I) = (mk K) I

Tactic:
rw [ClassGroup.mk_def, ClassGroup.mk_def, ← MonoidHom.comp_apply (Units.map _),
      ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans,
      FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
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, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩

Tactic:
rw [piecewise', piecewise_apply_left (f := (f₁.comap
    ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
    (hx := hx)]

Goal state after:
X : Type u_1
Z : Type u_3
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, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₁
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, hx⟩ = f₁ ⟨↑x, hx⟩
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G < ⊤

Tactic:
lt_top_iff_ne_top

Goal state after:
G : Type u_1
inst✝¹ : Group G
hG : IsSolvable G
inst✝ : Nontrivial G
⊢ _root_.commutator G ≠ ⊤
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✝¹ : Module.Finite R M
inst✝ : Flat R M
⊢ ∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)

Tactic:
exact fun x ↦ Module.free_of_flat_of_isLocalRing

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
inst✝ : Free R M
p : PrimeSpectrum R
⊢ rankAtStalk M p = ↑(finrank R M) p

Tactic:
simp [rankAtStalk, finrank_of_isLocalizedModule_of_free _ p.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f

Tactic:
refine ⟨fun h ↦ ?_, Flat.lTensor_preserves_injective_linearMap _⟩
  rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]
  simpa using Flat.lTensor_preserves_injective_linearMap _ h

Goal state after:
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)ˣ
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑(mul' R A ∘ₗ lTensor A (↑I).subtype)

Tactic:
obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.inv_mul ▸ one_le.mp le_rfl)
  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.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
hE,

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty Indep X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), IsBase B → B ⊆ E

Tactic:
hE,

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), IsBase B → B ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis (X ∩ I) X

Tactic:
uniqueBaseOn_isBasis_iff hX

Goal state after:
α : Type u_1
E I X : Set α
hX : X ⊆ E
⊢ X ∩ I = X ∩ I
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E : Set α
⊢ (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

Tactic:
by
  rw [← uniqueBaseOn_inter_ground_eq]
  refine ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)
  rw [dual_isBase_iff, uniqueBaseOn_isBase_iff inter_subset_right,
    uniqueBaseOn_isBase_iff sdiff_subset, uniqueBaseOn_ground]
  exact ⟨fun h ↦ by rw [← sdiff_sdiff_cancel_left hB, h, sdiff_inter_self_eq_sdiff],
    fun h ↦ by rw [h, inter_comm I]; simp⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hIJ : J'.encard < J.encard
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False

Tactic:
exact hIJ.not_ge (encard_mono hJJ')

Goal state after: