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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
x : ↥P'.ker
y : P.Ring
y_in : y ∈ P.ker
hy : f.toRingHom y = ↑x
⊢ (map f) (mk ⟨y, y_in⟩) = mk x

Tactic:
by simp [hy]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: case left
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ Submodule.span S (Set.range pres.differentialsSolution.var) = ⊤

pp: case right
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)

Tactic:
· rw [← Module.Relations.Solution.surjective_π_iff_span_eq_top, ← comm₂₃]
    exact Extension.toKaehler_surjective.comp pres.cotangentSpaceBasis.repr.symm.surjective

Goal state after:
case right
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
⊢ pres.differentialsSolution.π.ker = Submodule.span S (Set.range pres.differentialsRelations.relation)
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ p, IsEmpty p.R) → Free A M

Tactic:
rintro ⟨p, h⟩

Goal state after:
case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
p : Presentation A M
h : IsEmpty p.R
⊢ Free A M
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: case h.right
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i ↦ x (Finsupp.single i 1)
this : ∑ i, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i, f' i * a' i j = 0
j : Fin k
⊢ ((linearCombination R fun i ↦ equivFunOnFinite.symm (a' i)) f) j = 0 j

Tactic:
simp only [linearCombination_apply, zero_smul, implies_true, sum_fintype, finsetSum_apply]

Goal state after:
case h.right
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i ↦ x (Finsupp.single i 1)
this : ∑ i, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i, f' i * a' i j = 0
j : Fin k
⊢ ∑ i, (f i • equivFunOnFinite.symm (a' i)) j = 0 j
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
k : ℕ
a' : (Fin l →₀ R) →ₗ[R] Fin k →₀ R
y' : (Fin k →₀ R) →ₗ[R] M
ha'y' : x' = y' ∘ₗ a'
ha' : a' f' = 0
j : Fin k
⊢ (a' (equivFunOnFinite.symm f)) j = 0

Tactic:
simpa using DFunLike.congr_fun ha' j

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Subsingleton (LocalizedModule.Away 1 M) ↔ Subsingleton M

Tactic:
LocalizedModule.subsingleton_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers 1, r • m = 0) ↔ Subsingleton M
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R M
p : Ideal R
inst✝ : p.IsPrime
φ : N →ₗ[R] M
hφ : Function.Surjective ⇑((LocalizedModule.map p.primeCompl) φ)
⊢ ∃ a ∉ p, Function.Surjective ⇑((LocalizedModule.map (Submonoid.powers a)) φ)

Tactic:
by
  simp_rw [φ.localizedMap_surjective_iff_subsingleton_localized_coker] at hφ ⊢
  exact LocalizedModule.exists_subsingleton_away p

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
l : Fin (n + n)
⊢ Even (if n + n ≤ ↑l + ↑l then ↑l + ↑l - (n + n) else ↑l + ↑l)

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
l : Fin (n + n)
h : n + n ≤ ↑l + ↑l
⊢ Even (↑l + ↑l - (n + n))

case neg
n : ℕ
l : Fin (n + n)
h : ¬n + n ≤ ↑l + ↑l
⊢ Even (↑l + ↑l)
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
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M

Tactic:
← Submodule.subsingleton_iff R,

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
⊢ Subsingleton (Submodule R (k ⊗[R] M)) ↔ Subsingleton M
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
⊢ ⊥ = ⊤ ↔ Subsingleton M

Tactic:
← Submodule.subsingleton_iff R,

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
⊢ ⊥ = ⊤ ↔ Subsingleton (Submodule R M)
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✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : ↑⊤ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)

Tactic:
Submodule.top_coe

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✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : Set.univ ⊆ ↑(Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)))
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)
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
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
r : R₁
f : (i : ι) → s i
⊢ tprodCoeff R (r • (0, f).1) (0, f).2 = 0

Tactic:
by simp [zero_tprodCoeff]

Goal state after:
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
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : ¬s.card ≤ 1
⊢ False

Tactic:
rw [not_le, ← Fintype.card_coe, Fintype.one_lt_card_iff_nontrivial] at hs

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
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
⊢ False
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
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (⊥.colon {x}).radical M
r : R
⊢ (∃ n, r ^ n • x ∈ ⊥) ↔ ∃ n, r ^ n • f x ∈ ⊥

Tactic:
mem_bot,

Goal state after:
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'
hf : Function.Injective ⇑f
x : M
h : IsAssociatedPrime (⊥.colon {x}).radical M
r : R
⊢ (∃ n, r ^ n • x = 0) ↔ ∃ n, r ^ n • f x = 0
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
N : ι ⊕ ι₂ → Type u_12
inst✝¹ : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι₂) → Module R (N i)
a : (i₁ : ι) → N (Sum.inl i₁)
b : (i₂ : ι₂) → N (Sum.inr i₂)
⊢ (tmulEquivDep R N) (((tprod R) fun i₁ ↦ a i₁) ⊗ₜ[R] (tprod R) fun i₂ ↦ b i₂) = ⨂ₜ[R] (i : ι ⊕ ι₂), Sum.rec a b i

Tactic:
simp [tmulEquivDep]

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

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
N : ι ⊕ ι₂ → Type u_12
inst✝¹ : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι₂) → Module R (N i)
f : (i : ι ⊕ ι₂) → N i
⊢ (tmulEquivDep R N).symm (⨂ₜ[R] (i : ι ⊕ ι₂), f i) =
    ((tprod R) fun i₁ ↦ f (Sum.inl i₁)) ⊗ₜ[R] (tprod R) fun i₂ ↦ f (Sum.inr i₂)

Tactic:
simp [tmulEquivDep]

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

Goal state before:
pp: case neg.refine_1
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
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
hb : b ∈ (⊥.colon {x}).radical
⊢ b ∈ (⊥.colon {g x}).radical

Tactic:
refine Ideal.radical_mono (fun b hb ↦ ?_) hb

Goal state after:
case neg.refine_1
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
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b✝ : R
hb✝ : b✝ ∈ (⊥.colon {x}).radical
b : R
hb : b ∈ ⊥.colon {x}
⊢ b ∈ ⊥.colon {g x}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case neg.refine_2
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
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : b ^ n • g x ∈ ⊥
⊢ b ∈ p

Tactic:
mem_bot,

Goal state after:
case neg.refine_2
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
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {g x}).radical
n : ℕ
hb : b ^ n • g x = 0
⊢ b ∈ p
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x✝¹ : I.IsPrime
x✝ : ∃ x, I = ⊥.colon {x}
x : M
h : I = ⊥.colon {x}
⊢ ∃ f, Function.Injective ⇑f

Tactic:
replace h : I = ker (toSpanSingleton R M x) := by simp [h, SetLike.ext_iff]

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x✝¹ : I.IsPrime
x✝ : ∃ x, I = ⊥.colon {x}
x : M
h : I = (toSpanSingleton R M x).ker
⊢ ∃ f, Function.Injective ⇑f
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
x : Kˣ
⊢ spanSingleton R⁰ (↑x)⁻¹ * spanSingleton R⁰ ↑x = 1

Tactic:
by
        simp only [spanSingleton_one, Units.inv_mul', spanSingleton_mul_spanSingleton]

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

Goal state before:
pp: case h
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, spanSingleton R⁰ ↑x = ↑((Units.mapEquiv (ringEquivOfRingEquiv K L f).symm.toMulEquiv) I)) ∧
    (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) ((Units.mapEquiv (ringEquivOfRingEquiv K L f).symm.toMulEquiv) I) = I

Tactic:
refine ⟨?_, by simp [← Units.val_inj]⟩

Goal state after:
case h
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, spanSingleton R⁰ ↑x = ↑((Units.mapEquiv (ringEquivOfRingEquiv K L f).symm.toMulEquiv) I)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous[inst✝¹, inst✝] f
s : Set Z
⊢ IsOpen[inst✝¹] (f ⁻¹' g ⁻¹' s)

Tactic:
exact hf.isOpen_preimage _ (hg _)

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₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
⊢ (if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = g ⟨x, hx⟩

Tactic:
split_ifs with h

Goal state after:
case pos
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∈ C₁
⊢ f ⟨x, h⟩ = g ⟨x, hx⟩

case neg
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∉ C₁
⊢ g ⟨x, ⋯⟩ = g ⟨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
p : PrimeSpectrum R
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)

Tactic:
let e : LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal]
      Localization.AtPrime p.asIdeal ⊗[R] M :=
    LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M
  rw [rankAtStalk, e.finrank_eq]

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
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ ⟦SemimoduleCat.of R M'⟧ * ⟦SemimoduleCat.of R (Dual R M')⟧ = 1

Tactic:
← toSkeleton,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (SemimoduleCat.of R M') * ⟦SemimoduleCat.of R (Dual R M')⟧ = 1
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (SemimoduleCat.of R M') * ⟦SemimoduleCat.of R (Dual R M')⟧ = 1

Tactic:
← toSkeleton,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (SemimoduleCat.of R M') * toSkeleton (SemimoduleCat.of R (Dual R M')) = 1
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
⊢ ↑(Units.mkOfMulEqOne ⟦SemimoduleCat.of R (Finite.reprₛ R (Dual R M))⟧
        ⟦SemimoduleCat.of R (Dual R (Finite.reprₛ R (Dual R M)))⟧ ⋯) =
    ↑((equivShrink (Skeleton (SemimoduleCat R))ˣ).symm.toFun (Pic.mk R M))⁻¹

Tactic:
rw [Pic.mk, Equiv.toFun_as_coe, Equiv.symm_apply_apply]
    exact Quotient.sound ⟨(Finite.reprEquivₛ R _ ≪≫ₗ (Finite.reprEquivₛ R _).dualMap).toModuleIsoₛ⟩

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
⊢ (EuclideanDomain.gcd (Polynomial.map ιEE' ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)))
      (Polynomial.map ιEE' (Polynomial.map ιFE g))).Splits

Tactic:
exact (SplittingField.splits _).of_dvd (map_ne_zero map_g_ne_zero)
      (EuclideanDomain.gcd_dvd_right _ _)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
⊢ Maximal M.Indep I

Tactic:
maximal_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J
⊢ M.Indep I ∧ ∀ ⦃t : Set α⦄, M.Indep t → I ⊆ t → I = t
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
⊢ M.IsBase B

Tactic:
by_contra hnb

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
⊢ False