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

Goal state before:
pp: α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ B ∩ X ⊆ B \ {e}

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : B' ⊆ B ∪ X ∧ e ∉ B'
f : α
hfb : f ∈ B' \ B
hBf : M.IsBase (insert f (B \ {e}))
⊢ B ∩ X ⊆ B ∧ Disjoint (B ∩ X) {e}
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
isBase_restrict_iff',

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
⊢ (N.comap f).IsBasis' B E ↔ N.IsBasis' (f '' B) (f '' E) ∧ InjOn f B ∧ B ⊆ E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal (fun x ↦ ¬M.Indep x) C

Tactic:
simp_rw [minimal_iff_forall_ssubset, and_iff_right hC.not_indep, not_not]

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
h : X ∩ M.E ⊆ M.loops
e : α
heI : e ∈ I
⊢ False

Tactic:
exact (hI.indep.isNonloop_of_mem heI).not_isLoop (h (hI.subset heI))

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure I
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X

Tactic:
← closure_inter_ground

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hXI : X ⊆ M.closure (I ∩ M.E)
hIX : I ⊆ X
hI : I.encard ≤ M.eRk X
J : Set α
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
isBasis'_iff_indep_encard_eq_of_finite hIfin

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
hX : X ⊆ M.E
⊢ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X ↔ I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure Y

Tactic:
← closure_inter_ground

Goal state after:
α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure (Y ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure X

Tactic:
← closure_inter_ground

Goal state after:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure (X ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : e ∈ M.E
⊢ e ∈ M.closure X

Tactic:
by
  rw [← closure_inter_ground]
  exact M.mem_closure_of_mem ⟨heX, h⟩

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

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

Tactic:
simpa using hJ.subset_closure

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

Goal state before:
pp: case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E \ K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
subset_sdiff,

Goal state after:
case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (∀ (x : Set α), ¬(M.IsBase x ∧ x ⊆ M.E ∧ Disjoint x K)) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.closure (B \ {e}) ⊆ M.E \ X

Tactic:
subset_sdiff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
hsp : M.IsBase (insert f (B \ {e}))
⊢ M.closure (B \ {e}) ⊆ M.E ∧ Disjoint (M.closure (B \ {e})) X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case neg.inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e})
hf : f ∉ M.E
heB : e ∈ B
⊢ M.IsBasis (insert f B \ {e}) M.E

Tactic:
← closure_inter_ground

Goal state after:
case neg.inr
α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBasis B M.E
he : e ∈ M.closure (insert f B \ {e} ∩ M.E)
hf : f ∉ M.E
heB : e ∈ B
⊢ M.IsBasis (insert f B \ {e}) M.E
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Subsingleton R
x : ι → A
⊢ IsTranscendenceBasis R x ↔ Nonempty ι

Tactic:
have := Module.subsingleton R A
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨.of_subsingleton, fun s hs hx ↦
    hx.antisymm fun a _ ↦ ⟨Classical.arbitrary _, Subsingleton.elim ..⟩⟩⟩
  by_contra! hι
  have := h.2 {0} .of_subsingleton
  simp [range_eq_empty, eq_comm (a := ∅)] at this

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure X
hef : e ∈ M.closure (insert f X)
⊢ f ∈ M.closure (insert e X)

Tactic:
← closure_inter_ground

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
⊢ f ∈ M.closure (insert e X ∩ M.E)
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
S : Type u
A : Type v
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✝² : Nontrivial R
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
x✝¹ : { s // AlgebraicIndepOn R _root_.id s }
s : Set S
hs : AlgebraicIndepOn R _root_.id s
x✝ : { s // AlgebraicIndepOn S _root_.id s }
t : Set A
ht : AlgebraicIndepOn S _root_.id t
this : AlgebraicIndependent R (Sum.elim (fun i ↦ _root_.id ↑i) (⇑(algebraMap S A) ∘ fun i ↦ _root_.id ↑i))
⊢ #(↑↑⟨t, ht⟩ ⊕ ↑↑⟨s, hs⟩) ≤
    lift.{u, v} #↑↑⟨range (Sum.elim (fun i ↦ _root_.id ↑i) (⇑(algebraMap S A) ∘ fun i ↦ _root_.id ↑i)), ⋯⟩

Tactic:
rw [← lift_umax, mk_range_eq_of_injective this.injective, lift_id']

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
hB' : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B ⊆ S

Tactic:
exact ⟨B, hB', hB.subset⟩

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

Goal state before:
pp: α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ (M ↾ S).IsBase B ↔ M.IsBase B ∧ B ⊆ S

Tactic:
isBase_restrict_iff',

Goal state after:
α : Type u_2
M : Matroid α
S B : Set α
hS : M.Spanning S
⊢ M.IsBasis' B S ↔ 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 = M'

Tactic:
have hsp' : M.Spanning = M'.Spanning := by
    ext S
    refine (em (S ⊆ M.E)).elim (fun hSE ↦ by rw [hsp _ hSE])
      (fun hSE ↦ iff_of_false (fun h ↦ hSE h.subset_ground)
      (fun h' ↦ hSE (h'.subset_ground.trans h.symm.subset)))
  rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]
  intro I hIE
  rw [← coindep_def, ← coindep_def, coindep_iff_compl_spanning, coindep_iff_compl_spanning, hsp', h]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X R : Set α
⊢ (M ↾ R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E

Tactic:
by
  obtain ⟨I, hI⟩ := (M ↾ R).exists_isBasis' X
  obtain ⟨hI', hIR⟩ := isBasis'_restrict_iff.1 hI
  ext e
  rw [← hI.closure_eq_closure, ← hI'.closure_eq_closure, hI.indep.mem_closure_iff', mem_union,
    mem_inter_iff, hI'.indep.mem_closure_iff', restrict_ground_eq, restrict_indep_iff, mem_sdiff]
  by_cases he : M.Indep (insert e I)
  · simp [he, and_comm, insert_subset_iff, hIR, (he.subset_ground (mem_insert ..)),
      imp_or_left_iff_true]
  tauto

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 α
g h : G
⊢ h • fixedBy α g = fixedBy α (h * g * h⁻¹)

Tactic:
ext a
  simp_rw [Set.mem_smul_set_iff_inv_smul_mem, mem_fixedBy, mul_smul, smul_eq_iff_eq_inv_smul h]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ f.natSepDegree = f.natDegree ↔ f.Separable

Tactic:
simp_rw [← card_rootSet_eq_natDegree_iff_of_splits hf (SplittingField.splits f),
    rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rfl

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E

pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E

Tactic:
· rw [← finSepDegree_top F, ← finrank_top F E]
    refine induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K ∣ finrank F K)
      (by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]) (fun L x h ↦ ?_) ⊤
    have hdvd := mul_dvd_mul h <| finSepDegree_adjoin_simple_dvd_finrank L E x
    set M := L⟮x⟯
    rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
      Module.finrank_mul_finrank F L M] at hdvd

Goal state after:
case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E ∣ finrank F E
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ n, V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst✝²] (⋃ n, V ^ (n + 1))
n : ℕ
⊢ W * V ^ (n + 1) ⊆ W

Tactic:
induction n with

Goal state after:
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✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : f * w1 = g * w2
⊢ False

Tactic:
eq_inv_mul_iff_mul_eq.symm,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
x : L
hx : f x ≠ g x
hφx : φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K ↥E := IntermediateField.adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
H : Subgroup Gal(L/K) := E.fixingSubgroup
h_basis : ↑H ∈ galGroupBasis K L
W : Set Gal(L/K)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : Gal(L/K)
hw1 : w1 ∈ W
w2 : Gal(L/K)
hw2 : w2 ∈ W
h : w1 = f⁻¹ * (g * w2)
⊢ False
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
⊢ PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits

Tactic:
refine ⟨fun ⟨h⟩ f hf ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
⊢ f.Splits

case refine_2
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
⊢ PerfectField F
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case neg
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₂ σ y (minpolyDiv R x) = 0

Tactic:
· rw [← eval₂_map, ← minpolyDiv_spec] at hy
    simpa [sub_eq_zero, Ne.symm h] using hy

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 * d = 0
⊢ IsUnit a ∨ IsUnit b

Tactic:
← C_eq_zero

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 : 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
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.Trace.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ trace R R = LinearMap.id

Tactic:
ext; simpa using trace_algebraMap_of_basis (.singleton (Fin 1) R) 1

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
this : NormalizedGCDMonoid R
h1 :
  C (integerNormalization R⁰ a).content *
      ((integerNormalization R⁰ a).primPart *
        (C (integerNormalization R⁰ b).content * (integerNormalization R⁰ b).primPart)) =
    C (c * d) * p
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b

Tactic:
mul_comm _ (C _ * _),

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 : 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
this : NormalizedGCDMonoid R
h1 :
  C (integerNormalization R⁰ a).content *
      (C (integerNormalization R⁰ b).content * (integerNormalization R⁰ b).primPart *
        (integerNormalization R⁰ a).primPart) =
    C (c * d) * p
u : Rˣ
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ IsUnit a ∨ IsUnit b
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
K : Type w
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : IsPurelyInseparable F E
L : Type w
inst✝² : CommRing L
inst✝¹ : IsReduced L
inst✝ : Algebra F L
f g : E →ₐ[F] L
⊢ (↑f).comp (algebraMap F E) = (↑g).comp (algebraMap F E)

Tactic:
AlgHom.comp_algebraMap

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
K : Type w
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
⊢ x ∈ (algebraMap (↥L) E).range

Tactic:
have := (isSeparable_adjoin_simple_iff_isSeparable L E).2 h

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
inst✝ : Algebra.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this : Algebra.IsSeparable ↥L ↥(↥L)⟮x⟯
⊢ x ∈ (algebraMap (↥L) E).range
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
K : Type w
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this✝ : Algebra.IsSeparable ↥L ↥(↥L)⟮x⟯
this : Algebra.IsSeparable F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯)
⊢ x ∈ (algebraMap (↥L) E).range

Tactic:
have hx : x ∈ L⟮x⟯.restrictScalars F := mem_adjoin_simple_self _ x

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
inst✝ : Algebra.IsAlgebraic F E
x : E
L : IntermediateField F E := separableClosure F E
h : IsSeparable (↥L) x
this✝ : Algebra.IsSeparable ↥L ↥(↥L)⟮x⟯
this : Algebra.IsSeparable F ↥(IntermediateField.restrictScalars F (↥L)⟮x⟯)
hx : x ∈ IntermediateField.restrictScalars F (↥L)⟮x⟯
⊢ x ∈ (algebraMap (↥L) E).range
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑x.valMinAbs = x

Tactic:
valMinAbs_def_pos

Goal state after:
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(if x.val ≤ namedPattern k (n + 1) h✝ / 2 then ↑x.val else ↑x.val - ↑(namedPattern k (n + 1) h✝)) = x
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2

Tactic:
valMinAbs_def_pos

Goal state after:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n) ↔ x.val ≤ n / 2
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
⊢ map (algebraMap B (B ⧸ Q)) r = q

Tactic:
ext n

Goal state after:
B : Type u_2
inst✝⁴ : CommRing B
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
Q : Ideal B
inst✝ : Q.IsPrime
val✝ : Fintype G
P : Ideal B := {g | g • Q ≠ Q}.inf fun g ↦ g • Q
h1 : ¬P ≤ Q
b : B
hbQ : b ∉ Q
hbP : ∀ (g : G), g • Q ≠ Q → b ∈ g • Q
f : B[X] := MulSemiringAction.charpoly G b
q : (B ⧸ Q)[X]
hq : map (algebraMap B (B ⧸ Q)) f = X ^ rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f) * q
hq0 : ¬X ∣ q
j : ℕ := rootMultiplicity 0 (map (algebraMap B (B ⧸ Q)) f)
k : ℕ := q.natDegree
r : B[X] := ∑ i ∈ Finset.range (k + 1), (monomial i) (f.coeff (i + j))
n : ℕ
⊢ (map (algebraMap B (B ⧸ Q)) r).coeff n = q.coeff n
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
⊢ ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

Tactic:
valMinAbs_def_pos

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑a.val - ↑n ≤ 0
⊢ ↑(if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = if a.val ≤ n / 2 then a else -a
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = a.valMinAbs + ↑(if a.val ≤ n / 2 then 0 else n)

Tactic:
valMinAbs_def_pos

Goal state after:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n) + ↑(if a.val ≤ n / 2 then 0 else n)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
hpos : NeZero n
a : ZMod n
⊢ a.valMinAbs.natAbs = min a.val (n - a.val)

Tactic:
valMinAbs_def_pos

Goal state after:
n : ℕ
hpos : NeZero n
a : ZMod n
⊢ (if a.val ≤ n / 2 then ↑a.val else ↑a.val - ↑n).natAbs = min a.val (n - a.val)
Module: Mathlib.FieldTheory.Galois.IsGaloisGroup

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
R : Type u_5
B : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Module.Finite R B
inst✝² : IsDomain B
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G R B
A : Subring B := ⋯
this✝⁴ : Algebra (FractionRing ↥A) (FractionRing B) := ⋯
this✝³ : MulSemiringAction G (FractionRing B) := ⋯
this✝² : Algebra R ↥A := ⋯
this✝¹ : IsScalarTower R (↥A) B
this✝ : Module.Finite (↥A) B
this : IsGaloisGroup G (FractionRing ↥A) (FractionRing B)
⊢ Nat.card G ≠ 0

Tactic:
card_eq_finrank G (FractionRing A) (FractionRing B)

Goal state after:
G : Type u_1
inst✝⁷ : Group G
R : Type u_5
B : Type u_6
inst✝⁶ : CommRing R
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Module.Finite R B
inst✝² : IsDomain B
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G R B
A : Subring B := (algebraMap R B).range
this✝⁴ : Algebra (FractionRing ↥A) (FractionRing B) := FractionRing.liftAlgebra (↥A) (FractionRing B)
this✝³ : MulSemiringAction G (FractionRing B) := IsFractionRing.mulSemiringAction G B (FractionRing B)
this✝² : Algebra R ↥A := (algebraMap R B).rangeRestrict.toAlgebra
this✝¹ : IsScalarTower R (↥A) B
this✝ : Module.Finite (↥A) B
this : IsGaloisGroup G (FractionRing ↥A) (FractionRing B)
⊢ finrank (FractionRing ↥A) (FractionRing B) ≠ 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
⊢ False

Tactic:
have ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p hd

Goal state after:
case inl
K : Type u_1
inst✝³ : Ring K
inst✝² : NoZeroDivisors K
inst✝¹ : Nontrivial K
G : Subgroup Kˣ
inst✝ : Fintype ↥G
n : ℕ := Fintype.card ↥G
nzero : ↑(Fintype.card ↥G) = 0
p : ℕ
char_p : CharP K p
hd : p ∣ n
pprime : Nat.Prime p
fact_pprime : Fact (Nat.Prime p)
x : ↥G
hx : orderOf x = p
⊢ False
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| b.equivFun z x✝ • (b i * b x✝)

Tactic:
← mul_smul_comm

Goal state after:
case f
ι : Type w
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : Basis ι A B
z : B
i x✝ : ι
| b i * b.equivFun z x✝ • b x✝