mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ ↑(comap (algebraMap R S) ⁻¹' {p}) ≃ₜ PrimeSpectrum (p.asIdeal.Fiber S)

Tactic:
letI H : Topology.IsEmbedding (preimageOrderIsoFiber R S p).symm := by
    refine (Topology.IsEmbedding.of_comp_iff .subtypeVal).mp ?_
    have := PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks _ S _
      (Ideal.surjectiveOnStalks_residueField p.asIdeal)
    exact ((Homeomorph.prodUnique _ _).isEmbedding.comp this).comp
      (homeomorphOfRingEquiv (Algebra.TensorProduct.comm _ _ _).toRingEquiv).isEmbedding
  exact
  { __ := preimageOrderIsoFiber R S p
    continuous_toFun := by
      convert!
        (H.toHomeomorphOfSurjective (preimageOrderIsoFiber R S p).symm.surjective).symm.continuous
      ext1 x
      obtain ⟨x, rfl⟩ := (H.toHomeomorphOfSurjective
        (preimageOrderIsoFiber R S p).symm.surjective).surjective x
      simp only [Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Homeomorph.symm_apply_apply]
      simp
    continuous_invFun := H.continuous }

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
⊢ 1 ∈ f.range

Tactic:
use Finsupp.equivFunOnFinite.symm fun i ↦ i.1.2

Goal state after:
case h
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := ⋯
e : M ⊗[R] N ≃ₗ[R] R := ⋯
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := ⋯
⊢ f (Finsupp.equivFunOnFinite.symm fun i ↦ (↑i).2) = 1
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : K
⊢ IntermediateField.adjoin F ((minpoly F x).rootSet L) ≤ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L)

Tactic:
apply le_iSup _ x

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ ∃ s, Ideal.span ↑s = ⊤ ∧ ∀ r ∈ s, Free (Localization.Away r) (LocalizedModule.Away r M)

Tactic:
by
  classical
  -- write 1 = ∑ᵢ fᵢ(mᵢ) with `mᵢ : M` and `fᵢ : Dual R M`
  obtain ⟨S, hS⟩ := ((linearEquiv R M).symm 1).exists_finset
  refine ⟨S.image fun i ↦ i.1 i.2, ?_, fun r hr ↦ ?_⟩
  -- Part 1: The evaluations fᵢ(mᵢ) generate the unit ideal
  · simpa [Ideal.eq_top_iff_one, (LinearEquiv.symm_apply_eq _).mp hS, linearEquiv]
      using Ideal.sum_mem _ fun i hi ↦ Ideal.subset_span (Finset.mem_image_of_mem _ hi)
  -- Part 2: After localizing at any f(m), the module becomes free
  obtain ⟨⟨f, m⟩, _, rfl⟩ := Finset.mem_image.mp hr
  -- Extend f to a R_{f(m)}-linear functional f' on the localized module
  let f' : Dual (Localization.Away (f m)) (LocalizedModule.Away (f m) M) :=
    .extendScalarsOfIsLocalization (.powers (f m)) _ <| IsLocalizedModule.map
      (.powers (f m)) (LocalizedModule.mkLinearMap _ M) (Algebra.linearMap R _) f
  -- f'(m/1) = f(m)/1 is a unit in R_{f(m)}, so f' is surjective and therefore bijective
  have surj : Function.Surjective f' := LinearMap.range_eq_top.mp <| Ideal.eq_top_of_isUnit_mem
    _ ⟨_, IsLocalizedModule.map_apply ..⟩ (IsLocalization.Away.algebraMap_isUnit (f m))
  exact .of_equiv <| .symm <| .ofBijective f' (bijective_of_surjective surj)

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.Nonempty

Tactic:
by
  rw [nonempty_iff_ne_empty]; rintro rfl; exact M.empty_not_isBase hB

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ ¬M.Dep X ↔ M.Indep X

Tactic:
rw [Dep, and_iff_left hX, not_not]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: 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)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective ⇑((LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m)
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑m

Tactic:
coe_comp

Goal state after:
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)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑(LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ ⇑m)
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑m
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:
· exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ (e_1 : α), e_1 = e ∧ e_1 ∉ I ∨ e_1 ∈ I ∧ e_1 ∉ I → ¬M.Indep (insert e_1 I) ∧ e_1 ∈ M.E) ↔
    ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I

Tactic:
and_not_self,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
⊢ (∀ (e_1 : α), e_1 = e ∧ e_1 ∉ I ∨ False → ¬M.Indep (insert e_1 I) ∧ e_1 ∈ M.E) ↔
    ¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ x, M.IsBase x ∧ M.E \ x = B

Tactic:
refine ⟨fun h ↦ ⟨_, h.1, sdiff_sdiff_cancel_left h.2⟩,
    fun ⟨B', hB', h⟩ ↦ ⟨?_,h.symm.trans_subset sdiff_subset⟩⟩

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
x✝ : ∃ x, M.IsBase x ∧ M.E \ x = B
B' : Set α
hB' : M.IsBase B'
h : M.E \ B' = B
⊢ M.IsBase (M.E \ B)
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : M.IsBasis I X
hNM : N ≤r M
hX : X ⊆ N.E
⊢ N.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM; rwa [isBasis_restrict_iff, and_iff_left (show X ⊆ R from hX)]

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

Goal state before:
pp: β : Type u_2
N : Matroid β
⊢ ∀ ⦃I : Set β⦄, I ⊆ (N.comap id).E → ((N.comap id).Indep I ↔ N.Indep I)

Tactic:
by simp [injective_id.injOn]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : M.IsBasis I X
hJ : M.IsBasis J X
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}

Tactic:
rw [← isBase_restrict_iff] at hI hJ; exact hI.eq_exchange_of_sdiff_eq_singleton hJ hIJ

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ ¬M.Dep X

Tactic:
exact fun h ↦ hXC.ne ((isCircuit_iff.1 hC).2 h hXC.subset)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

Tactic:
IsCircuit,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ Minimal M.Dep C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I
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))
⊢ z ∈ M.closure ((⋃ i, I i) ∪ J \ {z})

Tactic:
closure_union_congr_left <| closure_iUnion_congr _ _ hC',

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))
⊢ z ∈ M.closure ((⋃ i, insert (x i) (I i)) ∪ J \ {z})
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)

Tactic:
rw [sInter_eq_biInter]

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis ((⋂ i ∈ Xs, i) ∩ I) (⋂ i ∈ Xs, i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Xs : Set (Set α)
hI : M.Indep I
hXs : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis (X ∩ I) X
⊢ M.IsBasis (⋂₀ Xs ∩ I) (⋂₀ Xs)

Tactic:
by
  rw [sInter_eq_biInter]
  exact hI.inter_isBasis_biInter hXs h

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure X
hef : e ∈ M.closure (insert f X)
⊢ f ∈ M.closure (insert e X)

Tactic:
rw [← closure_inter_ground] at *
  have hfE : f ∈ M.E := by
    by_contra! hfE; rw [insert_inter_of_notMem hfE] at hef; exact he hef
  have heE : e ∈ M.E := (M.closure_subset_ground _) hef
  rw [insert_inter_of_mem hfE] at hef; rw [insert_inter_of_mem heE]
  obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
  rw [← hI.closure_eq_closure, hI.indep.notMem_closure_iff] at he
  rw [← closure_insert_closure_eq_closure_insert, ← hI.closure_eq_closure,
    closure_insert_closure_eq_closure_insert, he.1.mem_closure_iff] at *
  rw [or_iff_not_imp_left, dep_iff, insert_comm,
    and_iff_left (insert_subset heE (insert_subset hfE hI.indep.subset_ground)), not_not]
  intro h
  rw [(h.subset (subset_insert _ _)).mem_closure_iff, or_iff_right (h.not_dep), mem_insert_iff,
    or_iff_left he.2] at hef
  subst hef; apply mem_insert

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
⊢ AlgebraicIndependent R fun i ↦ (Polynomial.aeval (X i)) (f i)

Tactic:
set x := fun i ↦ Polynomial.aeval (X i : MvPolynomial ι R) (f i)
  refine algebraicIndependent_of_finite_type' (C_injective _ _) fun t _ _ i hi ↦ ?_
  have hle : adjoin R (x '' t) ≤ supported R t := by
    rw [Algebra.adjoin_le_iff, Set.image_subset_iff]
    intro _ h
    rw [Set.mem_preimage]
    refine Algebra.adjoin_mono ?_ (Polynomial.aeval_mem_adjoin_singleton R _)
    simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]
  exact (transcendental_supported_polynomial_aeval_X R hi (hf i)).of_tower_top_of_subalgebra_le hle

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

Goal state before:
pp: α : Type u_2
I E X : Set α
⊢ X ∩ (E ∩ E) ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I

Tactic:
inter_self,

Goal state after:
α : Type u_2
I E X : Set α
⊢ X ∩ E ∩ I ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ h⁻¹ • g • x = h⁻¹ • x ↔ x ∈ fixedBy α g

Tactic:
smul_left_cancel_iff,

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
comm : Commute g h
x : α
⊢ g • x = x ↔ x ∈ fixedBy α g
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
ι' : Type u'
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
x✝ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
⊢ Algebra.IsAlgebraic (↥Rxy) A

Tactic:
have : IsScalarTower Rxy Sy A := .of_algebraMap_eq fun ⟨a, _⟩ ↦ show a = _ from rfl

Goal state after:
case inr
ι : Type u
ι' : Type u'
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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝² : Nontrivial S
this✝¹ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝ : Algebra.IsAlgebraic (↥Sy) A
x✝ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥Rxy) (↥Sy) A
⊢ Algebra.IsAlgebraic (↥Rxy) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s t : Set A
⊢ (matroid R A).IsBasis s t ↔ s = t

Tactic:
have := (FaithfulSMul.algebraMap_injective R A).subsingleton

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s t : Set A
this : Subsingleton R
⊢ (matroid R A).IsBasis s t ↔ s = t
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 : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{w, u} #ι = lift.{u, w} #↑(range x)

Tactic:
lift_mk_eq'.mpr ⟨.ofInjective _ hx.1.injective⟩

Goal state after:
ι : 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 : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{u, w} #↑(range x) = lift.{u, w} #↑(range x)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
by
  classical
  let _ := i.toAlgebra
  simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
    aroots_def, map_map, ← IsScalarTower.algebraMap_eq]

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⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E := ⋯
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : (Polynomial.map (algebraMap F ↥F⟮α⟯) (minpoly F α)).Splits
⊢ Gal(E/F) ≃ Gal(↥F⟮α⟯/F)

Tactic:
exact Equiv.mk (fun ϕ => iso.trans (ϕ.trans iso.symm)) fun ϕ => iso.symm.trans (ϕ.trans iso)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: 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
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
convert_to _ ↔ ∃ (n : ℕ) (y : F), Polynomial.aeval x (X ^ q ^ n - C y) = 0
  · simp_rw [RingHom.mem_range, map_sub, map_pow, aeval_C, aeval_X, sub_eq_zero, eq_comm]
  refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
  · obtain ⟨n, y, hx⟩ := (minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
    exact ⟨n, y, hx ▸ aeval F x⟩
  have hnezero := X_pow_sub_C_ne_zero (expChar_pow_pos F q n) y
  refine ((natSepDegree_le_of_dvd _ _ (minpoly.dvd F x h) hnezero).trans_eq <|
    natSepDegree_X_pow_char_pow_sub_C q n y).antisymm ?_
  rw [Nat.one_le_iff_ne_zero, natSepDegree_ne_zero_iff, ← Nat.one_le_iff_ne_zero]
  exact minpoly.natDegree_pos <| IsAlgebraic.isIntegral ⟨_, hnezero, 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
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.IsAlgebraic (↥(Algebra.adjoin F ↑s)) E

Tactic:
rw [← isAlgebraic_adjoin_iff_top, hs, Algebra.isAlgebraic_iff_isIntegral]

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ Algebra.IsIntegral (↥⊤) E
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: case refine_1
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
⊢ F ∈ finiteExts K L

pp: case refine_2
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
⊢ g ∈ (fun x ↦ σ * x * σ⁻¹) ⁻¹' (fun g ↦ g.carrier) E.fixingSubgroup

Tactic:
· have : FiniteDimensional K E := hE
      exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom

Goal state after:
case refine_2
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
⊢ g ∈ (fun x ↦ σ * x * σ⁻¹) ⁻¹' (fun g ↦ g.carrier) E.fixingSubgroup
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
x✝ : Algebra.IsSeparable F ↥F⟮x⟯
⊢ IsSeparable F x

pp: case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
⊢ Algebra.IsSeparable F ↥F⟮x⟯

Tactic:
· exact isSeparable_of_mem_isSeparable F E <| mem_adjoin_simple_self F x

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hsep : IsSeparable F x
⊢ Algebra.IsSeparable F ↥F⟮x⟯
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_2
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
N₁ N₂ : Submodule R M
⊢ N₁ ≤ B.flip.dualSubmodule N₂ ↔ N₂ ≤ B.dualSubmodule N₁

Tactic:
change (∀ (x : M), x ∈ N₁ → _) ↔ ∀ (x : M), x ∈ N₂ → _
  simp only [mem_dualSubmodule, Submodule.mem_one, flip_apply]
  exact forall₂_comm

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

Goal state before:
pp: case a
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
y : ↥L
hx : ∀ f ∈ L.fixingSubgroup, f ↑y = ↑y
mem : ↑y ∈ (adjoin ↥L {↑y}).toIntermediateField
this✝ : IntermediateField.fixedField ⊤ = ⊥
this : ⟨↑y, mem⟩ ∈ ⊥
hy : (algebraMap ↥L ↥(adjoin ↥L {↑y}).toIntermediateField) y = ⟨↑y, mem⟩
⊢ ↑y ∈ L

Tactic:
exact y.2

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

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1)) - x ^ (i + 1) ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
rw [coeff_minpolyDiv, add_sub_assoc, pow_succ, ← sub_mul, Algebra.algebraMap_eq_smul_one]

Goal state after:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) • 1 +
      ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))