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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
heC₁ : e ∈ C₁
heC₂ : e ∈ C₂
hfC₁ : f ∈ C₁
hfC₂ : f ∉ C₂
C : Set α
hCs : C ⊆ (C₁ ∪ ⋃ i, C₂) \ range fun i ↦ e
hC : M.IsCircuit C
hfC : f ∈ C
⊢ {e} ⊆ range fun i ↦ e

Tactic:
simp

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

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ (M ↾ X).cRank ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ

Tactic:
cRank_le_iff,

Goal state after:
α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ (∀ ⦃B : Set α⦄, (M ↾ X).IsBase B → #↑B ≤ κ) ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α✝ : Type u_1
M✝ : Matroid α✝
e✝ : α✝
α : Type u_1
M : Matroid α
e : α
R : Set α
hRE : R ⊆ M.E
heR : e ∈ R
⊢ e ∉ R \ {e}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
⊢ ∅ ⊆ Y ∧ ∅.Finite ∧ ∅ ⊆ M.closure ∅

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
inst✝ : M.Loopless
hI : ∅.Subsingleton
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
x✝ : ∃ x ∈ M.E, M.IsLoop x
e : α
left✝ : e ∈ M.E
he : M.IsLoop e
⊢ {e}.Subsingleton

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
⊢ M.cRk (M.closure X) = M.cRk X

Tactic:
← hI.isBasis_closure_right.cardinalMk_eq_cRk,

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X I : Set α
hI : M.IsBasis' I X
⊢ #↑I = M.cRk X
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y : Set α
⊢ M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ↾ {e | (M ↾ univ).IsNonloop e} = M ↾ {e | M.IsNonloop e}

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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 α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
a : α
ha : a ∈ B' \ B
⊢ ∃ S, Finite ↑S ∧ S ⊆ B ∧ ¬N.Indep (insert a S)

Tactic:
have := (hB.insert_dep ⟨hB'.subset_ground ha.1, ha.2⟩).1

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'
h : Infinite ↑(B' \ B)
a : α
ha : a ∈ B' \ B
this : ¬N.Indep (insert a B)
⊢ ∃ S, Finite ↑S ∧ S ⊆ B ∧ ¬N.Indep (insert a S)
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 α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
this : B \ B' ⊆ U
⊢ ℵ₀ ≤ #↑(B' \ B)

Tactic:
simp

Goal state after:
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 α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
this : B \ B' ⊆ U
e : ↑(B' \ B)
⊢ ℵ₀ ≤ #↑(B' \ B)

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_2
M : Matroid α
ι : Sort u_3
hι : Nonempty ι
Is : ι → Set α
h : M.Indep (⋃ i, Is i)
⊢ ⋂ i, M.closure (Is i) = ⋂ J ∈ range Is, M.closure J

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
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:
simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.closure (bif i then I else J) = bif i then M.closure I else M.closure J

Tactic:
simp

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 : AlgebraicIndependent R x
a✝ : ι
⊢ (Finsupp.linearCombination R x ∘ₗ Finsupp.lsingle a✝) 1 =
    (((aeval x).toLinearMap ∘ₗ Finsupp.linearCombination R X) ∘ₗ Finsupp.lsingle a✝) 1

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋃ i ∈ A, X i ∩ I ⊆ I

Tactic:
simp

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

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

Tactic:
by
  rw [hI.inter_isBasis_closure_iff_subset_closure_inter] at h ⊢
  exact (M.closure_subset_closure_of_subset_closure h).trans (M.closure_subset_closure
    (inter_subset_inter_left _ (h.trans (M.closure_subset_closure inter_subset_left))))

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

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

Tactic:
isBasis_iff_indep_closure,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.Indep ∅ ∧ X ⊆ M.closure ∅ ∧ ∅ ⊆ X ↔ X ⊆ M.closure ∅
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
x : A
⊢ AlgebraicIndependent R ![x] ↔ Transcendental R x

Tactic:
simp

Goal state after:
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
inst✝ : Algebra.Transcendental R A
x : A
hx : Transcendental R x
⊢ 1 ≤ Cardinal.mk ↑↑⟨{x}, ⋯⟩

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 ι
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
⊢ t ∩ s ∪ ∅ ⊆ s

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
nth_rw 2 [show I = insert e (I \ {e}) by simp [heI]]

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))
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✝ : Subsingleton R
this : Subsingleton A
⊢ 1 ≤ Cardinal.mk ↑↑⟨{0}, ⋯⟩

Tactic:
simp

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
ι' : 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:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : I ⊆ M.E
h : ∀ ⦃J : Set α⦄, J ⊂ I → M.closure J ⊂ M.closure I
e : α
heI : e ∈ I
hecl : e ∈ M.closure (I \ {e})
⊢ M.closure (insert e (I \ {e}) \ {e}) = M.closure (M.closure (I \ {e}))

Tactic:
simp

Goal state after:
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
x : ↥Rx
⊢ (algebraMap (↥Rx) A) x = ↑(e (e.symm (↑(Subalgebra.inclusion ⋯) x)))

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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
⊢ AlgebraicIndependent R Subtype.val ↔ Injective ⇑(algebraMap R A)

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

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

Tactic:
simp

Goal state after:
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
s : Set A
H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val
p : MvPolynomial A R
hp : p ∈ supported R s
⊢ p ∈ supported R ↑p.vars

Tactic:
simp

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

Goal state before:
pp: case e_6
ι : 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
r : R
⊢ ↑(hx.aevalEquiv (C r)) = ↑((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
simp

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 : AlgebraicIndependent R x
r : R
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (C r) = Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.AlgebraicClosure

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ algebraicClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ x ∈ g⁻¹ • s ↔ x ∈ s

Tactic:
Set.mem_inv_smul_set_iff

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ g • x ∈ s ↔ x ∈ s
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

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

Tactic:
Set.mem_inv_smul_set_iff

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
⊢ g • a ∈ s ↔ a ∈ 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
i : AlgebraicIndependent R x
p : ∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndepOn R _root_.id w
h : range x ⊆ w
x✝ : ι
⊢ (Subtype.val ∘ fun i ↦ ⟨x i, ⋯⟩) x✝ = x x✝

Tactic:
simp

Goal state after:
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 ∈ (fixedBy α g)ᶜ

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 ∈ (fixedBy α g)ᶜ

Tactic:
· exact a_moved

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 ∈ (fixedBy α g)ᶜ
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case e'_7
ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
a✝ : Nontrivial R
this : Unique ι
x✝ : PUnit.{1}
m✝ : PUnit.{1} →₀ ℕ
⊢ coeff m✝ ((⇑(uniqueAlgEquiv R PUnit.{1}).symm ∘ (fun x ↦ Polynomial.X) ∘ ⇑(Equiv.equivPUnit ι).symm) x✝) =
    coeff m✝ (X x✝)

Tactic:
simp

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

Goal state before:
pp: case refine_3
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝³ : Nontrivial S
this✝² : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this✝¹ : Algebra.IsAlgebraic (↥Sy) A
x✝² : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rxy) (↥Sy) A
this : IsScalarTower ↥Rx ↥Rxy ↥Sy
x✝¹ : ↥Sy
a : A
ha : a ∈ Sy
x✝ : S
⊢ IsAlgebraic ↥Rx ⟨(algebraMap S A) x✝, ⋯⟩

Tactic:
exact (hx.isAlgebraic.1 _).algHom (IsScalarTower.toAlgHom Rx S Sy)

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✝ : IsDomain A
s : Set A
⊢ (matroid R A).closure s = univ ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A

Tactic:
eq_univ_iff_forall,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s : Set A
⊢ (∀ (x : A), x ∈ (matroid R A).closure s) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsDomain R
fin : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
surj : Surjective ⇑f
⊢ lift.{v, u_1} (trdeg R (MvPolynomial (Fin n) R)) < lift.{u_1, v} ℵ₀

Tactic:
simp

Goal state after:
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✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
fin : trdeg R A < ℵ₀
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
⊢ lift.{u, w} ℵ₀ = lift.{w, u} ℵ₀

Tactic:
simp

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

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Nontrivial R
inst✝¹ : NoZeroDivisors A
inst✝ : Finite ι
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
⊢ lift.{w, u} #ι < lift.{u, w} ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : F
⊢ ((algebraMap F E).comp ↑(RingEquiv.refl F)) x✝ = ((↑topEquiv.toRingEquiv).comp (algebraMap F ↥⊤)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ Fintype.card ↑↑(f.aroots f.SplittingField).toFinset = f.natDegree

Tactic:
Finset.coe_sort_coe,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ Fintype.card ↥(f.aroots f.SplittingField).toFinset = f.natDegree
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {x y : Set G}, x ∈ {{1}} → y ∈ {{1}} → ∃ z ∈ {{1}}, z ⊆ x ∩ y

Tactic:
simp

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

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → 1 ∈ U

Tactic:
simp

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

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V * V ⊆ U

Tactic:
simp

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

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U

Tactic:
simp

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

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ ∀ (x₀ : G) {U : Set G}, U ∈ {{1}} → ∃ V ∈ {{1}}, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
⊢ Nat.card Gal(E/F) = finrank F E

Tactic:
let iso : F⟮α⟯ ≃ₐ[F] E :=
    { toFun := fun e => e.val
      invFun := fun e => ⟨e, by rw [hα]; exact IntermediateField.mem_top⟩
      map_mul' := fun _ _ => rfl
      map_add' := fun _ _ => rfl
      commutes' := fun _ => rfl }

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e ↦ ↑e, invFun := fun e ↦ ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
⊢ Nat.card Gal(E/F) = finrank F E
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Tactic:
rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
    (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
    add_eq_left, natSepDegree_eq_zero_iff] at h

Goal state after:
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : c.natDegree = 0
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x✝ : E
⊢ x✝ ∈ fixedField ⊥ ↔ x✝ ∈ ⊤

Tactic:
simp

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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ separableClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
simp

Goal state after: