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

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

Tactic:
spanning_iff_closure_eq

Goal state after:
α : Type u_1
M : Matroid α
e : α
⊢ ¬M.closure (M.E \ {e}) = M.E ↔ M.closure (M.E \ {e}) ≠ M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case e'_2.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E = ↑(⨆ i, M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩)

pp: case e'_3.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ⋃ i, Xs i ∩ M.E = ↑(⨆ i, ⟨Xs i ∩ M.E, ⋯⟩)

Tactic:
<;>

Goal state after:
case e'_2.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E = ↑(⨆ i, M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩)

case e'_3.e'_3
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ ⋃ i, Xs i ∩ M.E = ↑(⨆ i, ⟨Xs i ∩ M.E, ⋯⟩)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (⋃ i, M.closure (if i = true then X else Y)) =
    M.closure (⋃ b, if b = true then M.closure X else M.closure Y)

Tactic:
apply_ite

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.eRk X + M.eRank = M✶.eRk (X ∩ M.E) + M.eRank

Tactic:
← dual_ground,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.eRk X + M.eRank = M✶.eRk (X ∩ M✶.E) + 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:
← M.closure_closure I,

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ ¬M.Spanning (M.E \ (M.E \ M.closure (B \ {e}))) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t

Tactic:
sdiff_sdiff_cancel_left (M.closure_subset_ground _),

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ ¬M.Spanning (M.closure (B \ {e})) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ M.removeLoops_eq_self⟩
  rw [← h]
  infer_instance

Goal state after:
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
⊢ (∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)

Tactic:
have hiX : ⋂₀ Js ⊆ I := (sInter_subset_of_mem hne.some_mem).trans (hIs _ hne.some_mem)

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
⊢ (∀ i ∈ Js, M.closure (⋂₀ Js) ⊆ M.closure i) ∧ ⋂ J ∈ Js, M.closure J ⊆ M.closure (⋂₀ Js)
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)
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)
hf : Function.Injective ⇑u
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))

Tactic:
have h1 : Polynomial.aeval (X i : MvPolynomial σ R) = ((Subalgebra.val _).comp
      (supportedEquivMvPolynomial _).symm.toAlgHom |>.comp
      (Polynomial.aeval (X ⟨i, s.mem_insert i⟩ : MvPolynomial ↑(insert i s) R))) := by
    ext1; simp

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] := mapAlgHom (Polynomial.aeval f)
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)
hf : Function.Injective ⇑u
h1 :
  Polynomial.aeval (X i) =
    ((supported R (insert i s)).val.comp ↑(supportedEquivMvPolynomial (insert i s)).symm).comp
      (Polynomial.aeval (X ⟨i, ⋯⟩))
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ C ∩ K ≠ {e}

Tactic:
intro he
  have heC : e ∈ C := (he.symm.subset rfl).1
  simp_rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_iff_forall_ssubset, not_not] at hK
  have' hKe := hK.2 (t := K \ {e}) (sdiff_singleton_ssubset.2 (he.symm.subset rfl).2)
  apply hK.1
  rw [spanning_iff_ground_subset_closure]
  nth_rw 1 [← hKe.closure_eq, sdiff_sdiff_eq_sdiff_union]
  · refine (M.closure_subset_closure (subset_union_left (t := C))).trans ?_
    rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← closure_union_congr_right
      (hC.closure_sdiff_singleton_eq e), union_eq_self_of_subset_right]
    rw [← he, sdiff_self_inter]
    exact sdiff_subset_sdiff_left hC.subset_ground
  rw [← he]
  exact inter_subset_left.trans hC.subset_ground

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

Goal state before:
pp: case e'_2
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ ⋂ i ∈ A, I i = ⋂ i, I ↑i

pp: case e'_3
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ ⋂ i ∈ A, M.closure (I i) = ⋂ i, M.closure (I ↑i)

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ ⋂ i ∈ A, I i = ⋂ i, I ↑i

case e'_3
α : Type u_2
M : Matroid α
ι : Type u_4
A : Set ι
hA : A.Nonempty
I : ι → Set α
h : M.Indep (⋃ i ∈ A, I i)
this : Nonempty ↑A
⊢ ⋂ i ∈ A, M.closure (I i) = ⋂ i, M.closure (I ↑i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case e'_3
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i, X i = ⋂ i ∈ univ, X i.down

pp: case e'_4
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i, X i = ⋂ i ∈ univ, X i.down

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i, X i = ⋂ i ∈ univ, X i.down

case e'_4
α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
X : ι → Set α
hI : M.Indep I
h : ∀ (i : ι), M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i, X i = ⋂ i ∈ univ, X i.down
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))

pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))

Tactic:
<;>

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))

α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) ⊆ M.closure I

pp: case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure I ⊆ M.closure (insert f I \ {e})

Tactic:
<;>

Goal state after:
case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure (insert f I \ {e}) ⊆ M.closure I

case a
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep I
hf : f ∈ M.closure I
he : e ∈ M.closure (insert f I \ {e})
⊢ M.closure I ⊆ M.closure (insert f I \ {e})
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_1.e'_4.none
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) none = none.elim (x i) fun i ↦ x ↑i

pp: case e'_1.e'_4.some
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
val✝ : { i // i ∈ s }
⊢ ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) (some val✝) = (some val✝).elim (x i) fun i ↦ x ↑i

Tactic:
<;>

Goal state after:
case e'_1.e'_4.none
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
⊢ ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) none = none.elim (x i) fun i ↦ x ↑i

case e'_1.e'_4.some
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
i : ι
h : i ∉ s
val✝ : { i // i ∈ s }
⊢ ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) (some val✝) = (some val✝).elim (x i) fun i ↦ x ↑i
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ M.closure (insert f B \ {e})
heB : e ∈ insert f B
⊢ M.IsBase (insert f B \ {e})

Tactic:
by
  rw [← isBasis_ground_iff] at hB ⊢
  by_cases hf : f ∈ M.E
  · exact hB.isBasis_insert_sdiff_of_mem_closure he heB hf
  obtain rfl | heB := heB
  · simpa [show e ∉ B from fun h ↦ hf (hB.1.1.2 h)] using hB
  rw [← closure_inter_ground] at he
  cases hB.indep.notMem_closure_sdiff_of_mem heB (M.closure_subset_closure (by intro; aesop) he)

Goal state after:
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
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h✝ : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
h : ↑x = a
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x

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
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h✝ : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
h : ¬↑x = a
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x

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
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h✝ : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
h : ↑x = a
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x

case neg
ι : Type u_1
R : Type u_3
A : Type v
x✝ : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
ind : AlgebraicIndependent R fun i ↦ x✝ ↑i
H :
  ∀ (t : Set ι),
    t.Finite → (AlgebraicIndependent R fun i ↦ x✝ ↑i) → ∀ i ∉ s, i ∉ t → Transcendental (↥(adjoin R (x✝ '' t))) (x✝ i)
t : Set ι
hfin : t.Finite
a : ι
u : Set ι
ha : a ∈ t \ s
hu : u ⊆ t \ s
ha' : a ∉ u
h✝ : AlgebraicIndependent R fun i ↦ x✝ ↑i
this : a ∉ t ∩ s ∪ u
x : ↑(t ∩ s ∪ insert a u)
h : ¬↑x = a
⊢ x✝ ↑x = (((fun o ↦ o.elim (x✝ a) fun i ↦ x✝ ↑i) ∘ ⇑(subtypeInsertEquivOption this)) ∘ ⇑(Equiv.setCongr ⋯)) x
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case inl
ι : 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)
val✝ : ι'
⊢ (aeval (Sum.elim y x)) (X (Sum.inl val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inl val✝))

pp: case inr
ι : 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)
val✝ : ι
⊢ (aeval (Sum.elim y x)) (X (Sum.inr val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inr val✝))

Tactic:
<;>

Goal state after:
case inl
ι : 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)
val✝ : ι'
⊢ (aeval (Sum.elim y x)) (X (Sum.inl val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inl val✝))

case inr
ι : 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)
val✝ : ι
⊢ (aeval (Sum.elim y x)) (X (Sum.inr val✝)) = ((AlgHom.restrictScalars R (aeval y)).comp ↑e) (X (Sum.inr val✝))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case hC
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
x✝ : R
⊢ (((aeval x).comp (MvPolynomial.map (algebraMap R K))).comp C) x✝ = ((aeval x).comp C) x✝

pp: case hX
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
i✝ : ι
⊢ ((aeval x).comp (MvPolynomial.map (algebraMap R K))) (X i✝) = (aeval x).toRingHom (X i✝)

Tactic:
<;>

Goal state after:
case hC
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
x✝ : R
⊢ (((aeval x).comp (MvPolynomial.map (algebraMap R K))).comp C) x✝ = ((aeval x).comp C) x✝

case hX
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
i✝ : ι
⊢ ((aeval x).comp (MvPolynomial.map (algebraMap R K))) (X i✝) = (aeval x).toRingHom (X i✝)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_1.inl
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
val✝ : ↑sᶜ
⊢ (x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s))) (Sum.inl val✝) =
    Sum.elim (fun i ↦ x ↑i) (fun i ↦ x ↑i) (Sum.inl val✝)

pp: case e'_1.inr
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
val✝ : ↑s
⊢ (x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s))) (Sum.inr val✝) =
    Sum.elim (fun i ↦ x ↑i) (fun i ↦ x ↑i) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case e'_1.inl
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
val✝ : ↑sᶜ
⊢ (x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s))) (Sum.inl val✝) =
    Sum.elim (fun i ↦ x ↑i) (fun i ↦ x ↑i) (Sum.inl val✝)

case e'_1.inr
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
val✝ : ↑s
⊢ (x ∘ ⇑((Equiv.sumComm ↑sᶜ ↑s).trans (Equiv.Set.sumCompl s))) (Sum.inr val✝) =
    Sum.elim (fun i ↦ x ↑i) (fun i ↦ x ↑i) (Sum.inr val✝)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
⊢ M.Spanning (M.E \ X) ↔ M.closure (M.E \ X) = M.E

Tactic:
spanning_iff_closure_eq

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
⊢ M.closure (M.E \ X) = M.E ↔ M.closure (M.E \ X) = M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
h : M = loopyOn M.E
⊢ M.closure ∅ = M.E

Tactic:
rw [h, loopyOn_closure_eq, loopyOn_ground]

Goal state after:
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)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) (C r) =
      ↑(aeval fun o ↦ o.elim a x) (C r)

pp: case refine_2
ι : 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
⊢ ∀ (i : Option ι),
    ((↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) (X i) =
      ↑(aeval fun o ↦ o.elim a x) (X i)

Tactic:
<;>

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)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) (C r) =
      ↑(aeval fun o ↦ o.elim a x) (C r)

case refine_2
ι : 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
⊢ ∀ (i : Option ι),
    ((↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom) (X i) =
      ↑(aeval fun o ↦ o.elim a x) (X i)
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
⊢ g • a ∈ s → a ∈ s

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 ∈ s → g • 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
⊢ g • a ∈ s → a ∈ s

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 ∈ s → g • a ∈ s
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ fixedBy α m = Set.univ ↔ (fun x2 ↦ m • x2) = fun x2 ↦ 1 • x2

Tactic:
Set.eq_univ_iff_forall

Goal state after:
α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ (∀ (x : α), x ∈ fixedBy α m) ↔ (fun x2 ↦ m • x2) = fun x2 ↦ 1 • x2
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inl.ha
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Subsingleton A
⊢ ¬IsAlgebraic (↥(adjoin R s)) a

pp: case inl.hb
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Subsingleton A
⊢ ¬IsAlgebraic (↥(adjoin R t)) a

Tactic:
<;>

Goal state after:
case inl.ha
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Subsingleton A
⊢ ¬IsAlgebraic (↥(adjoin R s)) a

case inl.hb
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
s t : Set A
a : A
h : (matroid R A).IsBasis s t
h✝ : Subsingleton A
⊢ ¬IsAlgebraic (↥(adjoin R t)) a
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case left
F : Type u
inst✝ : Field F
⊢ Subsingleton (Emb F F)

pp: case right
F : Type u
inst✝ : Field F
⊢ Nonempty (Emb F F)

Tactic:
<;>

Goal state after:
case left
F : Type u
inst✝ : Field F
⊢ Subsingleton (Emb F F)

case right
F : Type u
inst✝ : Field F
⊢ Nonempty (Emb F F)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable

Tactic:
classical
  simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rfl

Goal state after: