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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C

Tactic:
obtain ⟨C, hCs, hC, hfC⟩ := hC₁.strong_multi_elimination (fun i : Unit ↦ e) (fun _ ↦ C₂) f
    (by simpa) (by simpa) (by simpa) (by simp) (by simpa) (by simpa)

Goal state after:
α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
C : Set α
hCs : C ⊆ (C₁ ∪ ⋃ i, C₂) \ range fun i ↦ e
hC : M.IsCircuit C
hfC : f ∈ C
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C ∧ f ∈ C
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X Y : Set α
⊢ (M ↾ X).cRk (Y ∩ (M ↾ X).E) = M.cRk (X ∩ Y)

Tactic:
restrict_ground_eq,

Goal state after:
α : Type u
M : Matroid α
X Y : Set α
⊢ (M ↾ X).cRk (Y ∩ X) = M.cRk (X ∩ Y)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
⊢ C.Finite

Tactic:
by
  have hi := hC.dep.not_indep
  rw [indep_iff_forall_finite_subset_indep] at hi; push Not at hi
  obtain ⟨J, hJC, hJfin, hJ⟩ := hi
  rwa [← hC.eq_of_not_indep_subset hJ hJC]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ M✶.IsCocircuit C

Tactic:
by
  rwa [isCocircuit_def, dual_dual]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ B).Nonempty

Tactic:
exact hX B hB

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

Goal state before:
pp: α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton
⊢ (∃ e ∈ M.E, M.IsLoop e) ↔ ∃ C, M.IsCircuit C ∧ C.Subsingleton

Tactic:
exact this

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
let g := (Algebra.botEquivOfInjective (MvPolynomial.C_injective σ R)).symm.trans
    (Subalgebra.equivOfEq _ _ supported_empty).symm

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ Transcendental R ((Polynomial.aeval (X i)) f)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ {e} ∧ e ∈ M.fundCocircuit e B ∧ {e} ⊆ I

Tactic:
and_iff_right
    (mem_fundCocircuit _ _ _),

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ {e} ∧ {e} ⊆ I
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'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x))
this : aeval (⇑f ∘ x) = f.comp (aeval x)
⊢ ∀ (p : MvPolynomial ι R), (aeval x) p ∈ (aeval Subtype.val).range

Tactic:
intro p

Goal state after:
ι : 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'
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hf_inj : InjOn ⇑f ↑(adjoin R (range x))
this : aeval (⇑f ∘ x) = f.comp (aeval x)
p : MvPolynomial ι R
⊢ (aeval x) p ∈ (aeval Subtype.val).range
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ M.IsRkFinite X ↔ M.cRk X < ℵ₀

Tactic:
IsRkFinite,

Goal state after:
α : Type u
M : Matroid α
X : Set α
⊢ (M ↾ X).RankFinite ↔ M.cRk X < ℵ₀
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
⊢ e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B

Tactic:
by
  -- By symmetry and duality, it suffices to show the implication in one direction.
  suffices aux : ∀ {N : Matroid α} {B' : Set α} (hB' : N.IsBase B') {e f},
      e ∈ N.fundCocircuit f B' → f ∈ N.fundCircuit e B' from
    ⟨fun h ↦ aux hB h, fun h ↦ aux hB.compl_isBase_dual <| by
      simpa [fundCocircuit, inter_eq_self_of_subset_right hB.subset_ground]⟩
  clear! B M e f
  intro M B hB e f he
  -- discharge the various degenerate cases.
  obtain rfl | hne := eq_or_ne e f
  · simp [mem_fundCircuit]
  have hB' : M✶.IsBase (M✶.E \ B) := hB.compl_isBase_dual
  obtain hfE | hfE := em' <| f ∈ M.E
  · rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he
    contradiction
  obtain hfB | hfB := em' <| f ∈ B
  · rw [fundCocircuit, fundCircuit_eq_of_mem (by simp [hfE, hfB])] at he
    contradiction
  obtain ⟨heE, heB⟩ : e ∈ M.E \ B := by
    simpa [hne] using (M.fundCocircuit_subset_insert_compl f B) he
  -- Use basis exchange to argue the equivalence.
  rw [fundCocircuit, hB'.indep.mem_fundCircuit_iff (by rwa [hB'.closure_eq]) (by simp [hfB])] at he
  rw [hB.indep.mem_fundCircuit_iff (by rwa [hB.closure_eq]) heB]
  have hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e})) :=
    (hB'.exchange_isBase_of_indep' ⟨heE, heB⟩ (by simp [hfE, hfB]) he).compl_isBase_of_dual
  refine hB'.indep.subset ?_
  simp only [dual_ground, sdiff_singleton_subset_iff]
  rw [sdiff_sdiff_right, inter_eq_self_of_subset_right (by simpa), union_singleton, insert_comm,
    ← union_singleton (s := M.E \ B), ← sdiff_sdiff, sdiff_sdiff_cancel_left hB.subset_ground]
  simp [hfB]

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
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0

Tactic:
intro p

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : ∀ (p : MvPolynomial ι R), (aeval x) p = 0 → p = 0
f : ι → MvPolynomial ι R
hf : ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
p : MvPolynomial ι R
⊢ (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
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
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0

Tactic:
intro p

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
p : MvPolynomial ι R
⊢ (aeval f) p = 0 → p = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
hinj : Injective ⇑(algebraMap R A)
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val → ∀ a ∈ s, a ∉ t → Transcendental (↥(adjoin R t)) a
t : Set { x // x ∈ s }
hfin : t.Finite
h : AlgebraicIndependent R fun i ↦ ↑↑i
i : { x // x ∈ s }
hi : i ∉ t
⊢ Subtype.val '' t ⊆ s

Tactic:
rintro _ ⟨x, _, rfl⟩

Goal state after:
R : Type u_3
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
hinj : Injective ⇑(algebraMap R A)
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val → ∀ a ∈ s, a ∉ t → Transcendental (↥(adjoin R t)) a
t : Set { x // x ∈ s }
hfin : t.Finite
h : AlgebraicIndependent R fun i ↦ ↑↑i
i : { x // x ∈ s }
hi : i ∉ t
x : { x // x ∈ s }
left✝ : x ∈ t
⊢ ↑x ∈ s
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), (aeval x) p = 0 → p = 0

Tactic:
intro p

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
⊢ (aeval x) p = 0 → p = 0
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
s : Set ι
i : ι
hi : i ∉ s
⊢ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
convert! ← hx.adjoin_of_disjoint (Set.disjoint_singleton_right.mpr hi)
  rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

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 ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0

Tactic:
intro p

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 ι R), (aeval x) p = 0 → p = 0
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι S
⊢ (aeval (⇑g ∘ x)) p = 0 → p = 0
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
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent R fun i ↦ (Polynomial.aeval (x i)) (f i)

Tactic:
convert! aeval_of_algebraicIndependent hx (algebraicIndependent_polynomial_aeval_X _ hf)
  rw [← AlgHom.comp_apply]
  congr 1; ext1; simp

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) → ↑s := fun x ↦ ⟨↑x, ⋯⟩
x : A
hx✝ : x ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ s) t
hx : ∃ a ∈ t, (Embedding.subtype fun x ↦ x ∈ s) a = x
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ s) t
hy : ∃ a ∈ t, (Embedding.subtype fun x ↦ x ∈ s) a = y
⊢ f ⟨x, hx✝⟩ = f ⟨y, hy✝⟩ → ⟨x, hx✝⟩ = ⟨y, hy✝⟩

Tactic:
obtain ⟨a, _, rfl⟩ := hx

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) → ↑s := fun x ↦ ⟨↑x, ⋯⟩
y : A
hy✝ : y ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ s) t
hy : ∃ a ∈ t, (Embedding.subtype fun x ↦ x ∈ s) a = y
a : { x // x ∈ s }
left✝ : a ∈ t
hx : (Embedding.subtype fun x ↦ x ∈ s) a ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ s) t
⊢ f ⟨(Embedding.subtype fun x ↦ x ∈ s) a, hx⟩ = f ⟨y, hy✝⟩ → ⟨(Embedding.subtype fun x ↦ x ∈ s) a, hx⟩ = ⟨y, hy✝⟩
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
e : α
⊢ e ∈ (M ↾ R).E ∧ ((M ↾ R).Indep (insert e I) → e ∈ I) ↔
    (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R \ M.E

Tactic:
restrict_ground_eq,

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 ∈ R ∧ ((M ↾ R).Indep (insert e I) → e ∈ I) ↔ (e ∈ M.E ∧ (M.Indep (insert e I) → e ∈ I)) ∧ e ∈ R ∨ e ∈ R \ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).closure S = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ⊆ M.closure S

Tactic:
restrict_ground_eq,

Goal state after:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).closure S = R ∧ S ⊆ R ↔ R ⊆ M.closure S
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
⊢ M.closure (S ∩ R) ∩ R ∪ R \ M.E = (M ↾ R).E ∧ S ⊆ (M ↾ R).E ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R

Tactic:
restrict_ground_eq,

Goal state after:
α : Type u_2
M : Matroid α
R S : Set α
⊢ M.closure (S ∩ R) ∩ R ∪ R \ M.E = R ∧ S ⊆ R ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case mpr
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
⊢ (∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x

Tactic:
intro p

Goal state after:
case mpr
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ IsTranscendenceBasis R x
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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
⊢ Algebra.IsAlgebraic S A

Tactic:
have : Algebra.IsAlgebraic S Sv := by
    simpa [Sv, ← Subalgebra.isAlgebraic_iff, isAlgebraic_adjoin_iff]

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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic S ↥Sv
⊢ Algebra.IsAlgebraic S A
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✝¹ : IsDomain S
inst✝ : NoZeroDivisors A
ι : Type u_2
v : ι → A
hv : IsTranscendenceBasis R v
H : ∀ (i : ι), IsAlgebraic S (v i)
Rv : Subalgebra R A := adjoin R (range v)
Sv : Subalgebra S A := adjoin S (range v)
this : Algebra.IsAlgebraic S ↥Sv
⊢ Rv ≤ (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R (range v)

Tactic:
exact le_sup_right

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun x ↦ X - C x) f.roots).prod
h2 : (Polynomial.map (RingHom.id F) f).roots.toFinset.card = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
map_id,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun x ↦ X - C x) f.roots).prod
h2 : f.roots.toFinset.card = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
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
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y

Tactic:
| prime hq =>

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 v
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Module.Finite F K
this✝ : Algebra ↥(separableClosure F K) ↥(restrictScalars F (separableClosure E K)) := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥(separableClosure F K)) (↥(restrictScalars F (separableClosure E K))) K
⊢ finInsepDegree E K ≤ finInsepDegree F K

Tactic:
exact Module.finrank_top_le_finrank_of_isScalarTower
    (separableClosure F K) ((separableClosure E K).restrictScalars F) K

Goal state after:
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
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : φ ∈ E.fixingSubgroup
⊢ False

Tactic:
rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : ∀ x ∈ E, φ x = x
⊢ False
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
⊢ x ∈ ↑(fixedField H ⊓ L) ↔ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(fixedField H ⊓ L)
⊢ x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))

case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : Subgroup Gal(K/k)
L : IntermediateField k K
inst✝ : Normal k ↥L
x : K
h : x ∈ ↑(lift (fixedField (Subgroup.map (restrictNormalHom ↥L) H)))
⊢ x ∈ ↑(fixedField H ⊓ L)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case refine_2
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
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) (a' * b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
h_contra : IsUnit a'
⊢ IsUnit ((mapRingHom (algebraMap R K)) a' * C a.leadingCoeff)

Tactic:
exact
      IsUnit.mul (IsUnit.map _ h_contra)
        (isUnit_iff_exists_inv.mpr
          (Exists.intro (C b.leadingCoeff) <| by rw [← C_mul, this, C_1]))

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
this : q.leadingCoeff = 1
⊢ q.Monic

Tactic:
exact this

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
this : (Polynomial.aeval s) q = 0
⊢ (Polynomial.aeval s) q = 0

Tactic:
exact this

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

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
this : (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier ∈ nhds 1
⊢ FiniteDimensional k ↥L

Tactic:
rw [GroupFilterBasis.nhds_one_eq] at this

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
this : (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier ∈ (galGroupBasis k K).filter
⊢ FiniteDimensional k ↥L
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ L.fixingSubgroup.Normal ↔ IsGalois k ↥L

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
⊢ IsGalois k ↥L

case refine_2
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsGalois k ↥L
⊢ L.fixingSubgroup.Normal