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

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
obtain hj' | hj := (em (j ∈ s)).symm

Goal state after:
case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj' : j ∉ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj' : j ∉ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
·

Goal state after:
case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj' : j ∉ s
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

pp: case neg
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : ¬n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
f : F[X]
n : ℕ
h : n = 0
⊢ (n • f.aroots (AlgebraicClosure F)).toFinset.card = if n = 0 then 0 else (f.aroots (AlgebraicClosure F)).toFinset.card
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
⊢ v j ∈ (matroid R S).closure (v '' s \ v '' {j})

Tactic:
← inj.image_sdiff_subset (singleton_subset_iff.mpr hj)

Goal state after:
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
⊢ v j ∈ (matroid R S).closure (v '' (s \ {j}))
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
f g : F[X]
h : f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
this :
  ∀ (f g : F[X]),
    f = 0 ∨ g = 0 → f = 0 → ((f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g)
hf : ¬f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

pp: F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
·

Goal state after:
case pos.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : f = 0 ∨ g = 0
this :
  ∀ (f g : F[X]),
    f = 0 ∨ g = 0 → f = 0 → ((f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g)
hf : ¬f = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr.inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

pp: case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
·

Goal state after:
case inr.inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj✝ : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
x : ι
hxj : x ∉ {j}
hj : j ∈ insert x s
this : Nontrivial ↥(adjoin R (v '' (insert x s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert x s \ {j}))
hi : x ∉ s
eq : v x = v j
⊢ v ↑⟨x, ⋯⟩ = ((fun x ↦ v ↑x) ∘ ⇑((Equiv.image (Equiv.swap j x) s).trans (Equiv.setCongr ⋯)).symm) ⟨x, ⋯⟩

pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
x : ι
hxj : x ∉ {j}
hxi : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = ((fun x ↦ v ↑x) ∘ ⇑((Equiv.image (Equiv.swap j i) s).trans (Equiv.setCongr ⋯)).symm) ⟨x, ⋯⟩

Tactic:
·

Goal state after:
case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj✝ : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
x : ι
hxj : x ∉ {j}
hj : j ∈ insert x s
this : Nontrivial ↥(adjoin R (v '' (insert x s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert x s \ {j}))
hi : x ∉ s
eq : v x = v j
⊢ v ↑⟨x, ⋯⟩ = ((fun x ↦ v ↑x) ∘ ⇑((Equiv.image (Equiv.swap j x) s).trans (Equiv.setCongr ⋯)).symm) ⟨x, ⋯⟩
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g

pp: case refine_2
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g) → ∃ x, C x = g

Tactic:
·

Goal state after:
case refine_1
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
hx : x = 0
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g

pp: case neg
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
hx : ¬x = 0
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g

Tactic:
·

Goal state after:
case pos
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
hx : x = 0
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
x : ι
hxj : x ∉ {j}
hxi : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = ((fun x ↦ v ↑x) ∘ ⇑((Equiv.image (Equiv.swap j i) s).trans (Equiv.setCongr ⋯)).symm) ⟨x, ⋯⟩

Tactic:
·

Goal state after:
case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
x : ι
hxj : x ∉ {j}
hxi : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = ((fun x ↦ v ↑x) ∘ ⇑((Equiv.image (Equiv.swap j i) s).trans (Equiv.setCongr ⋯)).symm) ⟨x, ⋯⟩
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2.inl
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
⊢ ∃ x, C x = g

pp: case refine_2.inr
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x : F
h : C x = g
⊢ ∃ x, C x = g

Tactic:
·

Goal state after:
case refine_2.inl
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
h : g = 0
⊢ ∃ x, C x = g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj✝ : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
k : ι
hkj : k ∉ {j}
hj : j ∈ insert k s
this : Nontrivial ↥(adjoin R (v '' (insert k s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert k s \ {j}))
hi : k ∉ s
ne : v k ≠ v j
his : v k ∈ v '' s
⊢ v k ∈ v '' s \ {v j}

pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
k : ι
hkj : k ∉ {j}
hks : k ∈ s
⊢ v k ∈ v '' s \ {v j}

Tactic:
·

Goal state after:
case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial S
this✝¹ : IsDomain S
this✝ : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj✝ : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
k : ι
hkj : k ∉ {j}
hj : j ∈ insert k s
this : Nontrivial ↥(adjoin R (v '' (insert k s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert k s \ {j}))
hi : k ∉ s
ne : v k ≠ v j
his : v k ∈ v '' s
⊢ v k ∈ v '' s \ {v j}
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg.refine_1
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
⊢ False

pp: case neg.refine_2
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
⊢ f = 0 ∧ g = 0 ∨ IsCoprime f g →
    ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b

Tactic:
·

Goal state after:
case neg.refine_1
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
k : ι
hkj : k ∉ {j}
hks : k ∈ s
⊢ v k ∈ v '' s \ {v j}

Tactic:
·

Goal state after:
case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
his : v i ∈ v '' s
k : ι
hkj : k ∉ {j}
hks : k ∈ s
⊢ v k ∈ v '' s \ {v j}
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg.refine_1
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
H : ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b
u : F[X]
hu : Irreducible u
x✝¹ : u ∣ f
x✝ : u ∣ g
v : F[X]
hf : f = u * v
w : F[X]
hg : g = u * w
⊢ False

Tactic:
obtain ⟨x, hx⟩ := IsAlgClosed.exists_aeval_eq_zero
      (AlgebraicClosure F) _ (degree_pos_of_irreducible hu).ne'
    exact H x ⟨h.1, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hf)⟩
      x ⟨h.2, by simpa only [map_mul, hx, zero_mul] using congr(aeval x $hg)⟩ rfl

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg.refine_2.inl
F : Type u
inst✝ : Field F
h : ¬0 = 0 ∧ ¬0 = 0
⊢ ∀ (a : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval a) 0 = 0 → ∀ (b : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval b) 0 = 0 → a ≠ b

pp: case neg.refine_2.inr
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f = 0 ∧ ¬g = 0
hc : IsCoprime f g
⊢ ∀ (a : AlgebraicClosure F), f ≠ 0 ∧ (aeval a) f = 0 → ∀ (b : AlgebraicClosure F), g ≠ 0 ∧ (aeval b) g = 0 → a ≠ b

Tactic:
·

Goal state after:
case neg.refine_2.inl
F : Type u
inst✝ : Field F
h : ¬0 = 0 ∧ ¬0 = 0
⊢ ∀ (a : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval a) 0 = 0 → ∀ (b : AlgebraicClosure F), 0 ≠ 0 ∧ (aeval b) 0 = 0 → a ≠ b
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case zero
F : Type u
inst✝¹ : Field F
f : F[X]
n : ℕ
inst✝ : CharZero F
⊢ ((expand F (1 ^ n)) f).natSepDegree = f.natSepDegree

pp: case prime
F : Type u
inst✝ : Field F
f : F[X]
q n : ℕ
hprime : Nat.Prime q
hchar✝ : CharP F q
⊢ ((expand F (q ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
·

Goal state after:
case zero
F : Type u
inst✝¹ : Field F
f : F[X]
n : ℕ
inst✝ : CharZero F
⊢ ((expand F (1 ^ n)) f).natSepDegree = f.natSepDegree
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
j : ι
v : ι → S
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
·

Goal state after:
case inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
j : ι
v : ι → S
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
⊢ ∃ n y, f = (expand F (q ^ n)) (X - C y)

pp: case refine_2
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
x✝ : ∃ n y, f = (expand F (q ^ n)) (X - C y)
n : ℕ
y : F
h : f = (expand F (q ^ n)) (X - C y)
⊢ f.natSepDegree = 1

Tactic:
·

Goal state after:
case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
⊢ ∃ n y, f = (expand F (q ^ n)) (X - C y)
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G), ∀ i ∈ B.toFilterBasis, a ∈ (fun y ↦ a * y) '' id i

pp: case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ B.toFilterBasis,
      ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id i ∈ map (fun y ↦ x * y) B.filter

Tactic:
·

Goal state after:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G), ∀ i ∈ B.toFilterBasis, a ∈ (fun y ↦ a * y) '' id i
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ B.toFilterBasis,
      ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id i ∈ map (fun y ↦ x * y) B.filter

Tactic:
·

Goal state after:
case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ B.toFilterBasis,
      ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id i ∈ map (fun y ↦ x * y) B.filter