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

Goal state before:
pp: α✝ α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ {e} ⊆ M.E

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ ⋂₀ {F | M.IsFlat F ∧ X ∩ (M.E ∩ M.E) ⊆ F} = ⋂₀ {F | M.IsFlat F ∧ X ∩ M.E ⊆ F}

Tactic:
inter_self

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

Goal state before:
pp: α✝ α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_5_iff_6 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
he : e ∈ M.E
⊢ {e} ⊆ M✶.E

Tactic:
simpa

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
x✝ : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
⊢ M.eRk X = 1

Tactic:
rw [← he.eRk_eq]

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
x✝ : ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
e : α
heX : e ∈ X
he : M.IsNonloop e
hXe : X ⊆ M.closure {e}
⊢ M.eRk X = M.eRk {e}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
F : Set α
hF : M.IsFlat F
⊢ F ∈ {F_1 | M.IsFlat F_1 ∧ F ∩ M.E ⊆ F_1}

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
⊢ emptyOn α = loopyOn ∅

Tactic:
loopyOn_empty

Goal state after:
α : Type u_2
⊢ emptyOn α = emptyOn α
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₂
⊢ ∀ (i : Unit), M.IsCircuit C₂

Tactic:
simpa

Goal state after:
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₂
⊢ ∀ (i : Unit), e ∈ C₁

Tactic:
simpa

Goal state after:
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₂
⊢ ∀ (i : Unit), e ∈ C₂

Tactic:
simpa

Goal state after:
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₂
⊢ f ∈ C₁

Tactic:
simpa

Goal state after:
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₂
⊢ ∀ (i : Unit), f ∉ C₂

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
e : α
x✝ : e ∈ M.closure (M.closure X ∪ K) \ (M.closure X ∪ K)
hecl : e ∈ M.closure (M.closure X ∪ K)
he : e ∉ M.closure X ∪ K
C : Set α
hCss : C ⊆ insert e (M.closure X)
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ M.closure X

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ {e} ⊆ M.coloops

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X K : Set α
hXK : Disjoint X K
hK : K ⊆ M.coloops
⊢ Disjoint (M.closure X) K

Tactic:
rwa [disjoint_iff_inter_eq_empty, closure_inter_eq_of_subset_coloops X hK,
    ← disjoint_iff_inter_eq_empty]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ {x} ⊆ I

Tactic:
simpa

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

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

Tactic:
← h.closure_eq_closure

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∈ X
J : Set α
hJ : M.IsBasis J {e}
⊢ {e} ⊆ X

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
inst✝ : M.Finitary
he : e ∈ M.closure X
heY : e ∉ X
C : Set α
hCs : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ X

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
⊢ M.removeLoops.IsNonloop e

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
hNM : M ↾ R ≤r M
inst✝ : (M ↾ R).Loopless
⊢ M ↾ R ≤r M.removeLoops

Tactic:
exact IsRestriction.of_subset M fun e heR ↦ ((M ↾ R).isNonloop_of_loopless heR).of_restrict

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

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ #↑Ii + M.cRk (IX ∪ IY) ≤ #↑(IX ∪ IY) + #↑(IX ∩ IY)

Tactic:
add_comm

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.cRk (IX ∪ IY) + #↑Ii ≤ #↑(IX ∪ IY) + #↑(IX ∩ IY)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ Disjoint C K ∨ (C ∩ K).Nontrivial

Tactic:
or_iff_not_imp_left,

Goal state after:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ ¬Disjoint C K → (C ∩ K).Nontrivial
Module: Mathlib.Combinatorics.Matroid.Closure

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

pp: case inr
α : Type u_2
M : Matroid α
Js : Set (Set α)
hne : Js.Nonempty
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.closure i
he' : M.Indep (insert e (⋂₀ Js))
J : Set α
heJ : insert e (⋂₀ Js) ⊆ J
f : α
hI : M.Indep (insert f (J \ {e}))
hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})
hiX : ⋂₀ Js ⊆ insert f (J \ {e})
heEI : e ∈ M.E \ insert f (J \ {e})
hJI : M.IsBasis J (insert e (insert f (J \ {e})))
hIb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
hfIJ : f ∈ insert f (J \ {e}) \ J
hfb : M.IsBasis (insert f (J \ {e})) (insert e (insert f (J \ {e})))
X : Set α
hX' : X ∈ Js
hfX : f ∉ X
heX : e ∈ X
⊢ False

Tactic:
· refine (hJI.indep.subset (insert_subset (heJ (mem_insert _ _)) ?_)).not_dep hd
    specialize hIs _ hX'
    rw [← singleton_union, ← sdiff_subset_iff, sdiff_singleton_eq_self hfX] at hIs
    exact hIs.trans sdiff_subset

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

Goal state before:
pp: α : 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
⊢ Indep ?m.39 (⋃ i, I ↑i)

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: 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)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ C x✝¹ = C x✝

Tactic:
simp_rw [← MvPolynomial.algebraMap_eq]

Goal state after:
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)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ (algebraMap R (MvPolynomial σ R)) x✝¹ = (algebraMap R (MvPolynomial σ R)) x✝
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Sort u_3
I : Set α
inst✝ : Nonempty ι
Js : ι → Set α
hI : M.Indep I
hJs : ∀ (i : ι), Js i ⊆ I
⊢ ⋃ i, Js i ⊆ I

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M✶.fundCircuit f (M✶.E \ B)
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∉ M✶.E

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB'✝ : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
hB' : M.IsBase (M.E \ (insert f (M✶.E \ B) \ {e}))
⊢ {e} ⊆ M.E

Tactic:
simpa

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 ι
i : ι
hs : AlgebraicIndepOn R x s
hi : Transcendental (↥(adjoin R (x '' s))) (x i)
⊢ AlgebraicIndepOn R x (insert i s)

Tactic:
nontriviality R
  have := hs.algebraMap_injective.nontrivial
  exact (insert_iff fun h ↦ hi <| isAlgebraic_algebraMap
    (⟨_, subset_adjoin ⟨i, h, rfl⟩⟩ : adjoin R (x '' s))).mpr ⟨hs, hi⟩

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ I
⊢ I \ {e} ⊂ I

Tactic:
simpa

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

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

Tactic:
or_iff_not_imp_left,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
hfE : f ∈ M.E
heE : e ∈ M.E
I : Set α
hef : e ∈ M.closure (insert f I)
he : M.Indep (insert e I) ∧ e ∉ I
hI : M.IsBasis I (X ∩ M.E)
⊢ ¬M.Dep (insert f (insert e I)) → f ∈ insert e I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
⊢ M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y) ∪ X ∩ Y)

Tactic:
union_eq_self_of_subset_right (inter_subset_right.trans h),

Goal state after:
α : Type u_2
M : Matroid α
X Y : Set α
h : Y ⊆ M.closure (X \ Y)
⊢ M.closure ((X \ Y ∪ X ∩ Y) \ Y) = M.closure (M.closure (X \ Y))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
h : e ∈ M.closure (X \ {e})
⊢ {e} ⊆ M.closure (X \ {e})

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e : α
he : e ∈ X
heE : e ∈ M.E
⊢ {e} ⊆ X

Tactic:
simpa

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning (M.closure S) ↔ M.Spanning S

Tactic:
spanning_iff_closure_eq,

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

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

Tactic:
spanning_iff_closure_eq,

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.Spanning S ↔ M.closure S ⊂ M.E

Tactic:
spanning_iff_closure_eq,

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.Spanning I ↔ M.Spanning X

Tactic:
spanning_iff_closure_eq,

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.closure I = M.E ↔ M.Spanning X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.closure I = M.E ↔ M.Spanning X

Tactic:
spanning_iff_closure_eq,

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hIX : M.IsBasis I X
⊢ M.closure I = M.E ↔ M.closure X = M.E
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
refine ⟨fun h ↦ ext_closure ?_, fun h ↦ by rw [h, loopyOn_closure_eq, loopyOn_ground]⟩
  refine fun X ↦ subset_antisymm (by simp [closure_subset_ground]) ?_
  rw [loopyOn_closure_eq, ← h]
  exact M.closure_mono (empty_subset _)

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

Tactic:
hx.mvPolynomialOptionEquivPolynomialAdjoin_C,

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) (Polynomial.C ((algebraMap R ↥(adjoin R (range x))) r)) = (aeval fun o ↦ o.elim a x) (C r)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2.none
ι : 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
⊢ a = none.elim a x

Tactic:
Option.elim

Goal state after:
case refine_2.none
ι : 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
⊢ a = a
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: case refine_2.some
ι : 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 : ι
⊢ x i = (some i).elim a x

Tactic:
Option.elim

Goal state after:
case refine_2.some
ι : 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 : ι
⊢ x i = x i
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
hx : IsTranscendenceBasis R x
b : ι
ai : AlgebraicIndependent R fun o ↦ o.elim (x b) x
h₁ : range x ⊆ range fun o ↦ o.elim (x b) x
h : range x = range fun o ↦ o.elim (x b) x
this : some b = none
⊢ False

Tactic:
simpa

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

Goal state before:
pp: ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (range x))) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F (range x))) E

Tactic:
set S := range x

Goal state after:
ι : Type u
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : IsTranscendenceBasis F x
S : Set E := range x
this : Algebra.IsAlgebraic (↥(adjoin F S)) E
⊢ Algebra.IsAlgebraic (↥(IntermediateField.adjoin F S)) E
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
S : Type v
inst✝¹ : CommRing S
inst✝ : IsDomain S
⊢ trdeg S (MvPolynomial ι S) = lift.{v, u} #ι

Tactic:
have := (IsTranscendenceBasis.mvPolynomial ι S).lift_cardinalMk_eq_trdeg.symm
  rwa [lift_id', ← lift_lift.{u}, lift_id] at this

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

Goal state before:
pp: case inr.inl
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
eq : v i = v j
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

pp: case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
· classical
    convert!
      H₁.comp_equiv <|
        .symm <|
          ((Equiv.swap j i).image s).trans <|
            .setCongr <| Equiv.image_swap_of_mem_of_notMem hj hi with
      ⟨x, rfl | hxi, hxj⟩
    · simp [eq]
    · simp [Equiv.swap_apply_of_ne_of_ne hxj (ne_of_mem_of_not_mem hxi hi)]

Goal state after:
case inr.inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj✝ : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
ne : v i ≠ v j
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)

Tactic:
basis'.tendsto_iff basis

Goal state after:
case refine_1
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ ib ∈ B, ∃ ia, (ia.1 ∈ B ∧ ia.2 ∈ B) ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this✝ : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
this : ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ (a b : G), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B, ∃ ia, (ia.1 ∈ B ∧ ia.2 ∈ B) ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib

Tactic:
simpa

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

Goal state before:
pp: case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := ⋯
this✝ : TopologicalSpace R := ⋯
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)

Tactic:
basis'.tendsto_iff basis

Goal state after:
case hmul
R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ ib ∈ B', ∃ ia, (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R✝ : Type u
inst✝¹ : Ring R✝
B✝ : RingFilterBasis R✝
R : Type u
inst✝ : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := B.toAddGroupFilterBasis
this✝¹ : TopologicalSpace R := B'.topology
basis : (𝓝 0).HasBasis (fun V ↦ V ∈ B') id
basis' : (𝓝 0 ×ˢ 𝓝 0).HasBasis (fun i ↦ i.1 ∈ B' ∧ i.2 ∈ B') fun i ↦ id i.1 ×ˢ id i.2
this✝ : IsTopologicalAddGroup R
this : ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ ib ∈ B', ∃ ia, (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun x1 x2 ↦ x1 * x2) x ∈ id ib

Tactic:
simpa

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✝
H✝ : Subgroup Gal(E✝/F)
K✝ : IntermediateField F E✝
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : IsGalois K L
H : Subgroup Gal(L/K)
hn : H.Normal
⊢ Normal K ↥(fixedField H)

Tactic:
apply normal_iff_forall_map_le'.mpr
    rintro σ x ⟨a, ha, rfl⟩ τ
    exact (symm_apply_eq σ).mp (ha ⟨σ⁻¹ * τ * σ, Subgroup.Normal.conj_mem' hn τ.1 τ.2 σ⟩)

Goal state after: