mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
⊢ Subgroup.map (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
      (toPrincipalIdeal R (FractionRing R)).range =
    (toPrincipalIdeal R K).range

Tactic:
ext I

Goal state after:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ I ∈
      Subgroup.map (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
        (toPrincipalIdeal R (FractionRing R)).range ↔
    I ∈ (toPrincipalIdeal R K).range
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
⊢ Subgroup.map (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)).toMonoidHom (toPrincipalIdeal R K).range =
    (toPrincipalIdeal S L).range

Tactic:
ext I

Goal state after:
R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
⊢ I ∈ Subgroup.map (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)).toMonoidHom (toPrincipalIdeal R K).range ↔
    I ∈ (toPrincipalIdeal S L).range
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: 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) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : 1 = e (∑ 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
⊢ ∑ i, (↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1) ((Finsupp.equivFunOnFinite.symm fun i ↦ (↑i).2) i) = 1

Tactic:
map_sum,

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) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : 1 = ∑ x ∈ S, e (x.1 ⊗ₜ[R] x.2)
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
⊢ ∑ i, (↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1) ((Finsupp.equivFunOnFinite.symm fun i ↦ (↑i).2) i) = 1
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum S
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)

Tactic:
let q : PrimeSpectrum R := p.comap (algebraMap R S)

Goal state after:
R : Type uR
M : Type uM
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
inst✝² : Module.Finite R M
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum S
q : PrimeSpectrum R := comap (algebraMap R S) p
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)
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
⊢ Pic.mk R M = 1 ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
← mk_self,

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ Pic.mk R M = Pic.mk R R ↔ Nonempty (M ≃ₗ[R] R)
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
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
S : Set K
splits : ∀ x ∈ S, IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : K
hx : x ∈ adjoin F S
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

Tactic:
by
  let E : IntermediateField F L := ⨆ x : S, adjoin F ((minpoly F x.val).rootSet L)
  have normal : Normal F E := normal_iSup (h := fun x ↦
    Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField (splits x x.2).2))
  have : ∀ x ∈ S, ((minpoly F x).map (algebraMap F E)).Splits := fun x hx ↦ splits_of_splits
    (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)
  obtain ⟨φ⟩ := nonempty_algHom_adjoin_of_splits fun x hx ↦ ⟨(splits x hx).1, this x hx⟩
  convert! (normal.splits <| φ ⟨x, hx⟩).map E.val.toRingHom
  simp [minpoly.algHom_eq _ φ.injective, ← minpoly.algHom_eq _ (adjoin F S).val.injective,
    Polynomial.map_map]

Goal state after:
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
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
⊢ IntermediateField.map E.val (↑g).fieldRange = E

Tactic:
AlgEquiv.fieldRange_eq_top g,

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
⊢ IntermediateField.map E.val ⊤ = E
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
exact hcard

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

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
⊢ ∀ ⦃I : Set α⦄, M.Indep I ↔ ∃ B, Maximal M.Indep B ∧ I ⊆ B

Tactic:
refine fun I ↦ ⟨fun h ↦ ?_, fun ⟨B, ⟨h, _⟩, hIB'⟩ ↦ M.indep_subset h hIB'⟩

Goal state after:
α : Type u_1
M : IndepMatroid α
I : Set α
h : M.Indep I
⊢ ∃ B, Maximal M.Indep B ∧ I ⊆ B
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
⊢ (unitsToPic R A).ker = (Units.map ↑(spanSingleton R)).range

Tactic:
ext I

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

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

Tactic:
ext I

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

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (x : Set α), IsBase x = M.IsBase x

Tactic:
by simp [hB]

Goal state after:
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''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
compl_subset_compl

Goal state after:
α : 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''ᶜ
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
hex : ∃ M, E = M.E ∧ M.Indep = Indep
⊢ ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I

Tactic:
by obtain ⟨M, -, rfl⟩ := hex; exact fun I J hJ hIJ ↦ hJ.subset hIJ

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
⊢ ∃ M_1, f '' M.E = M_1.E ∧ ∀ (I : Set β), M_1.Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
refine ⟨M.mapSetEmbedding ⟨_, hf.injective⟩, by simp, fun I ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (M.mapSetEmbedding { toFun := M.E.domRestrict f, inj' := ⋯ }).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : f '' D₀ = f '' I
⊢ False

Tactic:
rw [hf.image_eq_image_iff hD₀E hI.subset_ground] at h_eq

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
D₀ : Set α
hD₀ : ¬M.Indep D₀
hD₀E : D₀ ⊆ M.E
I : Set α
hI : M.Indep I
h_eq : D₀ = I
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

Tactic:
simp_rw [isCircuit_def, minimal_subset_iff, eq_comm (a := C)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X✝ I : Set α
M : Matroid α
inst✝ : M.Finitary
X : Set α
⊢ (M.restrictSubtype X).Finitary

Tactic:
rw [restrictSubtype]; infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X✝ I : Set α
M : Matroid α
inst✝ : M.RankFinite
X : Set α
⊢ (M.restrictSubtype X).RankFinite

Tactic:
rw [restrictSubtype]; infer_instance

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRk univ = M.eRank

Tactic:
rw [← eRk_inter_ground, univ_inter, eRank_def]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
hIfin : I.Finite
h : M.eRank ≤ M.eRk I
⊢ M.IsBase I

Tactic:
simpa using hI.isBasis_of_eRk_ge hIfin hI.subset_ground (M.eRk_ground.trans_le h)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
this :
  ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a
⊢ M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)

Tactic:
simpa [closure, subtypeClosure, Set.ext_iff]

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

Goal state before:
pp: α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure (Y ∩ M.E)

Tactic:
exact M.subset_closure_of_subset (subset_inter hXY hX)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I)

Tactic:
rwa [insert_eq_of_mem h]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I (M.closure I)

Tactic:
rw [hI.closure_eq_setOfPred_isBasis_insert]; exact hI.isBasis_setOfPred_insert_isBasis

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ e ∈ M.closure I \ I

Tactic:
by
  rw [mem_sdiff, hI.mem_closure_iff, or_and_right, and_not_self_iff, or_false,
    iff_self_and, imp_not_comm]
  intro heI; rw [insert_eq_of_mem heI]; exact hI.not_dep

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
⊢ Minimal M✶.Dep K ↔ Minimal (fun X ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
aux,

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ Minimal (fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K ↔
    Minimal (fun X ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α β : Type u
f : α → β
X : Set β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf).cRk X = (M.map f hf).cRk (f '' (f ⁻¹' X ∩ M.E))

Tactic:
image_preimage_inter,

Goal state after:
α β : Type u
f : α → β
X : Set β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf).cRk X = (M.map f hf).cRk (X ∩ f '' M.E)
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
ext I

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.removeLoops.Indep I ↔ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ f '' (f ⁻¹' I ∩ X) = I

Tactic:
image_preimage_inter,

Goal state after:
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
I₀ : Set α
hI₀ss : I₀ ⊆ f ⁻¹' I ∩ X
hbij : BijOn f I₀ (f '' (f ⁻¹' I ∩ X))
⊢ I ∩ f '' X = I
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
I X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ #↑I = (M ↾ X).cRank

Tactic:
(isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank

Goal state after:
α : Type u
M : Matroid α
I X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ (M ↾ X).cRank = (M ↾ X).cRank
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
inst✝ : Unique ι
⊢ AlgebraicIndependent R x ↔ Transcendental R (x default)

Tactic:
by
  rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]
  let i := uniqueAlgEquiv R ι
  have key : aeval (R := R) x = (Polynomial.aeval (R := R) (x default)).comp i := by
    ext y
    simp [i, Subsingleton.elim y default]
  simp [key]

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 (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (insert f X) = M.closure (insert e X)

Tactic:
← closure_closure,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (M.closure (insert f X)) = M.closure (insert e X)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
← closure_closure,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure (insert e X) \ M.closure X
⊢ M.closure (M.closure (insert f (insert e X))) = M.closure (insert e X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.closure S = M.E ∧ S ⊆ M.E ↔ M.closure S = M.E

Tactic:
and_iff_left hS

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.closure S = M.E ↔ M.closure S = M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ (∃ B, M.IsBase B ∧ B ⊆ S) ∧ S ⊆ M.E ↔ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
and_iff_left hS

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ (∃ B, M.IsBase B ∧ B ⊆ S) ↔ ∃ B, M.IsBase B ∧ B ⊆ S
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
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
⊢ False

Tactic:
have ⟨a, has, hax⟩ := not_subset.mp this

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
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False
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
x✝ : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
h✝ : Nontrivial R
B_base : Algebra.IsAlgebraic (↥(adjoin R B)) A
a x : A
hx : x ∈ B \ I
h : ¬IsAlgebraic (↥(adjoin R I)) x
⊢ ∃ x ∈ B \ I, AlgebraicIndepOn R _root_.id (insert x I)

Tactic:
exact ⟨x, hx, I_ind.insert <| by rwa [image_id]⟩

Goal state after:
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 : Set A
⊢ (matroid R A).Spanning s ↔ s = univ

Tactic:
simp_rw [Matroid.spanning_iff, matroid_closure_of_subsingleton, matroid_e, subset_univ, and_true]

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
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
have := (FaithfulSMul.algebraMap_injective S A).noZeroDivisors _ (map_zero _) (map_mul _)

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
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
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:
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.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h✝ : f = 0 ∨ g = 0
hf : f = 0
x✝ : ∃ x, C x = g
x : F
h : C x = g
⊢ 0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g

pp: case refine_2
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g) → ∃ x, C x = g

Tactic:
· by_cases hx : x = 0
      · exact .inl ⟨rfl, by rw [← h, hx, map_zero]⟩
      exact .inr ⟨x, Ne.isUnit hx, h⟩

Goal state after:
case refine_2
F : Type u
inst✝ : Field F
f✝ f g : F[X]
h : f = 0 ∨ g = 0
hf : f = 0
⊢ (0 = 0 ∧ g = 0 ∨ ∃ r, IsUnit r ∧ C r = g) → ∃ x, C x = g
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
σ : Gal(L/K)
⊢ (map (↑σ) E).fixingSubgroup = MulAut.conj σ • E.fixingSubgroup

Tactic:
ext τ
  simp only [coe_map, AlgEquiv.coe_toAlgHom, Set.mem_image, SetLike.mem_coe, AlgEquiv.smul_def,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
    Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← symm_apply_eq,
    IntermediateField.fixingSubgroup, mem_fixingSubgroup_iff]
  rfl

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
⊢ ∀ (m₀ : M) {U : Set M}, U ∈ BM.sets → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
by
      intro m₀ U U_in
      rcases smul_right m₀ U_in with ⟨V, V_in, H⟩
      exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) H

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

Goal state before:
pp: 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
inst✝ : Normal F E'
⊢ (Subgroup.comap (restrictNormalHom E) L.fixingSubgroup).index = L.fixingSubgroup.index

Tactic:
L.fixingSubgroup.index_comap_of_surjective
    (AlgEquiv.restrictNormalHom_surjective _)

Goal state after:
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
inst✝ : Normal F E'
⊢ L.fixingSubgroup.index = L.fixingSubgroup.index
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
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
⊢ (↑L.fixingSubgroup)ᶜ ∈ nhds σ

Tactic:
apply mem_nhds_iff.mpr

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
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
⊢ ∃ t ⊆ (↑L.fixingSubgroup)ᶜ, IsOpen t ∧ σ ∈ t