mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P :=
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
m : Mₚ P
r : R
s : ↥P.primeCompl
⊢ (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun
      (IsLocalization.mk' (Rₚ P) r s • m) =
    ↑e (IsLocalization.mk' (Rₚ P) r s) •
      (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun m

Tactic:
apply ((Module.End.isUnit_iff _).mp
      (IsLocalizedModule.map_units (LocalizedModule.mkLinearMap P.primeCompl M) s)).1

Goal state after:
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P := ⋯
m : Mₚ P
r : R
s : ↥P.primeCompl
⊢ ((algebraMap R (End R (LocalizedModule P.primeCompl M))) ↑s)
      ((↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun
        (IsLocalization.mk' (Rₚ P) r s • m)) =
    ((algebraMap R (End R (LocalizedModule P.primeCompl M))) ↑s)
      (↑e (IsLocalization.mk' (Rₚ P) r s) •
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun m)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case refine_2
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsOpen[inst✝¹] ((fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {1})

Tactic:
rw [← isClosed_compl_iff]
      convert! hU.1
      ext
      simp

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₁
⊢ (if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = f ⟨x, hx⟩

Tactic:
rw [dif_pos hx]

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : H ≠ ⊥
⊢ ⁅H, H⁆ < H

Tactic:
rw [← nontrivial_iff_ne_bot] at hH
  rw [← H.range_subtype, MonoidHom.range_eq_map, ← map_commutator, map_subtype_lt_map_subtype]
  exact commutator_lt_top_of_nontrivial H

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
⊢ IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H

Tactic:
by
  refine ⟨fun _ _ ↦ IsSolvable.commutator_lt_of_ne_bot, fun h ↦ ?_⟩
  suffices h : IsSolvable (⊤ : Subgroup G) from
    isSolvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))
  induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH
  rcases eq_or_ne H ⊥ with rfl | h'
  · infer_instance
  · obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')
    use n + 1
    rw [← map_subtype_inj, Subgroup.map_bot] at hn ⊢
    rw [← hn]
    clear hn
    induction n with
    | zero =>
      rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
    | succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
p : PrimeSpectrum R
⊢ rankAtStalk M p = 0 ↔ p ∉ support R M

Tactic:
by
  rw [notMem_support_iff]
  refine ⟨fun h ↦ ?_, fun h ↦ Module.finrank_zero_of_subsingleton⟩
  apply subsingleton_of_rank_zero (R := Localization.AtPrime p.asIdeal)
  dsimp [rankAtStalk] at h
  simp [← finrank_eq_rank, h]

Goal state after:
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
h : Normal F L
⊢ Normal F ↥(normalClosure F K L)

Tactic:
by
  obtain _ | φ := isEmpty_or_nonempty (K →ₐ[F] L)
  · rw [normalClosure, iSup_of_empty]; exact Normal.of_algEquiv (botEquiv F L).symm
  · exact (isNormalClosure_normalClosure F K L).normal

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: 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⟮α, β⟯ = F⟮γ⟯

Tactic:
use γ
    apply le_antisymm
    · rw [adjoin_le_iff]
      have α_in_Fγ : α ∈ F⟮γ⟯ := by
        rw [← add_sub_cancel_right α (c • β)]
        exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)
      rintro x (rfl | rfl) <;> assumption
    · rw [adjoin_simple_le_iff]
      have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
      have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)
      exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)

Goal state after:
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
K : IntermediateField F L
inst✝ : Normal F L
f : Gal(L/F)
⊢ map (↑f) K ≤ ⨆ f, map f K

Tactic:
exact le_iSup_of_le f le_rfl

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
hF : Normal F ↥E
hE : E ≤ ⨆ i, t i
this✝ : (Polynomial.map (algebraMap F ↥E) (minpoly F x)).Splits
this : (Polynomial.map (inclusion hE).toRingHom (Polynomial.map (algebraMap F ↥E) (minpoly F x))).Splits
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits

Tactic:
rwa [Polynomial.map_map] at this

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₁.encard.toNat = B₂.ncard

Tactic:
hB₁.encard_eq_encard_of_isBase hB₂,

Goal state after:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₂.encard.toNat = B₂.ncard
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
⊢ ExchangeProperty IsBase

Tactic:
by
    simp_rw [show IsBase = M.IsBase from funext (by simp [hB])]
    exact M.isBase_exchange

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
⊢ Function.Bijective ⇑(LinearMap.mul'' R A ∘ₗ (AlgebraTensorModule.lTensor A A) (submoduleAlgebra e).subtype)

Tactic:
by
    convert! (AlgebraTensorModule.congr (.refl ..) (submoduleAlgebraEquiv e) ≪≫ₗ e).bijective
    ext x
    refine x.induction_on (by simp) ?_ (by simp +contextual)
    intro a x
    obtain ⟨m, rfl⟩ := (submoduleAlgebraEquiv e).symm.surjective x
    suffices a * toAlgebra e m = e (a ⊗ₜ[R] m) by simpa using! this
    dsimp [toAlgebra]
    rw [map_one, ← smul_eq_mul, ← map_smul, smul_tmul', smul_eq_mul, mul_one]

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
⊢ ∃ x, ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ x

Tactic:
use n

Goal state after:
case h
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
I : Set α
hI : P I
hIX : I ⊆ X
hP : ∀ (Y : Set α), P Y → ∃ n₀, Y.encard = ↑n₀ ∧ n₀ ≤ n
⊢ ∀ y ∈ ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, y ≤ n
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : M.IsBase B
⊢ M✶.IsBase (M.E \ B)

Tactic:
rwa [dual_isBase_iff, sdiff_sdiff_cancel_left h.subset_ground]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : M.Indep I
hNM : N ≤r M
hIN : I ⊆ N.E
⊢ N.Indep I

Tactic:
by
  obtain ⟨R, -, rfl⟩ := hNM; simpa [hI]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ M.IsBasis (insert y (I \ {e})) X

Tactic:
rwa [isBase_restrict_iff] at h

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 : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = f '' Subtype.val '' I₀) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
Subtype.exists_set_subtype (p := fun J ↦ M.Indep J ∧ I = f '' J)

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ s ⊆ M.E, M.Indep s ∧ I = f '' s) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : I = I'
⊢ M.IsBasis I X

Tactic:
obtain rfl := hII'

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
hI' : M.Indep I
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ M.loops = E ∧ M.E = E

Tactic:
rw [h, loops]

Goal state after:
α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ (loopyOn E).closure ∅ = E ∧ (loopyOn E).E = E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'

Tactic:
suffices hcl : z ∈ M.closure ((⋃ i, I i) ∪ (J \ {z})) by
    rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl
    obtain ⟨C', hC'ss, hC', hzC'⟩ := hcl
    refine ⟨C', ?_, hC', hzC'⟩
    rwa [union_comm, ← insert_union, insert_sdiff_singleton, insert_eq_of_mem hzJ] at hC'ss

Goal state after:
case inr
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
⊢ z ∈ M.closure ((⋃ i, I i) ∪ J \ {z})
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}

Tactic:
he.closure_eq_closure_iff_isCircuit_of_ne hne,

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ M.IsCircuit {e, f} ↔ e = f ∨ ¬M.Indep {e, f}
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

Tactic:
imp_iff_not_or

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
x : α
hI : M.Indep I
⊢ ¬M.Indep (insert x I) ∧ x ∈ M.E ∨ x ∈ I ↔ x ∈ M.E ∧ (¬M.Indep (insert x I) ∨ x ∈ I)
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 + M.cRk Y

Tactic:
← hIY.cardinalMk_eq_cRk,

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
⊢ #↑Ii + M.cRk (IX ∪ IY) ≤ #↑IX + #↑IY
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.closure (M.E \ K ∪ {e}) ⊆ M.closure (M.E \ K)

Tactic:
refine (M.closure_subset_closure (subset_union_left (t := C))).trans ?_
    rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← closure_union_congr_right
      (hC.closure_sdiff_singleton_eq e), union_eq_self_of_subset_right]
    rw [← he, sdiff_self_inter]
    exact sdiff_subset_sdiff_left hC.subset_ground

Goal state after:
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)
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

Tactic:
have := hA.coe_sort

Goal state after:
α : 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
⊢ M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)
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)
⊢ Transcendental R f

Tactic:
rw [← transcendental_polynomial_aeval_X_iff R i]
    refine h.restrictScalars fun _ _ heq ↦ MvPolynomial.C_injective σ R ?_
    simp_rw [← MvPolynomial.algebraMap_eq]
    exact congr($(heq).1)

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
⊢ ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A

Tactic:
trdeg_eq_zero_iff

Goal state after:
R : Type u_3
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ ¬Algebra.IsAlgebraic R A ↔ ¬Algebra.IsAlgebraic R A
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
hSE : S ⊆ M.E
⊢ M.Spanning S ↔ M'.Spanning S

Tactic:
rw [hsp _ hSE]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m m' : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ m')) g'
hg : g.Separable
hg' : g'.Separable
⊢ g.natDegree = g'.natDegree

Tactic:
wlog hm : m ≤ m'
  · exact (this q g' g m' m h_expand.symm hg' hg (le_of_not_ge hm)).symm
  obtain ⟨s, rfl⟩ := exists_add_of_le hm
  rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand
  subst h_expand
  rcases isUnit_or_eq_zero_of_separable_expand q s (NeZero.pos q) hg with (h | rfl)
  · rw [natDegree_expand, natDegree_eq_zero_of_isUnit h, zero_mul]
  · rw [natDegree_expand, pow_zero, mul_one]

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
hx : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{w, u} #ι = lift.{u, w} (trdeg R A)

Tactic:
← matroid_cRank_eq,

Goal state after:
ι : 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
hx : IsTranscendenceBasis R x
this : FaithfulSMul R A
⊢ lift.{w, u} #ι = lift.{u, w} (matroid R A).cRank
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
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
⊢ IsTranscendenceBasis R x

Tactic:
← matroid_cRank_eq,

Goal state after:
ι : 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
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).cRank < ℵ₀
⊢ IsTranscendenceBasis R x
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✝⁷ : Nontrivial R
A : Type v
inst✝⁶ : CommRing A
inst✝⁵ : NoZeroDivisors A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ trdeg R S + trdeg S A = trdeg R A

Tactic:
by
  rw [← (trdeg R S).lift_id, ← (trdeg S A).lift_id, ← (trdeg R A).lift_id]
  exact lift_trdeg_add_eq R S A

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X ^ 1 ^ n - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X ^ 1 ^ n - C y

Tactic:
simp_rw [one_pow, pow_one] at hf ⊢

Goal state after:
case zero
F : Type u
inst✝² : Field F
f : F[X]
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
n : ℕ
y : F
inst✝¹ : CharZero F
inst✝ : ExpChar F 1
hf : f = X - C y
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F 1).range) ∧ f = X - C y
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⟮α⟯ = ⊤
e : E
⊢ e ∈ F⟮α⟯

Tactic:
hα

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⟮α⟯ = ⊤
e : E
⊢ e ∈ ⊤
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
⊢ comap i (separableClosure F K) = separableClosure F E

Tactic:
by
  ext x
  exact map_mem_separableClosure_iff i

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
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
⊢ {s | IsTranscendenceBasis F Subtype.val}.Nonempty

Tactic:
have ⟨s, hs⟩ := IntermediateField.fg_top F E

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.EssFiniteType F E
d : Finset E → ℕ := fun s ↦ finInsepDegree (↥(adjoin F ↑s)) E
s : Finset E
hs : adjoin F ↑s = ⊤
⊢ {s | IsTranscendenceBasis F Subtype.val}.Nonempty
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (algebraMap F E) y = x ^ q ^ n
⊢ ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n

Tactic:
use n

Goal state after:
case h
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (algebraMap F E) y = x ^ q ^ n
⊢ Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n