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

Goal state before:
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'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase ({f} ∪ B \ (B \ B'))

Tactic:
← hx,

Goal state after:
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'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase (B' \ B ∪ B \ (B \ B'))
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)

Tactic:
exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩

Goal state after:
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:
· obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
    exact (hM₁ hB).subset hIB

Goal state after:
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
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis' I X ↔ M.IsBasis I X

Tactic:
isBasis'_iff_isBasis_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : X ⊆ M.E
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ M.IsBasis I (⋃₀ Xs)

Tactic:
by
  rw [sUnion_eq_iUnion]
  have := Iff.mpr nonempty_coe_sort hne
  exact IsBasis.isBasis_iUnion _ fun X ↦ h X X.prop

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
e : α
he : e ∈ {x | M.IsBasis I (insert x I)} \ I
hu : M.Indep (insert e I)
⊢ e ∈ I

Tactic:
simpa using (hu.eq_of_isBasis he.1).symm

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

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

Tactic:
by
  convert! hJ.isBasis_self.union_isBasis_union hI _ <;>
  rw [union_eq_self_of_subset_right hIJ]
  assumption

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ⊆ B' ∪ R ∩ M.E

Tactic:
union_comm

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M✶.IsBasis (M.E \ (B' ∪ R ∩ M.E)) (M.E \ (R ∩ M.E))
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ B ⊆ R ∩ M.E ∪ B'
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis' I X ↔ I = X ∩ E

Tactic:
isBasis'_iff_isBasis_inter_ground,

Goal state after:
α : Type u_1
E I X : Set α
⊢ (freeOn E).IsBasis I (X ∩ (freeOn E).E) ↔ I = X ∩ E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ I = X ∩ E ∧ X ∩ E ⊆ E ↔ I = X ∩ E

Tactic:
and_iff_left inter_subset_right

Goal state after:
α : Type u_1
E I X : Set α
⊢ I = X ∩ E ↔ I = X ∩ E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ

Tactic:
isBasis'_iff_isBasis_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ univ
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBasis I X
⊢ M.IsBasis I X

Tactic:
exact ((isBasis_restrict_iff hR).1 hI).1

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B

Tactic:
simp_rw [coindep_iff_exists', subset_sdiff]
  exact ⟨fun ⟨⟨B, hB, _, hBX⟩, hX⟩ ↦ ⟨B, hB, hX, hBX.symm⟩,
    fun ⟨B, hB, hXE, hXB⟩ ↦ ⟨⟨B, hB, hB.subset_ground, hXB.symm⟩, hXE⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B → B ⊆ E → (N.IsBasis' (f '' B) (f '' E) ↔ N.IsBase (f '' B))

Tactic:
isBasis'_iff_isBasis_inter_ground,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ InjOn f B → B ⊆ E → (N.IsBasis (f '' B) (f '' E ∩ N.E) ↔ N.IsBase (f '' B))
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
h : M.IsRkFinite (X ∩ M.E)
⊢ M.IsRkFinite (M.closure X)

Tactic:
by simpa using h.closure

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X

Tactic:
rw [← isRkFinite_inter_ground_iff (X := X)]
  exact ⟨fun h ↦ h.subset <| M.inter_ground_subset_closure X, fun h ↦ by simpa using h.closure⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
⊢ ∃ B₀, M.IsBase B₀ ∧ B = f '' B₀

Tactic:
obtain ⟨B₀, hB₀, hbij⟩ := h.prop.exists_bijOn_of_map

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
⊢ ∃ B₀, M.IsBase B₀ ∧ B = f '' B₀
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (M.fundCircuit e I)

Tactic:
fundCircuit_eq_sInter hecl

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ M.IsCircuit (insert e (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}))
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis' I X
⊢ I.encard = M.eRk (X ∩ R)

Tactic:
isBasis'_iff_isBasis_inter_ground,

Goal state after:
α : Type u_1
M : Matroid α
R X I : Set α
hI : (M ↾ R).IsBasis I (X ∩ (M ↾ R).E)
⊢ I.encard = M.eRk (X ∩ R)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : 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 ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ J \ {z} ∪ range x \ {z} ⊆ range x ∪ J \ {z}

Tactic:
union_comm

Goal state after:
case inr
α : 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 ι
hC' : ∀ (i : ι), M.closure (I i) = M.closure (insert (x i) (I i))
⊢ range x \ {z} ∪ J \ {z} ⊆ range x ∪ J \ {z}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
x✝ : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.closure {e}
⊢ M.eRk {e} ≤ {e}.encard

Tactic:
(Tactic.exact
 "exact"
 (Term.app
  `M.eRk_le_encard
  [(choice
    («term{_}» "{" [`e] "}")
    (Term.structInst
     "{"
     []
     (Term.structInstFields [(Term.structInstField (Term.structInstLVal `e []) [])])
     (Term.optEllipsis [])
     []
     "}"))]))

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain rfl | hne := eq_or_ne f e

Goal state after:
case inl
α : Type u_2
M : Matroid α
f : α
B : Set α
hB : M.IsBase B
hfE : f ∈ M.E
he : f ∈ B
hf : f ∉ M.closure (B \ {f})
⊢ M.IsBase (insert f (B \ {f}))

case inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
hne : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.removeLoops.IsNonloop = M.IsNonloop

Tactic:
ext e

Goal state after:
α : Type u_1
M : Matroid α
e : α
⊢ M.removeLoops.IsNonloop e ↔ M.IsNonloop e
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B

pp: case inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
⊢ f ∈ M.fundCircuit e B

Tactic:
· rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he
    contradiction

Goal state after:
case inr.inr
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
⊢ f ∈ M.fundCircuit e B
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) = M.closure I

Tactic:
by
  apply subset_antisymm <;> apply closure_subset_closure_of_subset_closure
  · simp only [subset_def, mem_sdiff, mem_insert_iff, mem_singleton_iff]
    rintro a (rfl | haI)
    exacts [hf, M.subset_closure _ hI.subset_ground haI]
  · intro a haI
    obtain rfl | ne := eq_or_ne a e
    exacts [he, M.mem_closure_of_mem' ⟨.inr haI, ne⟩ (hI.subset_ground haI)]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ e ∈ (J ∪ I) \ I

Tactic:
union_comm

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
h : ∀ e ∈ J \ I, e ∉ M.closure (I ∪ J \ {e})
K : Set α
hKIJ : M.IsBasis K (I ∪ J)
hK : I ⊆ K
hssu : K ⊂ I ∪ J
e : α
heI : e ∈ I ∪ J
heK : e ∉ K
⊢ e ∈ (I ∪ J) \ I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ (∀ e ∈ I \ J, e ∉ M.closure (J ∪ I \ {e})) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
union_comm

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

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0

Tactic:
have : (g : A →+* B) _ = _ := congr(g $hp)

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : ↑g ((aeval x) p) = g 0
⊢ (aeval (⇑g ∘ x)) ((MvPolynomial.map ↑f) p) = 0
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E

Tactic:
ext e

Goal state after:
α : Type u_2
M : Matroid α
X R I : Set α
hI : (M ↾ R).IsBasis' I X
hI' : M.IsBasis' I (X ∩ R)
hIR : I ⊆ R
e : α
⊢ e ∈ (M ↾ R).closure X ↔ e ∈ M.closure (X ∩ R) ∩ R ∪ R \ M.E
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
r : R
⊢ (Polynomial.aeval a) (Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)) = (algebraMap R A) r

Tactic:
Polynomial.aeval_C,

Goal state after:
case refine_1
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
r : R
⊢ (algebraMap (↥(adjoin R (range x))) A) ((algebraMap R ↥(adjoin R (range x))) r) = (algebraMap R A) r
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (Polynomial.aeval a) (Polynomial.C (hx.aevalEquiv (X i))) = (aeval fun o ↦ o.elim a x) (X (some i))

Tactic:
Polynomial.aeval_C,

Goal state after:
case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (algebraMap (↥(adjoin R (range x))) A) (hx.aevalEquiv (X i)) = (aeval fun o ↦ o.elim a x) (X (some i))
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rt) (↥St) A
this✝¹ : NoZeroDivisors ↥St
this✝ : NoZeroDivisors ↥Rt
this : Algebra.IsAlgebraic ↥Rt ↥St
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)

Tactic:
change Transcendental St (x i)

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝² : IsScalarTower (↥Rt) (↥St) A
this✝¹ : NoZeroDivisors ↥St
this✝ : NoZeroDivisors ↥Rt
this : Algebra.IsAlgebraic ↥Rt ↥St
⊢ Transcendental (↥St) (x i)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
x : F
n : ℕ
⊢ ((X - C x) ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
by
  simp only [natSepDegree_pow, natSepDegree_X_sub_C]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case prime
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
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
⊢ False

Tactic:
have := expChar_of_injective_ringHom (R := F) C_injective q

Goal state after:
case prime
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
hf : f = X ^ q ^ n - C y
hq : Nat.Prime q
hchar✝ : CharP F q
hn : ¬n = 0
x✝ : y ∈ (frobenius F q).range
z : F
hy : (frobenius F q) z = y
this : ExpChar F[X] q
⊢ False
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
U : Set G
U_in : U ∈ B
⊢ ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id U

Tactic:
simpa using! inv U_in

Goal state after:
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
e : E
⊢ e ∈ F⟮α⟯

Tactic:
rw [hα]; exact IntermediateField.mem_top

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ finInsepDegree F F = 1

Tactic:
rw [finInsepDegree_def', insepDegree_self, Cardinal.one_toNat]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : SeparatelyContinuousMul G
H : Subgroup G
inst✝ : H.FiniteIndex
h : IsClosed ↑H
⊢ IsOpen ↑H

Tactic:
rw [← QuotientGroup.t1Space_iff] at h
  rw [← QuotientGroup.discreteTopology_iff]
  infer_instance

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h✝ : ExpChar F p
x y : F
hy : y ^ p - eval y (C x) = 0
⊢ (frobenius F p) y = x

Tactic:
eval_C,

Goal state after:
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h✝ : ExpChar F p
x y : F
hy : y ^ p - x = 0
⊢ (frobenius F p) y = x
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case mpr
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
h : ∀ x ∈ L, ((restrictNormalHom E) f) x = x
x : E
hx : x ∈ ↑L.toSubsemiring
⊢ f (↑(IsScalarTower.toAlgHom F E E') x) = ↑(IsScalarTower.toAlgHom F E E') x

Tactic:
replace h := congr(algebraMap E E' $(show f.restrictNormal E x = x from h x hx))

Goal state after:
case mpr
F : Type u_1
E : Type u_2
E' : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field E'
inst✝⁴ : Algebra F E
inst✝³ : Algebra F E'
inst✝² : Algebra E E'
inst✝¹ : IsScalarTower F E E'
L : IntermediateField F E
inst✝ : Normal F E
f : Gal(E'/F)
x : E
hx : x ∈ ↑L.toSubsemiring
h : (algebraMap E E') ((f.restrictNormal E) x) = (algebraMap E E') x
⊢ f (↑(IsScalarTower.toAlgHom F E E') x) = ↑(IsScalarTower.toAlgHom F E E') x
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
⊢ g ∈ lifts (algebraMap (↥(integralClosure R K)) K)

Tactic:
have := (SplittingField.splits g).mem_lift_of_roots_mem_range (hg.map _)
    (algebraMap (integralClosure R g.SplittingField) g.SplittingField)
     fun a ha =>
      (SetLike.ext_iff.mp (integralClosure R g.SplittingField).range_algebraMap _).mpr <|
        roots_mem_integralClosure hf ?_

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
this :
  map (algebraMap K g.SplittingField) g ∈ lifts (algebraMap (↥(integralClosure R g.SplittingField)) g.SplittingField)
⊢ g ∈ lifts (algebraMap (↥(integralClosure R K)) K)

case refine_1
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
f : R[X]
hf : f.Monic
g : K[X]
hg : g.Monic
hd : g ∣ map (algebraMap R K) f
a : g.SplittingField
ha : a ∈ (map (algebraMap K g.SplittingField) g).roots
⊢ a ∈ f.aroots g.SplittingField
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : Field S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
B : BilinForm S M
inst✝¹ : IsDomain R
hB : B.Nondegenerate
inst✝ : IsTorsionFree R S
N : Submodule R M
hN : Submodule.span S ↑N = ⊤
x y : ↥(B.dualSubmodule N)
e : (B.dualSubmoduleToDual N) x = (B.dualSubmoduleToDual N) y
z : M
hz : z ∈ ↑N
⊢ (B ↑x) z = (B ↑y) z

Tactic:
simpa using congr_arg (algebraMap R S) (LinearMap.congr_fun e ⟨z, hz⟩)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
use g'

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
g' : R[X]
hg' : map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
⊢ map (algebraMap R K) g' * C g.leadingCoeff = g
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : C ↑u = map φ f
hdeg : (C ↑u).degree = 0
⊢ IsUnit f

Tactic:
rw [hu, degree_map_eq_of_injective hinj] at hdeg

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : C ↑u = map φ f
hdeg : f.degree = 0
⊢ IsUnit f
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
⊢ IsIntegrallyClosed R → ∀ (p : R[X]), p.Monic → (Irreducible p ↔ Irreducible (map (algebraMap R K) p))

Tactic:
intro hR p hp; exact Monic.irreducible_iff_irreducible_map_fraction_map hp

Goal state after: