mathlib-initiative/mathlib-tactics huggingface dataset:
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
ϕ : F →+* E
α β : E
f g : F[X]
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
by
  let sf := (f.map ϕ).roots
  let sg := (g.map ϕ).roots
  classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push Not at hc
  exact ⟨c, hc⟩

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
sf : Type (max 0 u) := (n : ℕ) × ModuleCon R (Fin n → R)
c₁ c₂ : sf
⊢ c₁ = c₂ → ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd ≃ₗ[R] ModuleCon.Quotient (Fin c₂.fst → R) c₂.snd

Tactic:
rintro rfl

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
sf : Type (max 0 u) := (n : ℕ) × ModuleCon R (Fin n → R)
c₁ : sf
⊢ ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd ≃ₗ[R] ModuleCon.Quotient (Fin c₁.fst → R) c₁.snd
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✝ : (Skeleton (SemimoduleCat R))ˣ
M N : Skeleton (SemimoduleCat R)
⊢ M = N → ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out N)

Tactic:
rintro rfl

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✝ : (Skeleton (SemimoduleCat R))ˣ
M : Skeleton (SemimoduleCat R)
⊢ ↑(Quotient.out M) ≃ₗ[R] ↑(Quotient.out M)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
hι : Nonempty ι
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨅ i, t i)
i : ι
⊢ (Polynomial.map (algebraMap F ↥(t i)) (minpoly F ((inclusion ⋯) x))).Splits

Tactic:
exact (h i).splits' (inclusion (iInf_le t i) x)

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

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

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
hD : M.Dep ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B B' : Set α
e : α
hB : M.IsBase B
hB' : M.IsBase B'
h : B \ B' = {e}
f : α
hf : f ∈ B' \ B
hb : M.IsBase (insert f (B \ {e}))
⊢ f ≠ e

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
B B' : Set α
hB : M.IsBase B
hB' : M.IsBase B'
f : α
hf : f ∈ B' \ B
h : B \ B' = {f}
hb : M.IsBase (insert f (B \ {f}))
⊢ False
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]
hzero : (aeval (α ^ n)) s = 0
h : α = 0
⊢ IsAlgebraic F α

Tactic:
exact h.symm ▸ isAlgebraic_zero

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
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
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hzero : ¬(aeval (α ^ n)) s = 0
hm : 0 < m
⊢ s ≠ 0

Tactic:
rintro rfl

Goal state after:
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 : F[X]
hm : 0 < m
h : α ^ m * (aeval (α ^ n)) 0 - (aeval (α ^ n)) r = 0
hzero : ¬(aeval (α ^ n)) 0 = 0
⊢ False
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
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
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
hn : 0 < n
hndvd : ¬n ∣ n * s.natDegree + m
⊢ s.leadingCoeff ≠ 0

Tactic:
exact leadingCoeff_ne_zero.2 hzero

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

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ f ≠ e

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
f : α
he : f ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {f})
hf : f ∈ B' \ (B \ {f})
hfB : M.Indep (insert f (B \ {f}))
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : 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'
⊢ I ≠ B'

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
hB' : M.IsBase I
hIB' : I ⊆ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
⊢ I ≠ B''ᶜ ∩ M.E

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X B : Set α
hB : M.IsBase B
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
B'' : Set α
hB'' : M.IsBase B''
hIE : B''ᶜ ∩ M.E ⊆ M.E
hIB : Disjoint (B''ᶜ ∩ M.E) B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) (B''ᶜ ∩ M.E)
hI : ¬M.IsBase (M.E \ (B''ᶜ ∩ M.E))
hB''₁ : B' \ (B''ᶜ ∩ M.E) ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ B''ᶜ ∩ M.E ⊆ B''ᶜ
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = J ∩ (M.E ∩ X)

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
M : Matroid α
I J X : Set α
hI : M.IsBasis' I X
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = J ∩ M.E ∩ X
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case h
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := ⋯
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X \ I ∧ insert e I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert e I) B

Tactic:
simp_rw [mem_sdiff, insert_subset_iff, and_iff_left heI, and_iff_right heE, and_iff_right hIE]

