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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I → (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

Tactic:
rintro (⟨hI, hIE⟩ | hI)

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : ¬N.Indep (f '' I)
hIE : I ⊆ f ⁻¹' N.E
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E

case inr
α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hI : N.Indep (f '' I) ∧ ¬InjOn f I
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E
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:
obtain ⟨R, -, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
R : Set α
hIN : I ⊆ (M ↾ R).E
⊢ (M ↾ R).Indep I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
h : M✶.RankPos
⊢ ¬M.IsBase M.E

Tactic:
rwa [rankPos_iff, dual_isBase_iff, sdiff_empty] at h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : M.Dep X
hNM : N ≤r M
hXE : X ⊆ N.E
⊢ N.Dep X

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
R : Set α
hXE : X ⊆ (M ↾ R).E
⊢ (M ↾ R).Dep X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
⊢ {e} ⊆ M.closure ∅

Tactic:
← closure_subset_closure_iff_subset_closure,

Goal state after:
α : Type u_1
M : Matroid α
e : α
h : M.closure {e} = M.loops ∧ e ∈ M.E
⊢ M.closure {e} ⊆ M.closure ∅
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ (M.restrictSubtype M.E).IsBase B ↔ M.IsBase (Subtype.val '' B)

Tactic:
restrictSubtype_isBase_iff,

Goal state after:
α : Type u_1
M : Matroid α
B : Set ↑M.E
⊢ M.IsBasis' (Subtype.val '' B) M.E ↔ M.IsBase (Subtype.val '' B)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).loops = M.loops ∩ R

Tactic:
by
  rw [restrict_loops_eq', sdiff_eq_empty.2 hR, union_empty]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.eRk X ≤ M.eRk Y

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ I.encard ≤ M.eRk Y
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M N : Matroid α
e : α
h : N.IsNonloop e
hNM : N ≤r M
⊢ M.IsNonloop e

Tactic:
obtain ⟨R, -, rfl⟩ := hNM

Goal state after:
α : Type u_1
M : Matroid α
e : α
R : Set α
h : (M ↾ R).IsNonloop e
⊢ M.IsNonloop e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ M.eRk X = ⊤ ↔ ¬M.IsRkFinite X

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis' I X
⊢ I.encard = ⊤ ↔ ¬M.IsRkFinite X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
hr : M.eRk Y ≤ M.eRk X
I : Set α
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
hXY : X ⊆ Y
I : Set α
hr : M.eRk Y ≤ I.encard
hI : M.IsBasis' I X
J : Set α
hJ : M.IsBasis' J Y
hIJ : I ⊆ J
⊢ M.closure X = M.closure Y
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ M.eRk (M.closure (insert e I)) = M.eRk X + 1

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
I : Set α
he : e ∈ M.E ∧ (e ∈ M.E → ¬(M.Indep (insert e I) → e ∈ I))
hI : M.IsBasis' I X
⊢ M.eRk (M.closure (insert e I)) = I.encard + 1
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
heI : e ∉ I
hC : M.IsCircuit (insert e I)
hI : M.IsBasis I (insert e I)
heC : e ∈ insert e I
⊢ M.eRk (insert e I) + 1 = (insert e I).encard

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
heI : e ∉ I
hC : M.IsCircuit (insert e I)
hI : M.IsBasis I (insert e I)
heC : e ∈ insert e I
⊢ I.encard + 1 = (insert e I).encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ M.eRk X = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}

Tactic:
hI.eRk_eq_encard,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M.IsBasis I X
⊢ I.encard = 1 → ∃ e ∈ X, M.IsNonloop e ∧ X ⊆ M.closure {e}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
h : M.eRk X ≤ 1
I : Set α
hI : M.IsBasis I X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
hI.eRk_eq_encard,

Goal state after:
case refine_1
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
I : Set α
h : I.encard ≤ 1
hI : M.IsBasis I X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
h : M.IsLoop e
⊢ ¬M✶.IsLoop e

Tactic:
rw [← dual_dual M, dual_isLoop_iff_isColoop] at h

Goal state after:
α : Type u_1
M : Matroid α
e : α
h : M✶.IsColoop e
⊢ ¬M✶.IsLoop e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
hI.eRk_eq_encard,

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

Goal state before:
pp: α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
⊢ (loopyOn Y).eRk X = 0

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
X Y I : Set α
hI : (loopyOn Y).IsBasis' I X
⊢ I.encard = 0
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : (freeOn Y).IsBasis I X
⊢ (freeOn Y).eRk X = X.encard

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
X Y : Set α
hXY : X ⊆ Y
I : Set α
hI : (freeOn Y).IsBasis I X
⊢ I.encard = X.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M✶.eRk X + (M.E \ B).encard = M.eRk (M.E \ X) + X.encard

Tactic:
hI.eRk_eq_encard,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ (B ∩ X).encard + (M.E \ B).encard = M.eRk (M.E \ X) + X.encard
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
← closure_subset_closure_iff_subset_closure,

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis I X
⊢ M.closure X ⊆ M.closure I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton
⊢ M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial

Tactic:
loopless_iff_forall_not_isLoop

Goal state after:
α : Type u_1
M : Matroid α
this : (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton
⊢ (∀ e ∈ M.E, ¬M.IsLoop e) ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
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}))
⊢ {e} ⊆ M.E

Tactic:
← he

Goal state after:
α : 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}))
⊢ C ∩ K ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(I \ J) = #↑(J \ I)

Tactic:
rw [← lift_inj.{u, v}, ← mk_image_eq_of_injOn_lift _ _ (hfI.mono sdiff_subset),
    ← mk_image_eq_of_injOn_lift _ _ (hfJ.mono sdiff_subset), lift_inj, hfI.image_sdiff,
    hfJ.image_sdiff, ← sdiff_union_sdiff_cancel inter_subset_left (image_inter_subset f I J),
    inter_comm, sdiff_inter_self_eq_sdiff, mk_union_of_disjoint, hI.cardinalMk_sdiff_comm hJ,
    ← sdiff_union_sdiff_cancel inter_subset_left (image_inter_subset f J I), inter_comm,
    sdiff_inter_self_eq_sdiff, mk_union_of_disjoint, inter_comm J I] <;>
  exact disjoint_sdiff_left.mono_right (sdiff_subset.trans inter_subset_left)

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

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

Tactic:
have hB' := hB.isBasis_closure_right

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
h : M.Spanning S
B : Set α
hB : M.IsBasis B S
hB' : M.IsBasis B (M.closure S)
⊢ ∃ B, M.IsBase B ∧ B ⊆ S
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
⊢ M.Spanning = M'.Spanning

Tactic:
ext S

Goal state after:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
S : Set α
⊢ M.Spanning S ↔ M'.Spanning S
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) → ↑s := fun x ↦ ⟨↑x, ⋯⟩
a : { x // x ∈ s }
left✝¹ : a ∈ t
hx : (Embedding.subtype fun x ↦ x ∈ s) a ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ s) t
b : { x // x ∈ s }
left✝ : b ∈ t
hy : (Embedding.subtype fun x ↦ x ∈ s) b ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ s) t
⊢ f ⟨(Embedding.subtype fun x ↦ x ∈ s) a, hx⟩ = f ⟨(Embedding.subtype fun x ↦ x ∈ s) b, hy⟩ →
    ⟨(Embedding.subtype fun x ↦ x ∈ s) a, hx⟩ = ⟨(Embedding.subtype fun x ↦ x ∈ s) b, hy⟩

Tactic:
simp only [f, imp_self, Subtype.mk_eq_mk]

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

Goal state before:
pp: ι : Type u
A : Type v
x : ι → A
inst✝⁴ : CommRing A
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ AlgebraicIndependent K x

Tactic:
rw [algebraicIndependent_empty_type_iff]

Goal state after:
ι : Type u
A : Type v
x : ι → A
inst✝⁴ : CommRing A
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ⇑(algebraMap K A)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : 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
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
this : Nontrivial R
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
← mem_algebraicClosure,

Goal state after:
ι : 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 ∈ algebraicClosure (↥(adjoin R (v '' (insert i s \ {j})))) S
this : Nontrivial R
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
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

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:
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case pos
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : σ x = y
⊢ σ (eval x (minpolyDiv R x)) = σ ((aeval x) (derivative (minpoly R x)))

Tactic:
eval_minpolyDiv_self

Goal state after:
case pos
R : Type u_3
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
y : T
σ : S →+* T
hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0
h : σ x = y
⊢ σ ((aeval x) (derivative (minpoly R x))) = σ ((aeval x) (derivative (minpoly R x)))
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
⊢ C p.leadingCoeff ∣ p

Tactic:
use minpoly R s

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
⊢ p = C p.leadingCoeff * minpoly R s
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
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K := ⋯
⊢ L ≤ M

Tactic:
rw [← fixedField_fixingSubgroup M, IntermediateField.le_iff_le]

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : IsOpen L.fixingSubgroup.carrier
S : Set Gal(K/k)
gp : Subgroup Gal(K/k)
eq : (fun g ↦ g.carrier) gp = S
M : IntermediateField k K
sub : (fun g ↦ g.carrier) M.fixingSubgroup ⊆ (↑(IntermediateFieldEquivClosedSubgroup.toFun L)).carrier
hM : M ∈ finiteExts k K
eq' : M.fixingSubgroup = gp
this : FiniteDimensional k ↥M
L' : FiniteGaloisIntermediateField k K :=
  let __src := normalClosure k (↥M) K;
  { toIntermediateField := __src, finiteDimensional := ⋯, isGalois := ⋯ }
⊢ M.fixingSubgroup ≤ L.fixingSubgroup
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 q : R[X]
hp : p.IsPrimitive
h_dvd : map (algebraMap R K) p ∣ map (algebraMap R K) q
⊢ p ∣ q

Tactic:
rcases h_dvd with ⟨r, hr⟩

Goal state after:
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 q : R[X]
hp : p.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
⊢ p ∣ q
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case inl.tmul
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
⊢ ∃ n, x ⊗ₜ[k] y ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
obtain ⟨n, a, ha⟩ := IsPurelyInseparable.pow_mem k q y

Goal state after:
case inl.tmul
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : (algebraMap k K) a = y ^ q ^ n
⊢ ∃ n, x ⊗ₜ[k] y ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ a.valMinAbs * 2 = ↑n ↔ 2 * a.val = n

Tactic:
rcases n with - | n

Goal state after:
case zero
a : ZMod 0
⊢ a.valMinAbs * 2 = ↑0 ↔ 2 * a.val = 0

case succ
n : ℕ
a : ZMod (n + 1)
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a b : ZMod n
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

Tactic:
rcases n with - | n

Goal state after:
case zero
a b : ZMod 0
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs

case succ
n : ℕ
a b : ZMod (n + 1)
⊢ (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: κ : Type w
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
⊢ traceMatrix A ⇑(b.reindex f) = (reindex f f) (traceMatrix A ⇑b)

Tactic:
ext (x y); simp

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

Goal state before:
pp: case a
a b : ℤ
⊢ ↑(a.gcd b) ∣ ↑(EuclideanDomain.gcd a b).natAbs

Tactic:
· rw [Int.dvd_natAbs]
    exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left ..) (Int.gcd_dvd_right ..)

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

Goal state before:
pp: case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
b : B
M : A[X]
a : A
ha1 : ∀ (g : G), g • (algebraMap A B) a = (algebraMap A B) a
ha2 : (algebraMap A B) a ∉ Q
hb :
  ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then (algebraMap A B) a * b₀ else 0)
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) =
      if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a * b₀)) else X
key :
  f ((algebraMap (B ⧸ Q) L) ((algebraMap (A ⧸ P) (B ⧸ Q)) ((algebraMap A (A ⧸ P)) a))) *
      f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap (B ⧸ Q) L) ((algebraMap (A ⧸ P) (B ⧸ Q)) ((algebraMap A (A ⧸ P)) a)) *
      (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)

Tactic:
← algebraMap_apply,

Goal state after:
case intro
A : Type u_1
B : Type u_2
inst✝¹⁸ : CommRing A
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Algebra A B
G : Type u_3
inst✝¹⁵ : Group G
inst✝¹⁴ : Finite G
inst✝¹³ : MulSemiringAction G B
inst✝¹² : SMulCommClass G A B
P : Ideal A
Q : Ideal B
inst✝¹¹ : Q.IsPrime
inst✝¹⁰ : Q.LiesOver P
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra (A ⧸ P) K
inst✝⁶ : Algebra (B ⧸ Q) L
inst✝⁵ : Algebra (A ⧸ P) L
inst✝⁴ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝³ : Algebra K L
inst✝² : IsScalarTower (A ⧸ P) K L
inst✝¹ : Algebra.IsInvariant A B G
inst✝ : Module.IsTorsionFree (B ⧸ Q) L
f : Gal(L/K)
val✝ : Fintype G
b₀ : B
hx :
  ∀ (g : ↥(MulAction.stabilizer G Q)),
    ((Ideal.Quotient.stabilizerHom Q P G) g) ((Ideal.Quotient.mk Q) b₀) = (Ideal.Quotient.mk Q) b₀
b : B
M : A[X]
a : A
ha1 : ∀ (g : G), g • (algebraMap A B) a = (algebraMap A B) a
ha2 : (algebraMap A B) a ∉ Q
hb :
  ∀ (g : G), (algebraMap B (B ⧸ Q)) (g • b) = (algebraMap B (B ⧸ Q)) (if g • Q = Q then (algebraMap A B) a * b₀ else 0)
key₀ :
  ∀ (g : G),
    map (algebraMap B (B ⧸ Q)) (X - C (g • b)) =
      if g • Q = Q then X - C ((algebraMap B (B ⧸ Q)) ((algebraMap A B) a * b₀)) else X
key :
  f ((algebraMap (A ⧸ P) L) ((algebraMap A (A ⧸ P)) a)) * f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) =
    (algebraMap (A ⧸ P) L) ((algebraMap A (A ⧸ P)) a) * (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)
⊢ f ((algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)) = (algebraMap (B ⧸ Q) L) ((algebraMap B (B ⧸ Q)) b₀)