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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (insert (f e) (f '' B)) ∧ insert (f e) (f '' B) ⊆ range f
⊢ False

Tactic:
← image_insert_eq

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
e : α
hfe : f e ∉ f '' B
hi : N.Indep (f '' insert e B) ∧ f '' insert e B ⊆ range f
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)

Tactic:
obtain ⟨x, hx, hxI⟩ := hI.augment hJ (by simpa [encard_eq_coe_toFinset_card])

Goal state after:
α : Type u_1
M : Matroid α
I J : Finset α
hI : M.Indep ↑I
hJ : M.Indep ↑J
hIJ : I.card < J.card
x : α
hx : x ∈ ↑J \ ↑I
hxI : M.Indep (insert x ↑I)
⊢ ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (I ∪ J)

Tactic:
closure_union_congr_left hI.closure_eq_closure,

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hY : M.IsRkFinite Y
I : Set α
hI : M.IsBasis' I X
hIfin : I.Finite
J : Set α
hJ : M.IsBasis' J Y
hJfin : J.Finite
⊢ (X ∪ Y) ∩ M.E ⊆ M.closure (X ∪ J)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' I)
⊢ M.Indep (Subtype.val '' ⇑f ⁻¹' ⇑f '' I) ∧ ∃ t, ⇑f '' t = ⇑f '' I

Tactic:
rw [preimage_image_eq _ f.injective]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set ↑M.E
hI : M.Indep (Subtype.val '' I)
⊢ M.Indep (Subtype.val '' I) ∧ ∃ t, ⇑f '' t = ⇑f '' I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f ⁻¹' ⇑f '' I) ∧ ⇑f '' I ⊆ range ⇑f

Tactic:
rw [preimage_image_eq _ f.injective]

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I : Set α
hI : M.Indep I
⊢ M.Indep I ∧ ⇑f '' I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase (⇑f ⁻¹' ⇑f '' B) ∧ ⇑f '' B ⊆ range ⇑f

Tactic:
rw [preimage_image_eq _ f.injective]

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
B : Set α
hB : M.IsBase B
⊢ M.IsBase B ∧ ⇑f '' B ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
⊢ M.IsCircuit (M.fundCircuit e I)

Tactic:
have aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I := sInter_subset_of_mem (by simpa)
  rw [fundCircuit_eq_sInter hecl]
  refine (hI.subset aux).insert_isCircuit_of_forall ?_ ?_ ?_
  · simp [show ∃ x ⊆ I, e ∈ M.closure x ∧ e ∉ x from ⟨I, by simp [hecl, heI]⟩]
  · rw [hI.closure_sInter_eq_biInter_closure_of_forall_subset ⟨I, by simpa⟩ (by simp +contextual)]
    simp
  simp only [mem_sInter, mem_ofPred_eq, and_imp]
  exact fun f hf hecl ↦ (hf _ (sdiff_subset.trans aux) hecl).2 rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ↪ β
I X : Set β
⊢ (M.mapEmbedding f).IsBasis I X ↔ M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ range ⇑f

Tactic:
by
  rw [mapEmbedding, map_isBasis_iff']
  refine ⟨?_, fun ⟨hb, hIX, hX⟩ ↦ ?_⟩
  · rintro ⟨I, X, hIX, rfl, rfl⟩
    simp [preimage_image_eq _ f.injective, image_mono hIX.subset, hIX]
  obtain ⟨X, rfl⟩ := subset_range_iff_exists_image_eq.1 hX
  obtain ⟨I, -, rfl⟩ := subset_image_iff.1 hIX
  exact ⟨I, X, by simpa [preimage_image_eq _ f.injective] using hb⟩

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 β
E X I : Set α
M : Matroid α
inst✝ : M.RankPos
B : Set ↑M.E
hB : (M.restrictSubtype M.E).IsBase B
hB' : M.IsBase (Subtype.val '' B)
⊢ B.Nonempty

Tactic:
by simpa using hB'.nonempty

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
hNM : N ≤r M
⊢ N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e

Tactic:
by
  obtain ⟨R, hR, rfl⟩ := hNM
  simp only [restrict_isLoop_iff, restrict_ground_eq, and_congr_right_iff, or_iff_left_iff_imp]
  exact fun heR heE ↦ (heE (hR heR)).elim

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
R : Set α
⊢ (M ↾ R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R

Tactic:
rw [← indep_singleton, restrict_indep_iff, singleton_subset_iff, indep_singleton]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : M.IsLoop e
⊢ M✶.IsColoop e

Tactic:
rwa [IsColoop, dual_dual]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
⊢ M.IsBasis' I X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X

Tactic:
by
  refine ⟨fun h ↦ ⟨h.subset,h.indep, h.eRk_eq_encard.symm⟩, fun ⟨hIX, hI, hcard⟩ ↦ ?_⟩
  obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis'_of_subset hIX
  rwa [hIfin.eq_of_subset_of_encard_le hIJ (hJ.encard_eq_eRk.trans hcard.symm).le]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
⊢ M.closure univ = M.E

Tactic:
by
  rw [← closure_inter_ground, univ_inter, closure_ground]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.closure B = M.E

Tactic:
rw [← isBasis_ground_iff] at hB

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
hB : M.IsBasis B M.E
⊢ M.closure B = M.E
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X I₀ : Set α
hI₀X : I₀ ⊆ X
hfI₀ : InjOn f I₀
hIX : M.IsBasis' (f '' I₀) (f '' X)
⊢ #↑I₀ ≤ ⨆ B, #↑↑B

Tactic:
exact IsBasis'.cardinalMk_le_cRk <| comap_isBasis'_iff.2 ⟨hIX, hfI₀, hI₀X⟩

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

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

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

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (M ↾ univ).removeLoops = M.removeLoops

Tactic:
rw [removeLoops_eq_restrict, restrict_restrict_eq _ (subset_univ _), removeLoops_eq_restrict]
  simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
have := transcendental_supported_polynomial_aeval_X R (Set.notMem_empty i) hf

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
⊢ Transcendental R ((Polynomial.aeval (X i)) f)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M✶.RankPos ↔ ∃ C, M.IsCircuit C

Tactic:
rw [rankPos_iff, dual_isBase_iff, sdiff_empty, not_iff_comm, not_exists,
    ← ground_indep_iff_isBase, indep_iff_forall_subset_not_isCircuit]
  exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩

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

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

Tactic:
rw [Transcendental] at h
    contrapose h
    refine isAlgebraic_algebraMap (⟨Polynomial.aeval (X i) f, ?_⟩ : supported R s)
    exact Algebra.adjoin_mono (Set.singleton_subset_iff.2 (Set.mem_image_of_mem _ h))
      (Polynomial.aeval_mem_adjoin_singleton _ _)

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
obtain ⟨B, hB⟩ := M.exists_isBasis S

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
⊢ ∃ B, M.IsBase B ∧ B ⊆ S
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
rw [spanning_iff_exists_isBase_subset', and_iff_left hS]

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

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

Tactic:
intro s hs hs'

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

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α),
    f x ∈ M.E →
      (M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔
        M.Indep (insert (f x) (f '' I)) → ∃ x_1 ∈ I, f x_1 = f x)

Tactic:
← image_insert_eq

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α),
    f x ∈ M.E →
      (M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ (∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e) →
    (∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e

Tactic:
rintro ⟨x, ⟨hxE, hxi⟩, rfl⟩

Goal state after:
case mpr
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
hxi : M.Indep (insert x I) → x ∈ I
⊢ (∃ x_1 ∈ M.E, f x_1 = f x) ∧ ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).closure S = R ∧ S ⊆ R ↔ R ⊆ M.closure S

Tactic:
and_iff_left hSR,

Goal state after:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : R ⊆ M.E
⊢ (M ↾ R).closure S = R ↔ R ⊆ M.closure S
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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 S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝¹ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rt) (↥St) A
this✝ : NoZeroDivisors ↥St
this : NoZeroDivisors ↥Rt
x✝ : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic ↥Rt ⟨y, hy⟩

Tactic:
← isAlgebraic_algHom_iff (IsScalarTower.toAlgHom Rt St A) Subtype.val_injective

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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 S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝¹ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rt) (↥St) A
this✝ : NoZeroDivisors ↥St
this : NoZeroDivisors ↥Rt
x✝ : ↥St
y : A
hy : y ∈ St
⊢ IsAlgebraic (↥Rt) ((IsScalarTower.toAlgHom (↥Rt) (↥St) A) ⟨y, hy⟩)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case refine_1
ι : 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
i : ι'
⊢ IsAlgebraic ↥Rxy ⟨y i, ⋯⟩

Tactic:
exact isAlgebraic_algebraMap (⟨y i, subset_adjoin ⟨i, rfl⟩⟩ : Rxy)

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

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → 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
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
B : Set A
⊢ IsTranscendenceBasis R Subtype.val ↔ (indepMatroid R A).matroid.IsBase B

Tactic:
simp_rw [Matroid.isBase_iff_maximal_indep, isTranscendenceBasis_iff_maximal]

Goal state after:
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → 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
inst✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
B : Set A
⊢ Maximal (AlgebraicIndepOn R _root_.id) B ↔ Maximal (indepMatroid R A).matroid.Indep B
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 B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔ x ∈ algebraicClosure (↥(adjoin R s)) A

Tactic:
mem_algebraicClosure,

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 B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A), (∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔ IsAlgebraic (↥(adjoin R s)) x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case refine_1
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
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
eq : ↑S = s
a : A
h : IsAlgebraic (↥S) a
⊢ a ∈ s

pp: case refine_2
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
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
⊢ (∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s) → ↑S = s

Tactic:
· rw [← eq]; exact h.restrictScalars (adjoin R s)

Goal state after:
case refine_2
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
S : Subalgebra (↥(adjoin R s)) A := algebraicClosure (↥(adjoin R s)) A
⊢ (∃ S, ↑S = s ∧ ∀ (a : A), IsAlgebraic (↥S) a → a ∈ s) → ↑S = s
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
⊢ (∀ (x : A), x ∈ algebraicClosure (↥(adjoin R s)) A) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A

Tactic:
mem_algebraicClosure,

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), IsAlgebraic (↥(adjoin R s)) x) ↔ Algebra.IsAlgebraic (↥(adjoin R s)) A
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
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
⊢ ϕ • ↑x * ϕ • ↑y = ↑x * ↑y

Tactic:
show ϕ • (x : E) = ↑x from ϕ.2 x,

Goal state after:
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
x : ↥K
y : ↥(fixedField K.fixingSubgroup)
ϕ : ↥K.fixingSubgroup
⊢ ↑x * ϕ • ↑y = ↑x * ↑y
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
⊢ IsOpen ↑⊤.fixingSubgroup

Tactic:
exact IntermediateField.fixingSubgroup_isOpen ⊤

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) • 1 +
      ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
refine add_mem ?_ ?_

Goal state after:
case succ.refine_1
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ (minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) • 1 ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

case succ.refine_2
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥L) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
y : K
hy : y ∈ ↑L'.toIntermediateField
⊢ ↑(((restrictNormalHom ↥L'.toIntermediateField) h) ⟨y, hy⟩) =
    ↑(((restrictNormalHom ↥L'.toIntermediateField) σ) ⟨y, hy⟩)

Tactic:
rw [eq]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
⊢ C ((algebraMap R K) c) * C ((algebraMap R K) d) * (a * b) = C ((algebraMap R K) c) * a * (C ((algebraMap R K) d) * b)

Tactic:
ring

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

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
⊢ (∀ (x : E), (minpoly F x).natSepDegree = 1) ↔
    ∀ (x : E), ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow q

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

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : finSepDegree F ↥F⟮x⟯ * finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range

Tactic:
mul_eq_one,

Goal state after:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : finSepDegree F ↥F⟮x⟯ = 1 ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
inst✝⁶ : Group G
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
inst✝² : MulSemiringAction G B
hG : IsGaloisGroup G A B
inst✝¹ : CommSemiring A'
inst✝ : Algebra A' B
e : A →+* A'
he : ∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a
he' : Function.Surjective ⇑e
⊢ ∀ (m : G) (n : A') (a : B), m • n • a = n • m • a

Tactic:
intro g a' b
    obtain ⟨a, rfl⟩ : ∃ a, e a = a' := he' a'
    rw [Algebra.smul_def, Algebra.smul_def, he, ← Algebra.smul_def, ← Algebra.smul_def]
    exact hG.commutes.smul_comm g a b

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Tactic:
dsimp [valMinAbs]
    rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm, Int.natCast_add,
      Nat.cast_one]

Goal state after: