mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) • (-1) ^ ↑(i.predAbove j) • f (Matrix.vecCons (v j) (i.removeNth (j.removeNth v))) +
      (-1) ^ ↑j • f (j.removeNth v) =
    0

Tactic:
← neg_one_pow_smul_map_insertNth,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) •
        (-1) ^ ↑(i.predAbove j) • (-1) ^ ↑?p • f (insertNth ?p (v j) (i.removeNth (j.removeNth v))) +
      (-1) ^ ↑j • f (j.removeNth v) =
    0

case p
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ Fin (m + 1)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (Basis.exteriorPower n b).repr (ιMulti_family R n (⇑b) s) = Finsupp.single s 1

Tactic:
by
  ext t
  by_cases hst : s = t <;> simp [hst]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
M' : Submodule R S
h : M' ≤ M
inst✝ : Flat R ↥N
⊢ M'.LinearDisjoint N

Tactic:
by
  let i := mulMap M N ∘ₗ (inclusion h).rTensor N
  have hi : Function.Injective i := H.injective.comp <|
    Module.Flat.rTensor_preserves_injective_linearMap _ <| inclusion_injective h
  have : i = mulMap M' N := by ext; simp [i]
  exact ⟨this ▸ hi⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : ⟨↑b, ⋯⟩ = 0 ∧ ⟨↑a, ⋯⟩ = 0
⊢ False

Tactic:
repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hn

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝¹ : Nontrivial R
inst✝ : Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h : LinearIndependent R ![a, b]
m : Fin 2 → ↥M := ⇑(inclusion ⋯) ∘ ![a, b]
hm : LinearIndependent R m
this : AddCommGroup (Fin 2 →₀ ↥N) := Finsupp.instAddCommGroup
n : Fin 2 →₀ ↥N := Finsupp.single 0 ⟨↑b, ⋯⟩ - Finsupp.single 1 ⟨↑a, ⋯⟩
hn : b = 0 ∧ a = 0
⊢ False
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
f : (i : ι) → s i
⊢ (reindex R s e) ((tprod R) f) = (tprod R) fun i ↦ f (e.symm i)

Tactic:
dsimp [reindex]

Goal state after:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
f : (i : ι) → s i
⊢ (lift ((domDomCongrLinearEquiv' R R s (⨂[R] (i : ι₂), s (e.symm i)) e).symm (tprod R))) ((tprod R) f) =
    (tprod R) fun i ↦ f (e.symm i)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ Module.Finite R M ∧ Projective R M

Tactic:
let f : (S →₀ N) →ₗ[R] R := Finsupp.lsum R fun i ↦ e.toLinearMap ∘ₗ TensorProduct.mk R M N i.1.1

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
⊢ Module.Finite R M ∧ Projective R M
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

Tactic:
rw [← minpoly.algHom_eq _ φ.injective]

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
φ : K →ₐ[F] L
x : K
⊢ (Polynomial.map (algebraMap F L) (minpoly F (φ x))).Splits
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := ⋯
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := ⋯
β_in_Fγ : β ∈ F⟮γ⟯
⊢ F⟮α, β⟯ ≤ F⟮γ⟯

Tactic:
rw [adjoin_le_iff]

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ {α, β} ⊆ ↑F⟮γ⟯
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂

Tactic:
· rw [← normalClosure_of_normal K₂]
    exact normalClosure_mono K₁ K₂ h

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
⊢ AlgebraicIndependent R x

Tactic:
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
  rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv
  exact hfv.of_comp

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ ≤ F⟮α + x • β⟯

Tactic:
rw [adjoin_le_iff]

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
K : IntermediateField F E
⊢ ∃ α, F⟮α⟯ = K

Tactic:
have := FiniteDimensional.of_finite_intermediateField F E
  rcases finite_or_infinite F with (_ | _)
  · obtain ⟨α, h⟩ := exists_primitive_element_of_finite_bot F K
    exact ⟨α, by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h⟩
  · apply induction_on_adjoin (fun K ↦ ∃ α : E, F⟮α⟯ = K) ⟨0, adjoin_zero⟩
    rintro K β ⟨α, rfl⟩
    simp_rw [adjoin_simple_adjoin_simple, eq_comm]
    exact primitive_element_inf_aux_of_finite_intermediateField F α β

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

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∃ B, IsBase B

Tactic:
hB

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∃ B, M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), IsBase B → B ⊆ M.E

Tactic:
hB

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), M.IsBase B → B ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBasis I X

Tactic:
rwa [isBasis_restrict_iff, and_iff_left (show X ⊆ R from hX)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : SurjOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ InjOn f B ∧ B ⊆ E

Tactic:
by
  simp_rw [comapOn_isBase_iff, and_congr_left_iff, and_imp, isBasis'_iff_isBasis_inter_ground,
    inter_eq_self_of_subset_right h, isBasis_ground_iff, implies_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
⊢ ∃ M_1, range ⇑f = M_1.E ∧ ∀ (I : Set β), M_1.Indep I ↔ M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
obtain (rfl | ⟨⟨e, he⟩⟩) := eq_emptyOn_or_nonempty M
    · refine ⟨emptyOn β, ?_⟩
      simp only [emptyOn_ground] at f
      simp [range_eq_empty f, subset_empty_iff]
    have _ : Nonempty M.E := ⟨⟨e,he⟩⟩
    have _ : Nonempty α := ⟨e⟩
    refine ⟨M.comapOn (range f) (fun x ↦ ↑(invFunOn f univ x)), rfl, ?_⟩
    simp_rw [comapOn_indep_iff, ← and_assoc, and_congr_left_iff, subset_range_iff_exists_image_eq]
    rintro _ ⟨I, rfl⟩
    rw [← image_image, InjOn.invFunOn_image f.injective.injOn (subset_univ _),
      preimage_image_eq _ f.injective, and_iff_left_iff_imp]
    rintro - x hx y hy
    simp only [Subtype.val_inj]
    exact (invFunOn_injOn_image f univ) (image_mono (subset_univ I) hx)
      (image_mono (subset_univ I) hy)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
⊢ B ⊆ M.E → (((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B))

Tactic:
hB

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ ((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∉ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}

pp: case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

pp: case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ f ∈ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}, e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
· simp [show ∃ x ⊆ I, e ∈ M.closure x ∧ e ∉ x from ⟨I, by simp [hecl, heI]⟩]

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ e ∈ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J})

case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ f ∈ ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J}, e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E

Tactic:
by
  rw [← hM, restrictSubtype_dual]

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
x✝ : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.closure {e}
⊢ M.eRk X ≤ 1

Tactic:
refine (M.eRk_mono he).trans ?_

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
x✝ : ∃ e ∈ M.E, X ⊆ M.closure {e}
e : α
left✝ : e ∈ M.E
he : X ⊆ M.closure {e}
⊢ M.eRk (M.closure {e}) ≤ 1
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ (M ↾ X).cRk Y = M.cRk Y

Tactic:
by
  have aux : ∀ ⦃I⦄, M.IsBasis' I Y ↔ (M ↾ X).IsBasis' I Y := by
    simp_rw [isBasis'_restrict_iff, inter_eq_self_of_subset_left hYX, iff_self_and]
    exact fun I h ↦ h.subset.trans hYX
  simp_rw [le_antisymm_iff, cRk_le_iff]
  exact ⟨fun I hI ↦ (aux.2 hI).cardinalMk_le_cRk, fun I hI ↦ (aux.1 hI).cardinalMk_le_cRk⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ M.IsCocircuit K ↔ Minimal (fun X ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
rw [isCocircuit_def, isCircuit_def, aux, iff_comm]

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ Minimal (fun X ↦ ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
    Minimal (fun X ↦ (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
ext B
  rw [isBase_iff_maximal_indep, removeLoops_indep_eq, isBase_iff_maximal_indep]

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
⊢ N.IsBase B → N.IsBase B' → #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
hB

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase B → ∀ {e f : α}, e ∈ M.fundCocircuit f B → f ∈ M.fundCircuit e B

Tactic:
hB

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ ∀ {e f : α}, e ∈ M.fundCocircuit f B → f ∈ M.fundCircuit e B
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 : ι
h : i ∉ s
⊢ AlgebraicIndependent R ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) ↔
    AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
AlgebraicIndepOn

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 ι
i : ι
h : i ∉ s
⊢ AlgebraicIndependent R ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) ↔
    (AlgebraicIndependent R fun i ↦ x ↑i) ∧ Transcendental (↥(adjoin R (x '' s))) (x i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.closure S = M.E → True

Tactic:
exact fun _ ↦ trivial

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

Goal state before:
pp: case refine_1
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBasis B S
⊢ M.IsBase B

pp: case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.closure B

Tactic:
· exact h.indep.isBase_of_spanning <| by rwa [h.spanning_iff_spanning]

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
h : M.IsBase B ∧ B ⊆ S
⊢ S ⊆ M.closure B
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)
⊢ IsTranscendenceBasis R x

Tactic:
refine ⟨(AlgHom.algebraicIndependent_iff f h).mp H.1, ?_⟩
  intro s hs hs'
  have := H.2 (f '' s)
    ((algebraicIndependent_image h.injOn).mp ((AlgHom.algebraicIndependent_iff f h).mpr hs))
    (by rw [Set.range_comp]; exact Set.image_mono hs')
  rwa [Set.range_comp, (Set.image_injective.mpr h).eq_iff] at this

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

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
by
    obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)
    rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]

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 α
a : α
g : G
⊢ g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
by
  rw [mem_fixedBy, smul_left_cancel_iff]
  rfl

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 α
inst✝ : FaithfulSMul G α
g h : G
disjoint : (fixedBy α g)ᶜ = Set.univᶜ
comm : Commute g h
⊢ g = 1

Tactic:
compl_inj_iff,

Goal state after:
α : Type u_1
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : FaithfulSMul G α
g h : G
disjoint : fixedBy α g = Set.univ
comm : Commute g h
⊢ g = 1
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

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

Tactic:
have := (nonempty_unique ι).some

Goal state after:
ι : Type u
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
a✝ : Nontrivial R
this : Unique ι
⊢ IsTranscendenceBasis R fun x ↦ Polynomial.X
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✝ : Subsingleton A
s : Set A
⊢ ∀ ⦃I X : Set A⦄, (matroid R A).IsBasis I s → (matroid R A).IsBasis I X → X ⊆ s

Tactic:
matroid_isBasis_iff_of_subsingleton

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✝ : Subsingleton A
s : Set A
⊢ ∀ ⦃I X : Set A⦄, I = s → I = X → X ⊆ s
Module: Mathlib.FieldTheory.SeparableDegree

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
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F E)

Tactic:
← (embProdEmbOfIsAlgebraic F (adjoin F (Set.range x)) E).infinite_iff

Goal state after:
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
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
⊢ Infinite (Emb F ↥(adjoin F (Set.range x)) × Emb (↥(adjoin F (Set.range x))) E)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ ((map (algebraMap E K) f).aroots (AlgebraicClosure K)).toFinset.card = (f.aroots (AlgebraicClosure K)).toFinset.card

Tactic:
aroots_def,

Goal state after:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ (map (algebraMap K (AlgebraicClosure K)) (map (algebraMap E K) f)).roots.toFinset.card =
    (map (algebraMap E (AlgebraicClosure K)) f).roots.toFinset.card
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun x ↦ X - C x) f.roots).prod
h2 : (f.aroots F).toFinset.card = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
aroots_def,

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun x ↦ X - C x) f.roots).prod
h2 : (Polynomial.map (algebraMap F F) f).roots.toFinset.card = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case adjoin_rootSet'
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
h1 : F⟮α⟯ = ⊤
⊢ α ∈ (minpoly F α).rootSet E

Tactic:
Polynomial.mem_rootSet

Goal state after:
case adjoin_rootSet'
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
h1 : F⟮α⟯ = ⊤
⊢ minpoly F α ≠ 0 ∧ (Polynomial.aeval α) (minpoly F α) = 0