mathlib-initiative/mathlib-tactics huggingface dataset:
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' \ I ∪ B
⊢ ∃ x ∈ X \ I, insert x I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint (insert x I) B

Tactic:
rw [← compl_subset_compl, ← hIB.sdiff_eq_right, ← union_sdiff_distrib, sdiff_eq, compl_inter,
      compl_compl, union_subset_iff, compl_subset_compl] at hB''₂

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.IsBasis I (⋃ i, X i)

Tactic:
by
  convert! IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _ <;> rw [iUnion_const]
  exact (hI (Classical.arbitrary ι)).indep

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
hIJ : I ⊆ J
hJ : M.Indep J
⊢ J ∩ X = J ∩ (X ∩ M.E)

Tactic:
inter_comm X,

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

Goal state before:
pp: R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e : ↥I ⊗[R] ↥J ≃ₗ[R] R
⊢ I = ⊤ ∧ J = ⊤

Tactic:
have e := e.symm ≪≫ₗ Submodule.LinearDisjoint.mulMap
    (.of_left_le_one_of_flat I J <| le_top.trans one_eq_top.ge)

Goal state after:
R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
⊢ I = ⊤ ∧ J = ⊤
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E R : Set α
h : R ⊆ E
⊢ freeOn E ↾ R = freeOn R

Tactic:
simp [h, eq_freeOn_iff]

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

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
⊢ ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
by
      rintro I B hI hImax hBmax
      suffices hcard : I.encard < B.encard by
        obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
        exact ⟨e, ⟨heB, heI⟩, hi⟩
      refine lt_of_not_ge fun hle ↦ ?_
      obtain ⟨x, hxnot, hxI⟩ := exists_insert_of_not_maximal indep_subset hI hImax
      have hlt : B.encard < (insert x I).encard := by
        rwa [encard_insert_of_notMem hxnot, ← not_le, ENat.add_one_le_iff, not_lt]
        rw [encard_ne_top_iff]
        obtain ⟨n, hn⟩ := indep_bdd
        exact finite_of_encard_le_coe (hn _ hI)
      obtain ⟨y, -, hyB, hi⟩ := indep_aug hBmax.prop hxI hlt
      exact hBmax.not_prop_of_ssuperset (ssubset_insert hyB) hi

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Set α
⊢ ∀ ⦃J : Set α⦄,
    (∀ (J : Finset α), ↑J ⊆ I → Indep J) →
      I.Finite →
        (∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1) →
          J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J

Tactic:
J

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I J : Set α
⊢ (∀ (J : Finset α), ↑J ⊆ I → Indep J) →
    I.Finite →
      (∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1) →
        J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
N : Matroid β
f : α → β
h_range : N.E ⊆ range f
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).map f hf = N

Tactic:
refine ext_indep (by simpa [image_preimage_eq_iff]) ?_
  simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, forall_subset_image_iff]
  exact fun I hI ↦ ⟨by grind, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set ↑M.E
⊢ (M.restrictSubtype M.E).IsBasis I X ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X)

Tactic:
restrictSubtype_isBasis_iff,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set ↑M.E
⊢ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X) ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.closure (M.loops ∪ X) = M.closure X

Tactic:
simp [union_comm]

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

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

Tactic:
eRk,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.eRank = (M ↾ M.E).eRank
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
hK : M.IsCocircuit K
f : α
he : f ∈ K
he' : M.IsCircuit {f}
hfe : f ≠ f
⊢ False

Tactic:
exact hfe rfl

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

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

Tactic:
rw [hI.eRk_eq_encard, encard_eq_top_iff, ← hI.finite_iff_isRkFinite, Set.Infinite]

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

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
I : Set α
inst✝ : M.RankFinite
h : M.eRk I = I.encard
hfin : I.Finite
⊢ M.Indep I

Tactic:
rwa [indep_iff_eRk_eq_encard_of_finite hfin]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
⊢ e ∈ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F

Tactic:
M.closure_def' X,

Goal state after:
α : Type u_2
M : Matroid α
e : α
X : Set α
hX : X ⊆ M.E
⊢ e ∈ ⋂₀ {F | M.IsFlat F ∧ X ⊆ F} ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → e ∈ F
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ Y ⊆ M.closure X ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F

Tactic:
M.closure_def' X,

Goal state after:
α : Type u_2
M : Matroid α
Y X : Set α
hX : X ⊆ M.E
⊢ Y ⊆ ⋂₀ {F | M.IsFlat F ∧ X ⊆ F} ↔ ∀ (F : Set α), M.IsFlat F → X ⊆ F → Y ⊆ F
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E

Tactic:
by
  rw [isColoop_iff_sdiff_not_spanning, spanning_iff_closure_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (M.map f hf).eRank = M.eRank

Tactic:
← (hB.map hf).encard_eq_eRank,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (f '' B).encard = M.eRank
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure I

Tactic:
h.closure_eq_closure

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure X
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
B : Set α
inst✝ : M.InvariantCardinalRank
hB : M.IsBase B
⊢ #↑B = M.cRank

Tactic:
have hrw : ∀ B' : {B : Set α // M.IsBase B}, #B' = #B := fun B' ↦ B'.2.cardinalMk_eq hB

Goal state after:
α : Type u
M : Matroid α
B : Set α
inst✝ : M.InvariantCardinalRank
hB : M.IsBase B
hrw : ∀ (B' : { B // M.IsBase B }), #↑↑B' = #↑B
⊢ #↑B = M.cRank
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
⊢ Function.Injective
    (Subtype.val ∘
      ⇑(supportedEquivMvPolynomial (insert i s)).symm ∘
        ⇑(renameEquiv R (Set.subtypeInsertEquivOption h).symm) ∘
          ⇑(optionEquivRight R ↑s).symm ∘ ⇑g ∘ ⇑(optionEquivRight R ↑s) ∘ ⇑(optionEquivLeft R ↑s).symm)

Tactic:
apply Subtype.val_injective.comp

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := ⋯
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
⊢ Function.Injective
    (⇑(supportedEquivMvPolynomial (insert i s)).symm ∘
      ⇑(renameEquiv R (Set.subtypeInsertEquivOption h).symm) ∘
        ⇑(optionEquivRight R ↑s).symm ∘ ⇑g ∘ ⇑(optionEquivRight R ↑s) ∘ ⇑(optionEquivLeft R ↑s).symm)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
I J B B' X Y : Set α
inst✝ : M.Finitary
⊢ ∀ ⦃B B' : Set α⦄ ⦃N : Matroid α⦄, N.Finitary → N.IsBase B → N.IsBase B' → #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
intro B B' N hfin hB hB'

Goal state after:
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
⊢ #↑(B \ B') ≤ #↑(B' \ B)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M✶.E

Tactic:
dual_ground

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∈ M.E
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)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ ¬IsAlgebraic (↥(supported R ∅)) ((RingHom.id (MvPolynomial σ R)) ((Polynomial.aeval (X i)) f))

Tactic:
RingHom.id_apply,

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
⊢ ¬IsAlgebraic (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
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 : AlgebraicIndependent R x
⊢ LinearIndependent R x

Tactic:
rw [linearIndependent_iff_injective_finsuppLinearCombination]

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 : AlgebraicIndependent R x
⊢ Injective ⇑(Finsupp.linearCombination R x)
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:
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.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
hp : ((aeval x).comp (bind₁ f)) p = 0
⊢ (aeval x) ((aeval f) p) = 0

Tactic:
AlgHom.comp_apply

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
hp : (aeval x) ((bind₁ f) p) = 0
⊢ (aeval x) ((aeval f) p) = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x : ι → 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
hx : AlgebraicIndependent R x
ι' : Type u_4
y : ι' → A
hxS : range x ⊆ range ⇑(algebraMap S A)
hy : AlgebraicIndependent S y
e : S ≃ₐ[R] ↥(IsScalarTower.toAlgHom R S A).range := AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x)
x✝ : Algebra (↥Rx) S := ((↑e.symm).comp (Subalgebra.inclusion ⋯)).toAlgebra
⊢ AlgebraicIndependent R (Sum.elim y x)

Tactic:
have : IsScalarTower Rx S A := .of_algebraMap_eq fun x ↦ show _ = (e (e.symm _)).1 by simp

Goal state after:
ι : Type u_1
R : Type u_3
S : Type u
A : Type v
x : ι → 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
hx : AlgebraicIndependent R x
ι' : Type u_4
y : ι' → A
hxS : range x ⊆ range ⇑(algebraMap S A)
hy : AlgebraicIndependent S y
e : S ≃ₐ[R] ↥(IsScalarTower.toAlgHom R S A).range := AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) ⋯
Rx : Subalgebra R A := adjoin R (range x)
x✝ : Algebra (↥Rx) S := ((↑e.symm).comp (Subalgebra.inclusion ⋯)).toAlgebra
this : IsScalarTower (↥Rx) S A
⊢ AlgebraicIndependent R (Sum.elim y 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 X
⊢ False

Tactic:
rwa [closure_insert_eq_of_mem_closure hf, sdiff_self, iff_false_intro (notMem_empty _)] at he

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✝¹ : 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
le : Rv ≤ Subalgebra.restrictScalars R Sv
this✝² : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this✝¹ : IsScalarTower (↥Rv) (↥Sv) A
this✝ : Nontrivial R
this : Algebra.IsAlgebraic (↥(adjoin R (range v))) A
⊢ Algebra.IsAlgebraic S A

Tactic:
have : Algebra.IsAlgebraic Sv A := .extendScalars (Subalgebra.inclusion_injective le)

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
le : Rv ≤ Subalgebra.restrictScalars R Sv
this✝³ : Algebra ↥Rv ↥Sv := (Subalgebra.inclusion le).toAlgebra
this✝² : IsScalarTower (↥Rv) (↥Sv) A
this✝¹ : Nontrivial R
this✝ : Algebra.IsAlgebraic (↥(adjoin R (range v))) A
this : Algebra.IsAlgebraic (↥Sv) A
⊢ Algebra.IsAlgebraic S A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
a✝ : Nontrivial R
this : Unique ι
⊢ IsTranscendenceBasis R fun x ↦ Polynomial.X

Tactic:
refine (isTranscendenceBasis_equiv (Equiv.equivPUnit.{_, 1} _).symm).mp <|
    (MvPolynomial.uniqueAlgEquiv R PUnit).symm.isTranscendenceBasis_iff.mp ?_

Goal state after:
ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
a✝ : Nontrivial R
this : Unique ι
⊢ IsTranscendenceBasis R
    (⇑(uniqueAlgEquiv R PUnit.{?u.54 + 1}).symm ∘ (fun x ↦ Polynomial.X) ∘ ⇑(Equiv.equivPUnit ι).symm)
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)
⊢ Algebra.IsAlgebraic (↥Rxy) A

Tactic:
have := hx.1.algebraMap_injective.nontrivial

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
⊢ Algebra.IsAlgebraic (↥Rxy) A
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 y, minpoly F x = (expand F (q ^ n)) (X - C y)

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
  · have halg : IsIntegral F x := by_contra fun h' ↦ by
      simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h
    exact (minpoly.irreducible halg).natSepDegree_eq_one_iff_of_monic' q
      (minpoly.monic halg) |>.1 h
  rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

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

Tactic:
by
  rw [insepDegree, Subsingleton.elim (separableClosure F F) ⊤, IntermediateField.rank_top]

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 = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F ↑s)) E
t : Set E
hts : t ⊆ ↑s
ht : IsTranscendenceBasis F Subtype.val
⊢ {s | IsTranscendenceBasis F Subtype.val}.Nonempty

Tactic:
lift t to Finset E using s.finite_toSet.subset hts

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 = ⊤
this : Algebra.IsAlgebraic (↥(Algebra.adjoin F ↑s)) E
t : Finset E
hts : ↑t ⊆ ↑s
ht : IsTranscendenceBasis F Subtype.val
⊢ {s | IsTranscendenceBasis F Subtype.val}.Nonempty
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ = finrank F ↥F⟮α⟯ ↔ IsSeparable F α

Tactic:
rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral,
    natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral), IsSeparable]

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
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
x : L
hx : x ∈ E
h_in_F : σ⁻¹ x ∈ F
⊢ σ (g (σ⁻¹ x)) = x

Tactic:
have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x := by
      rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
      exact hg (σ⁻¹ x) h_in_F

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
x : L
hx : x ∈ E
h_in_F : σ⁻¹ x ∈ F
h_g_fix : g (σ⁻¹ x) = σ⁻¹ x
⊢ σ (g (σ⁻¹ x)) = x
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
⊢ ∃ H, ↑H ⊆ W

Tactic:
let S : Subgroup G := {
    carrier := ⋃ n, V ^ (n + 1)
    mul_mem' := fun ha hb ↦ by
      rcases mem_iUnion.mp ha with ⟨k, hk⟩
      rcases mem_iUnion.mp hb with ⟨l, hl⟩
      apply mem_iUnion.mpr
      use k + 1 + l
      rw [add_assoc, pow_add]
      exact Set.mul_mem_mul hk hl
    one_mem' := by
      apply mem_iUnion.mpr
      use 0
      simp [mem_of_mem_nhds hV.nhds]
    inv_mem' := fun ha ↦ by
      rcases mem_iUnion.mp ha with ⟨k, hk⟩
      apply mem_iUnion.mpr
      use k
      rw [← hV.inv]
      simpa only [inv_pow, Set.mem_inv, inv_inv] using hk }

Goal state after:
G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ ∃ H, ↑H ⊆ W