Goal state after:
case h
α : Type u_1
M✝ : Matroid α
I✝ B✝ X✝ : Set α
M : Matroid α
I X : Set α
hIE : I ⊆ M.E
B : Set α
hB : M.IsBase B
hIB : Disjoint I B
hI_not_max : ¬Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) I
hX_max : Maximal (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) X
hXE : X ⊆ M.E
B' : Set α := M.E \ X
hB' : M.IsBase B'
hX : B' = M.E \ X
hI : ¬M.IsBase (M.E \ I)
B'' : Set α
hB'' : M.IsBase B''
hB''₁ : B' \ I ⊆ B''
hB''₂ : B'' ⊆ B' ∪ B ∧ I ⊆ B''ᶜ
hssu : I ⊂ B''ᶜ ∩ M.E
e : α
heI : e ∉ I
heB'' : e ∉ B''
heE : e ∈ M.E
⊢ e ∈ X ∧ ∃ B, M.IsBase B ∧ Disjoint (insert e I) B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
E : Set α
hE : E.Finite
M : Matroid α
⊢ M ∈ {M | M.E = E} → M ∈ {M | M.E ⊆ E}

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
hE : M.E.Finite
⊢ M ∈ {M_1 | M_1.E ⊆ M.E}
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I : Set α
⊢ I = ∅ → I ⊆ E

Tactic:
rintro rfl

Goal state after:
α : Type u_1
E : Set α
⊢ ∅ ⊆ E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
⊢ M.E = E → ((∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅)

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
I : Set α
hIE : I ⊆ M.E
⊢ I = ∅ → M.Indep I

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ (X ∩ Jᶜ) ⊆ B'

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ X ∩ Jᶜ ⊆ B'
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X

Tactic:
simp_rw [isBase_iff_maximal_indep, IsBasis', maximal_iff, restrict_indep_iff]

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E → M.E = E ∧ M.Indep E

Tactic:
rintro rfl

Goal state after:
case refine_1
α : Type u_1
E : Set α
⊢ (freeOn E).E = E ∧ (freeOn E).Indep E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

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

Tactic:
rintro rfl

Goal state after:
α : Type u_1
N : Matroid α
h : N <r N
⊢ False
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : M✶.RankPos
hB : M.IsBase B
⊢ B ≠ M.E

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
h : M✶.RankPos
hB : M.IsBase M.E
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (M.map f hf).Indep (f '' B) ∧ ∀ ⦃t : Set β⦄, (M.map f hf).Indep t → f '' B ⊆ t → f '' B = t

Tactic:
refine ⟨hB.indep.map f hf, fun I hI hBI ↦ ?_⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
⊢ f '' B = I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
hBI : f '' B ⊆ I
I₀ : Set α
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ f '' B = I

Tactic:
← hbij.image_eq,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
I₀ : Set α
hBI : f '' B ⊆ f '' I₀
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ f '' B = I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
f : α
hfI : f ∈ I
⊢ e ≠ f

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∉ I
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
hfI : e ∈ I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
h : M.IsBasis I C
⊢ I ≠ C

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hC : M.IsCircuit I
h : M.IsBasis I I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ (M.mapEmbedding f).IsBase (⇑f '' B)

Tactic:
rw [Matroid.mapEmbedding, map_isBase_iff]
  exact ⟨B, hB, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
⊢ I = ∅ → M.IsBasis I X

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis ∅ X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hX : X ⊆ M.loops
⊢ M.IsBasis I X ↔ I = ∅

Tactic:
refine ⟨fun h ↦ ?_, by rintro rfl; simpa⟩
  have := (closure_eq_loops_of_subset hX) ▸ h.isBasis_closure_right
  simpa using this

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
⊢ I ≠ X

Tactic:
rintro rfl

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hX : M.Dep I
hI : M.IsBasis I I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z (J \ {z} ∪ ⋃ i, I i)
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i

Tactic:
← insert_union,

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
C' : Set α
hC'ss : C' ⊆ insert z (J \ {z}) ∪ ⋃ i, I i
hC' : M.IsCircuit C'
hzC' : z ∈ C'
⊢ C' ⊆ J ∪ ⋃ i, I i
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
e : α
I E : Set α
⊢ (uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E

Tactic:
by
  rw [← indep_singleton, uniqueBaseOn_indep_iff', singleton_subset_iff]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [hI.eRk_eq_encard, encard_eq_top_iff, ← hI.finite_iff_isRkFinite, Set.Infinite]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ (M.coloops ∩ K) = X ∩ K

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ M.coloops ∩ K = X ∩ K
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard

Tactic:
rw [← hB'.compl_isBase_of_dual.encard_eq_eRank, hI.eRk_eq_encard, hd.eRk_eq_encard,
    ← encard_union_eq (by tauto_set), ← encard_union_eq (by tauto_set)]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ (B ∩ X ∪ M.E \ B).encard = (M.E \ B ∩ (M.E \ X) ∪ X).encard
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
I J X : Set β
hI : (M.map f hf).IsBasis I X
hJ : (M.map f hf).IsBasis J X
⊢ #↑(I \ J) = #↑(J \ I)

Tactic:
obtain ⟨I, X, hIX, rfl, rfl⟩ := map_isBasis_iff'.1 hI

Goal state after:
α : Type u
β : Type v
f : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid α
inst✝ : M.InvariantCardinalRank
hf : InjOn f M.E
J : Set β
I X : Set α
hIX : M.IsBasis I X
hJ : (M.map f hf).IsBasis J (f '' X)
hI : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ #↑(f '' I \ J) = #↑(J \ f '' I)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i ↦ x ↑i) ↔ Disjoint s t

Tactic:
refine ⟨fun ind ↦ of_not_not fun ndisj ↦ ?_, adjoin_of_disjoint hx⟩

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i ↦ x ↑i
ndisj : ¬Disjoint s t
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
⊢ IsTranscendenceBasis R x

Tactic:
by convert! e.symm.isTranscendenceBasis hx; ext; simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g⁻¹ • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
rw [← fixedBy_inv, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_inv]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).RankFinite
⊢ IsTranscendenceBasis R x

Tactic:
exact .of_subtype_range hx.injective <| matroid_indep_iff.mpr hx.to_subtype_range
    |>.isBase_of_cRank_le <| lift_le.mp <| (matroid_cRank_eq R A ▸ le).trans_eq
      (mk_range_eq_of_injective hx.injective).symm

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{max w v, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s } = lift.{w, max v w} #({ x // x ∈ t } ⊕ { x // x ∈ s })

Tactic:
mk_sum,

Goal state after:
R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{max w v, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s } =
    lift.{w, max v w} (lift.{v, w} #{ x // x ∈ t } + lift.{w, v} #{ x // x ∈ s })
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finSepDegree F F = 1

Tactic:
finSepDegree_self

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ 1 = 1
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
h : (minpoly F x).natSepDegree = 1
halg : IsIntegral F x
⊢ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

Tactic:
exact (minpoly.irreducible halg).natSepDegree_eq_one_iff_of_monic' q
      (minpoly.monic halg) |>.1 h

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
⊢ ClosureOperator (IntermediateField F E)

Tactic:
refine .mk' (fun K ↦ (separableClosure K E).restrictScalars F) (fun K L le x hx ↦ ?_)
    le_restrictScalars_separableClosure fun K x hx ↦ ?_

Goal state after:
case refine_1
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K L : IntermediateField F E
le : K ≤ L
x : E
hx : x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) K
⊢ x ∈ (fun K ↦ IntermediateField.restrictScalars F (separableClosure (↥K) E)) L

case refine_2
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
K : IntermediateField F E
x : E
hx :
  x ∈
    IntermediateField.restrictScalars F
      (separableClosure (↥(IntermediateField.restrictScalars F (separableClosure (↥K) E))) E)
⊢ x ∈ IntermediateField.restrictScalars F (separableClosure (↥K) E)
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : Gal(L/K)
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑σ.symm) E
g : Gal(L/K)
hg : g ∈ F.fixingSubgroup.carrier
x : L
hx : x ∈ E
⊢ ↑↑σ.symm x = σ⁻¹ x

Tactic:
by dsimp

Goal state after: