mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : (B₁ \ insert f (B₂ \ {e})).encard ≤ (insert f (B₂ \ {e}) \ B₁).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
rw [insert_sdiff_of_mem _ hf.1, sdiff_sdiff_comm, ← union_singleton, ← sdiff_sdiff,
    sdiff_sdiff_right, inter_singleton_eq_empty.mpr he.2, union_empty] at hencard

Goal state after:
case inr.inr
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
e : α
he : e ∈ B₂ \ B₁
hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard
f : α
hf : f ∈ B₁ \ B₂
hB' : IsBase (insert f (B₂ \ {e}))
this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard
hencard : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
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] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : 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 := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ EuclideanDomain.gcd
      (Polynomial.map (algebraMap (↥F⟮γ⟯) E)
        ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)))
      (Polynomial.map (algebraMap (↥F⟮γ⟯) E) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)) =
    h

Tactic:
·

Goal state after:
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] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : 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 := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ EuclideanDomain.gcd
      (Polynomial.map (algebraMap (↥F⟮γ⟯) E)
        ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X)))
      (Polynomial.map (algebraMap (↥F⟮γ⟯) E) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)) =
    h
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B.Nonempty

Tactic:
nonempty_iff_ne_empty

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
inst✝ : M.RankPos
hB : M.IsBase B
⊢ B ≠ ∅
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ ≤ F⟮α + x • β⟯

pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯

Tactic:
·

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ ≤ F⟮α + x • β⟯
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ I ⊆ B

pp: case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
⊢ M.IsBase (M.E \ B)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ I ⊆ B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ B
⊢ I ⊆ B

pp: case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : Disjoint I B'
⊢ B' ⊆ M.E \ B

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
h : M.IsBase (M.E \ B)
I : Set α
hI : I ⊆ M.E
B' : Set α
x✝ : M.IsBase B' ∧ Disjoint I B'
hBI : B ⊆ I
hB' : M.IsBase B'
hIB' : I ⊆ M.Eᶜ ∪ B
⊢ I ⊆ B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
⊢ M.IsBase (M.E \ (M.E \ B'))

pp: case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
⊢ B ⊆ M.E \ B'

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
x✝ :
  (∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
    ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
B' : Set α
hB' : M.IsBase B'
hBB' : Disjoint B B'
h : ∀ ⦃y : Set α⦄, y ⊆ M.E → ∀ (x : Set α), M.IsBase x ∧ Disjoint y x → B ⊆ y → B = y
⊢ M.IsBase (M.E \ (M.E \ B'))
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯

Tactic:
·

Goal state after:
case a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α + x • β⟯ ≤ F⟮α, β⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
⊢ ∃ α, F⟮α⟯ = ⊤

pp: case inr
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_finite : Fintype F
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
·

Goal state after:
case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_inf : IsEmpty (Fintype F)
⊢ ∃ α, F⟮α⟯ = ⊤
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D.Nonempty

Tactic:
nonempty_iff_ne_empty

Goal state after:
α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D ≠ ∅
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✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_finite : Fintype F
⊢ ∃ α, F⟮α⟯ = ⊤

Tactic:
·

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : Algebra.IsSeparable F E
F_finite : Fintype F
⊢ ∃ α, F⟮α⟯ = ⊤
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
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
this :
  ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} {m n : ℕ},
    m ≠ n → F⟮α ^ m⟯ = F⟮α ^ n⟯ → m < n → IsAlgebraic F α
hmn : ¬m < n
⊢ IsAlgebraic F α

pp: F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
⊢ IsAlgebraic F α

Tactic:
·

Goal state after:
case inr
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
this :
  ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {α : E} {m n : ℕ},
    m ≠ n → F⟮α ^ m⟯ = F⟮α ^ n⟯ → m < n → IsAlgebraic F α
hmn : ¬m < n
⊢ IsAlgebraic F α
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : m = 0
⊢ IsAlgebraic F α

pp: case neg
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
⊢ IsAlgebraic F α

Tactic:
·

Goal state after:
case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : m = 0
⊢ IsAlgebraic F α
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s
hzero : (aeval (α ^ n)) s = 0
⊢ IsAlgebraic F α

pp: case neg
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s
hzero : ¬(aeval (α ^ n)) s = 0
⊢ IsAlgebraic F α

Tactic:
·

Goal state after:
case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : ¬m = 0
r s : F[X]
h : α ^ m = (aeval (α ^ n)) r / (aeval (α ^ n)) s
hzero : (aeval (α ^ n)) s = 0
⊢ IsAlgebraic F α
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))

pp: case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = {e}
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hcard : (B' \ B).encard = (B \ B').encard
hfB : f ∈ B'
h : B \ B' = ∅
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case neg.refine_1
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ f ≠ 0

pp: case neg.refine_2
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ (aeval α) f = 0

Tactic:
·

Goal state after:
case neg.refine_1
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ f ≠ 0
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.IsBase (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.IsBase (insert e I)

pp: case inr
α : Type u_1
M : Matroid α
I : Set α
e f : α
he : e ∉ I
hf : f ∉ I
heI : M.IsBase (insert e I)
hfI : M.Indep (insert f I)
hef : e ≠ f
⊢ M.IsBase (insert f I)

Tactic:
·

Goal state after:
case inl
α : Type u_1
M : Matroid α
I : Set α
e : α
he : e ∉ I
heI : M.IsBase (insert e I)
hf : e ∉ I
hfI : M.Indep (insert e I)
⊢ M.IsBase (insert e I)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case pos
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∈ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

pp: case neg
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∉ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
x : α
hxB' : x ∈ B'
hx : x ∉ I
hxB : x ∈ B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp
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)ˣ
h : I ∈ (unitsToPic R A).ker
⊢ I ∈ (Units.map ↑(spanSingleton R)).range

pp: case mpr
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)ˣ
h : I ∈ (Units.map ↑(spanSingleton R)).range
⊢ I ∈ (unitsToPic R A).ker

Tactic:
·

Goal state after:
case mp
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)ˣ
h : I ∈ (unitsToPic R A).ker
⊢ I ∈ (Units.map ↑(spanSingleton R)).range
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
⊢ False

pp: case refine_2
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ M.IsBase B

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
⊢ False
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp.refine_1
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)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ ∃ b, (↑e 1).1 * b = 1

pp: case mp.refine_2
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)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ ∃ c, c * (↑e 1).1 = 1

Tactic:
·

Goal state after:
case mp.refine_1
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)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
⊢ ∃ b, (↑e 1).1 * b = 1
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case neg.refine_2
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ (aeval α) f = 0

Tactic:
·

Goal state after:
case neg.refine_2
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ (aeval α) f = 0
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: case inl
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f x ⊆ f y
⊢ y ∈ f x

pp: case inr
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f y ⊆ f x
⊢ y ∈ f x

Tactic:
·

Goal state after:
case inl
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f x ⊆ f y
⊢ y ∈ f x
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case pos
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

pp: case neg
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
·

Goal state after:
case pos
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: case inr
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f y ⊆ f x
⊢ y ∈ f x

Tactic:
·

Goal state after:
case inr
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
X : Set α
x✝¹ : X ⊆ E
I : Set α
hI : Indep I
hIX : I ⊆ X
Is : Set (Set α)
hIs : Is ⊆ {Y | Indep Y ∧ Y ⊆ X}
hchain : IsChain (fun x1 x2 ↦ x1 ⊆ x2) Is
x✝ : Is.Nonempty
J : Set α
hJ : J ⊆ ⋃₀ Is
hJfin : J.Finite
f : α → Set α
hf : ∀ e ∈ J, f e ∈ Is ∧ e ∈ f e
hne : J.Nonempty
x : α
hxJ : x ∈ J
hxmax : ∀ ⦃j : α⦄, (fun x ↦ x ∈ J) j → f x ⊆ f j → f j ⊆ f x
y : α
hyJ : y ∈ J
hle : f y ⊆ f x
⊢ y ∈ f x
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
⊢ M₂.Indep I

pp: case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
⊢ M₁.Indep I

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
⊢ M₂.Indep I