mathlib-initiative/mathlib-tactics huggingface dataset:
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] := ⋯
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
hf : Function.Injective ⇑u
⊢ (Polynomial.aeval (X i)) Polynomial.X =
    (((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
        (Polynomial.aeval (X ⟨i, ⋯⟩)))
      Polynomial.X

Tactic:
;

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] := ⋯
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R := ⋯
hf : Function.Injective ⇑u
⊢ (Polynomial.aeval (X i)) Polynomial.X =
    (((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
        (Polynomial.aeval (X ⟨i, ⋯⟩)))
      Polynomial.X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ {e} ∪ I

Tactic:
singleton_union

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
heEI : e ∈ M.E \ I
J : Set α
hJI : M.IsBasis J (insert e I)
heJ : insert e (⋂₀ Js) ⊆ J
hIb : M.IsBasis I (insert e I)
f : α
hfIJ : f ∈ I \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e I)
⊢ J ⊆ insert e I
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
x✝ : R
⊢ ((algebraMap (↥(supported R ∅)) (MvPolynomial σ R)).comp ↑g) x✝ =
    ((↑(RingHom.id (MvPolynomial σ R))).comp (algebraMap R (MvPolynomial σ R))) x✝

Tactic:
;

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
x✝ : R
⊢ ((algebraMap (↥(supported R ∅)) (MvPolynomial σ R)).comp ↑g) x✝ =
    ((↑(RingHom.id (MvPolynomial σ R))).comp (algebraMap R (MvPolynomial σ R))) x✝
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
⊢ Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f) ↔ i ∉ s ∧ Transcendental R f

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, hf⟩ ↦ transcendental_supported_polynomial_aeval_X R h hf⟩

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ i ∉ s

case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R f
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))
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)

Tactic:
;

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))
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
h : f ∈ M.closure (I \ {e})
a✝ : α
⊢ a✝ ∈ insert f I \ {e} → a✝ ∈ insert f (I \ {e})

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hfI : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
heI : e ∈ I
h : f ∈ M.closure (I \ {e})
a✝ : α
⊢ a✝ ∈ insert f I \ {e} → a✝ ∈ insert f (I \ {e})
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf : f ∉ M.E
heB : e ∈ B
a✝ : α
⊢ a✝ ∈ insert f B \ {e} ∩ M.E → a✝ ∈ B \ {e}

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf : f ∉ M.E
heB : e ∈ B
a✝ : α
⊢ a✝ ∈ insert f B \ {e} ∩ M.E → a✝ ∈ B \ {e}
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
x : { x // x ∈ s }
left✝ : x ∈ t
⊢ ↑x ∈ s

Tactic:
;

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

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

pp: case neg
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : ¬AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

Tactic:
;

Goal state after:
case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y

case neg
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : ¬AlgebraicIndependent R x
⊢ AlgebraicIndependent R (Sum.elim y x) ↔ AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(adjoin R (range x))) y
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ Injective ⇑((AlgHom.restrictScalars R (aeval y)).comp ↑e) ↔ True ∧ Injective ⇑(aeval y)

Tactic:
;

Goal state after:
case pos
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι' : Type u_4
y : ι' → A
hx : AlgebraicIndependent R x
e : MvPolynomial (ι' ⊕ ι) R ≃ₐ[R] MvPolynomial ι' ↥(adjoin R (range x)) :=
  (sumAlgEquiv R ι' ι).trans (mapAlgEquiv ι' hx.aevalEquiv)
this : aeval (Sum.elim y x) = (AlgHom.restrictScalars R (aeval y)).comp ↑e
⊢ Injective ⇑((AlgHom.restrictScalars R (aeval y)).comp ↑e) ↔ True ∧ Injective ⇑(aeval y)
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
s : Set ι
x✝ : A
⊢ x✝ ∈ x '' s ↔ x✝ ∈ range fun i ↦ x ↑i

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
x✝ : A
⊢ x✝ ∈ x '' s ↔ x✝ ∈ range fun i ↦ x ↑i
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_2.e'_2
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ sᶜᶜ = s

Tactic:
;

Goal state after:
case e'_2.e'_2
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ sᶜᶜ = s
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (X ∩ M.E)
hfE : f ∉ M.E
⊢ False
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
insert_inter_of_mem hfE

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e : α
heE : e ∈ M.E
I : Set α
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
hfE : e ∈ M.E
h : M.Indep (insert e (insert e I))
⊢ e ∈ insert e I
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
S : Type u
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Nontrivial R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ trdeg R S + trdeg S A ≤ trdeg R A

Tactic:
rw [← (trdeg R S).lift_id, ← (trdeg S A).lift_id, ← (trdeg R A).lift_id]

Goal state after:
R : Type u_3
S : Type u
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Nontrivial R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ Cardinal.lift.{u, u} (trdeg R S) + Cardinal.lift.{u, u} (trdeg S A) ≤ Cardinal.lift.{u, u} (trdeg R A)
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)
x✝ : ι
⊢ Polynomial.aeval (x x✝) = (aeval x).comp (Polynomial.aeval (X x✝))

Tactic:
;

Goal state after:
ι : 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)
x✝ : ι
⊢ Polynomial.aeval (x x✝) = (aeval x).comp (Polynomial.aeval (X 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
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x✝ : ι
⊢ (Polynomial.aeval (x x✝)) Polynomial.X = ((aeval x).comp (Polynomial.aeval (X x✝))) Polynomial.X

Tactic:
;

Goal state after:
ι : 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)
x✝ : ι
⊢ (Polynomial.aeval (x x✝)) Polynomial.X = ((aeval x).comp (Polynomial.aeval (X x✝))) Polynomial.X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.closure S ⊆ M.closure T

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
S T : Set α
hS : M.Spanning S
hST : S ⊆ T
hT : T ⊆ M.E
⊢ M.closure S ⊆ M.closure T
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.IsBase B
hBI : B ⊆ I
⊢ M.IsBase I

Tactic:
;

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.IsBase B
hBI : B ⊆ I
⊢ M.IsBase I
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case inl
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : Nonempty ι
h✝ : Subsingleton R
⊢ Nonempty { x_1 // x_1 ∈ range x }

Tactic:
;

Goal state after:
case inl
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : Nonempty ι
h✝ : Subsingleton R
⊢ Nonempty { x_1 // x_1 ∈ range x }
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ ⇑f '' range x ⊆ ⇑f '' s

Tactic:
;

Goal state after:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ ⇑f '' range x ⊆ ⇑f '' s
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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
⊢ ⇑↑e.symm ∘ ⇑e ∘ x = x

Tactic:
;

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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
⊢ ⇑↑e.symm ∘ ⇑e ∘ x = x
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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
x✝ : ι
⊢ (⇑↑e.symm ∘ ⇑e ∘ x) x✝ = x x✝

Tactic:
;

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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R x
x✝ : ι
⊢ (⇑↑e.symm ∘ ⇑e ∘ x) x✝ = x x✝
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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
⊢ x = ⇑e.symm ∘ ⇑e ∘ x

Tactic:
;

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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
⊢ x = ⇑e.symm ∘ ⇑e ∘ x
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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
x✝ : ι
⊢ x x✝ = (⇑e.symm ∘ ⇑e ∘ x) x✝

Tactic:
;

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'
e : A ≃ₐ[R] A'
hx : IsTranscendenceBasis R (⇑e ∘ x)
x✝ : ι
⊢ x x✝ = (⇑e.symm ∘ ⇑e ∘ x) x✝
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
inst✝ : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ lift.{v, v} #ι ≤ lift.{v, v} (trdeg R A)

Tactic:
;

Goal state after:
R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ι : Type v
x : ι → A
hx : AlgebraicIndependent R x
⊢ lift.{v, v} #ι ≤ lift.{v, v} (trdeg R A)
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
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
⊢ lift.{v, v} (trdeg R A) ≤ lift.{v, v} (trdeg R A')

Tactic:
;

Goal state after:
R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Injective ⇑f
⊢ lift.{v, v} (trdeg R A) ≤ lift.{v, v} (trdeg R A')
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case e'_4
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
a✝ : Nontrivial R
i : { s // AlgebraicIndepOn R _root_.id s }
x✝ : ↑↑i
⊢ (⇑f ∘ fun a ↦ invFun ⇑f ↑a) x✝ = _root_.id ↑x✝

Tactic:
;

Goal state after:
case e'_4
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
a✝ : Nontrivial R
i : { s // AlgebraicIndepOn R _root_.id s }
x✝ : ↑↑i
⊢ (⇑f ∘ fun a ↦ invFun ⇑f ↑a) x✝ = _root_.id ↑x✝
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
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ lift.{v, v} (trdeg R A') ≤ lift.{v, v} (trdeg R A)

Tactic:
;

Goal state after:
R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hf : Surjective ⇑f
⊢ lift.{v, v} (trdeg R A') ≤ lift.{v, v} (trdeg R A)
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 : Set ι
i✝ : ↑s
⊢ (aeval (x ∘ Subtype.val)) (X i✝) = ((aeval x).comp (rename Subtype.val)) (X i✝)

Tactic:
;

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 : Set ι
i✝ : ↑s
⊢ (aeval (x ∘ Subtype.val)) (X i✝) = ((aeval x).comp (rename Subtype.val)) (X i✝)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ ∀ (r : R), (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (C r)) = (aeval fun o ↦ o.elim a x) (C r)

Tactic:
intro r

Goal state after:
case refine_1
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
r : R
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (C r)) = (aeval fun o ↦ o.elim a x) (C r)
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case mp
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : g • a ∈ s
⊢ a ∈ s

Tactic:
;

Goal state after:
case mp
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : g • a ∈ s
⊢ a ∈ s
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ g • a ∈ s

Tactic:
;

Goal state after:
case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ g • a ∈ s