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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ Function.Bijective ⇑(toModuleEnd R M)

Tactic:
have : toModuleEnd R (S := R) M = (lid R M).conj ∘ rTensorEquiv R R
      (comm .. ≪≫ₗ linearEquiv R M) ∘ RingEquiv.moduleEndSelf R ∘ MulOpposite.opEquiv := by
    ext; simp [LinearEquiv.conj, liftAux]

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
this :
  ⇑(toModuleEnd R M) =
    ⇑(lid R M).conj ∘
      ⇑(rTensorEquiv R R (TensorProduct.comm R M (Dual R M) ≪≫ₗ linearEquiv R M)) ∘
        ⇑(RingEquiv.moduleEndSelf R) ∘ ⇑MulOpposite.opEquiv
⊢ Function.Bijective ⇑(toModuleEnd R M)
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
have hx := IsIntegral.of_finite F x

Goal state after:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p *
      Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

Tactic:
splits_mul _ (map_ne_zero (minpoly.ne_zero hx))

Goal state after:
case inr
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits ∧
    (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F E) (minpoly F x)).Splits

F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL :
  (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p *
      Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) (minpoly F x)).Splits
⊢ Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p ≠ 0
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
one_mem : 1 ∈ span R ↑(Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T')
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑(mul' R A ∘ₗ lTensor A (↑I).subtype)

Tactic:
mem_span_finset

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
one_mem :
  ∃ f,
    Function.support f ⊆ ↑(Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T') ∧
      ∑ a ∈ Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T', f a • a = 1
⊢ Projective R ↥↑I ∧ Function.Bijective ⇑(mul' R A ∘ₗ lTensor A (↑I).subtype)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ¬M.RankInfinite ↔ M.RankFinite

Tactic:
← not_rankFinite_iff,

Goal state after:
α : Type u_1
M : Matroid α
⊢ ¬¬M.RankFinite ↔ M.RankFinite
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case pos
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
hm : m = 0
⊢ IsAlgebraic F α

Tactic:
rw [hm] at heq hmn
    simp only [pow_zero, adjoin_one] at heq
    obtain ⟨y, h⟩ := mem_bot.1 (heq.symm ▸ mem_adjoin_simple_self F (α ^ n))
    refine ⟨X ^ n - C y, X_pow_sub_C_ne_zero hmn y, ?_⟩
    simp only [map_sub, map_pow, aeval_X, aeval_C, h, sub_self]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
⊢ FiniteDimensional F E

Tactic:
by
  obtain ⟨α, hprim⟩ := h
  have hfin := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) α)
  rw [hprim] at hfin
  exact topEquiv.toLinearEquiv.finiteDimensional

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ B ∩ X ⊆ I

Tactic:
hI.eq_of_subset_indep (hB.indep.inter_right X) (subset_inter hIB hI.subset)
    inter_subset_right

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ B ∩ X ⊆ B ∩ X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis J Y ∧ M.IsBasis I X

Tactic:
exact ⟨hJY, hIX⟩

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ B'' ∩ J ∪ B'' ∩ (X \ J) ⊆ B'

Tactic:
hdj.symm.inter_eq,

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ ∅ ∪ B'' ∩ (X \ J) ⊆ B'
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_4
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ Disjoint J B'

Tactic:
have hI' : (B'' ∩ X) ∪ (B' \ X) ⊆ B' := by
      rw [union_subset_iff, and_iff_left sdiff_subset, ← union_sdiff_cancel hJX,
        inter_union_distrib_left, hdj.symm.inter_eq, empty_union, sdiff_eq, ← inter_assoc,
        ← sdiff_eq, sdiff_subset_comm, sdiff_eq, inter_assoc, ← sdiff_eq, inter_comm]
      exact subset_trans (inter_subset_inter_right _ hB''.subset_ground) hXJ

Goal state after:
case refine_4
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
⊢ Disjoint J B'
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
⊢ I.Finite

Tactic:
obtain ⟨n, hn⟩ := indep_bdd

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Set α⦄, Indep I → Indep J → I.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
hle : B.encard ≤ I.encard
x : α
hxnot : x ∉ I
hxI : Indep (insert x I)
n : ℕ
hn : ∀ (I : Set α), Indep I → I.encard ≤ ↑n
⊢ I.Finite
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ f '' B₀ = f '' J

Tactic:
hbij.image_eq

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set β
h : Maximal (M.map f hf).Indep B
B₀ : Set α
hB₀ : M.Indep B₀
hbij : BijOn f B₀ B
J : Set α
hJ : M.Indep J
hB₀J : B₀ ⊆ J
⊢ B = f '' J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
I₀ : Set α
hBI : B ⊆ I₀
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ f '' I₀ = I

Tactic:
hbij.image_eq

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
f : α → β
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
I : Set β
hI : (M.map f hf).Indep I
I₀ : Set α
hBI : B ⊆ I₀
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ I = I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C X : Set α
hC : M.IsCircuit C
hXC : X ⊂ C
⊢ M.Indep X

Tactic:
by
  rw [← not_dep_iff (hXC.subset.trans hC.subset_ground)]
  exact fun h ↦ hXC.ne ((isCircuit_iff.1 hC).2 h hXC.subset)

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

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

Tactic:
by rwa [eq_comm, image_preimage_eq_iff]

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

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

Tactic:
by rwa [eq_comm, image_preimage_eq_iff]

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
heC : e ∈ C
hCeI : C \ {e} ⊆ I
heCcl : e ∈ M.closure (C \ {e})
heI : e ∈ M.closure I
⊢ C \ {e} ∈ {J | J ⊆ I ∧ e ∈ M.closure J}

Tactic:
exact ⟨hCeI, heCcl⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ (M ↾ R).fundCircuit e I = M.fundCircuit e I

Tactic:
simp_rw [fundCircuit, M.restrict_closure_eq (R := R) (X := {e}) (by simpa)]

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) =
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ∨ M.IsNonloop e

Tactic:
rw [isNonloop_iff, and_iff_left he]; apply em

Goal state after:
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:
simp_rw [he.closure_eq_closure_iff_isCircuit_of_ne hne, or_iff_right hne,
    isCircuit_iff_dep_forall_sdiff_singleton_indep, dep_iff, insert_subset_iff,
    singleton_subset_iff, and_iff_left hf.mem_ground, and_iff_left he.mem_ground,
    and_iff_left_iff_imp]

Goal state after:
case inr
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hf : M.IsNonloop f
hne : e ≠ f
⊢ ¬M.Indep {e, f} → ∀ e_1 ∈ {e, f}, M.Indep ({e, f} \ {e_1})
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank = ⊤ ↔ M.RankInfinite

Tactic:
← not_rankFinite_iff,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M.eRank = ⊤ ↔ ¬M.RankFinite
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
⊢ M.eRank ≤ M.eRk X

Tactic:
rw [← hB.encard_eq_eRk, ← (hB.isBase_of_spanning hX).encard_eq_eRank]

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

Goal state before:
pp: α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
⊢ (∀ (a : Set α), M.IsBasis' (f '' a) (f '' X) → InjOn f a → a ⊆ X → lift.{v, u} #↑a ≤ lift.{u, v} (⨆ B, #↑↑B)) ∧
    ∀ (a : Set β), M.IsBasis' a (f '' X) → lift.{u, v} #↑a ≤ lift.{v, u} (⨆ B, #↑↑B)

Tactic:
refine ⟨fun I hI hfI hIX ↦ ?_, fun I hIX ↦ ?_⟩

Goal state after:
case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ lift.{v, u} #↑I ≤ lift.{u, v} (⨆ B, #↑↑B)

case refine_2
α : Type u
β : Type v
M : Matroid β
f : α → β
X : Set α
I : Set β
hIX : M.IsBasis' I (f '' X)
⊢ lift.{u, v} #↑I ≤ lift.{v, u} (⨆ B, #↑↑B)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
rw [isCocircuit_iff_minimal_compl_nonspanning]

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
⊢ Minimal (fun X ↦ ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
⊢ #↑(B \ B') ≤ #↑(B' \ B)

Tactic:
let U := ⋃ a : ↥(B' \ B), S a a.2

Goal state after:
case neg
α : Type u
β : Type v
f : α → β
M : Matroid α
I J B✝ B'✝ X Y : Set α
inst✝ : M.Finitary
B B' : Set α
N : Matroid α
hfin : N.Finitary
hB : N.IsBase B
hB' : N.IsBase B'
h : Infinite ↑(B' \ B)
S : (a : α) → a ∈ B' \ B → Set α
S_fin : ∀ (a : α) (ha : a ∈ B' \ B), Finite ↑(S a ha)
hSB : ∀ (a : α) (ha : a ∈ B' \ B), S a ha ⊆ B
dep : ∀ (a : α) (ha : a ∈ B' \ B), ¬N.Indep (insert a (S a ha))
U : Set α := ⋃ a, S ↑a ⋯
⊢ #↑(B \ B') ≤ #↑(B' \ B)
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
⊢ #↑(f '' I \ f '' (I ∩ J)) = #↑(f '' (J \ I))

Tactic:
hfJ.image_sdiff,

Goal state after:
α : 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
⊢ #↑(f '' I \ f '' (I ∩ J)) = #↑(f '' J \ f '' (J ∩ I))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: σ : Type u_3
R : Type u_4
inst✝ : CommRing R
⊢ AlgebraicIndependent R X

Tactic:
rw [AlgebraicIndependent, aeval_X_left]

Goal state after:
σ : Type u_3
R : Type u_4
inst✝ : CommRing R
⊢ Injective ⇑(AlgHom.id R (MvPolynomial σ R))
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : ∀ (p : MvPolynomial ι S), (aeval (⇑g ∘ x)) p = 0 → p = 0
hf : Injective ⇑f
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
p : MvPolynomial ι R
hp : (aeval x) p = 0
this : (MvPolynomial.map ↑f) p = 0
⊢ (MvPolynomial.map ↑f) p = (MvPolynomial.map ↑f) 0

Tactic:
rwa [map_zero]

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

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

Tactic:
by
  -- It is enough to prove that `map` and `closure` commute for `M`-independent sets.
  suffices aux : ∀ ⦃I⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' (M.closure I) by
    obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)
    rw [← closure_inter_ground, map_ground, ← M.closure_inter_ground, ← hI.closure_eq_closure,
      ← aux hI.indep, ← image_preimage_inter, ← (hI.map hf).closure_eq_closure]
  -- Let `I` be independent, and transform the goal using closure/independence lemmas
  refine fun I hI ↦ Set.ext fun e ↦ ?_
  simp only [(hI.map f hf).mem_closure_iff', map_ground, mem_image, map_indep_iff,
    forall_exists_index, and_imp, hI.mem_closure_iff']
  -- The goal now easily follows from the invariance of independence under maps.
  constructor
  · rintro ⟨⟨x, hxE, rfl⟩, h2⟩
    refine ⟨x, ⟨hxE, fun hI' ↦ ?_⟩, rfl⟩
    obtain ⟨y, hyI, hfy⟩ := h2 _ hI' image_insert_eq.symm
    rw [hf.eq_iff (hI.subset_ground hyI) hxE] at hfy
    rwa [← hfy]
  rintro ⟨x, ⟨hxE, hxi⟩, rfl⟩
  refine ⟨⟨x, hxE, rfl⟩, fun J hJ hJI ↦ ⟨x, hxi ?_, rfl⟩⟩
  replace hJ := hJ.map f hf
  have hrw := image_insert_eq ▸ hJI
  rwa [← hrw, map_image_indep_iff (insert_subset hxE hI.subset_ground)] at hJ

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 : G
a : α
h : ∀ (j : ℤ), a ∈ fixedBy α (g ^ j)
⊢ a ∈ fixedBy α g

Tactic:
by simpa using h 1

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ X.natSepDegree = 1

Tactic:
simp only [natSepDegree, aroots_X, Multiset.toFinset_singleton, Finset.card_singleton]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
q : ℕ
inst✝ : ExpChar F q
n : ℕ
y : F
⊢ (X ^ q ^ n - C y).natSepDegree = 1

Tactic:
rw [← expand_X, ← expand_C (q ^ n), ← map_sub, natSepDegree_expand, natSepDegree_X_sub_C]

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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsSeparable F ↥(t i)
⊢ Algebra.IsSeparable F ↥(⨆ i, t i)

Tactic:
simp_rw [← le_separableClosure_iff] at h ⊢
  exact iSup_le h

Goal state after:
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
h : Nat.card Gal(E/F) = finrank F E
⊢ IsGalois F E

Tactic:
apply of_fixedField_eq_bot
  have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup Gal(E/F))) E := finrank_pos
  rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm,
    finrank_mul_finrank, ← h, one_mul, IntermediateField.finrank_fixedField_eq_card]
  apply Nat.card_congr
  exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }

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
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
⊢ finInsepDegree F ↥⊤ = finInsepDegree F K

Tactic:
rw [finInsepDegree_def', insepDegree_top, ← finInsepDegree_def']

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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ g * C g.leadingCoeff⁻¹ ∣ map (algebraMap R K) f

Tactic:
rwa [Associated.dvd_iff_dvd_left (show Associated (g * C g.leadingCoeff⁻¹) g from _)]

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✝ : IsIntegrallyClosed R
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
⊢ Associated (g * C g.leadingCoeff⁻¹) g
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: 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
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K ((algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)

Tactic:
rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]

Goal state after:
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
hs : IsIntegral R s
p : R[X]
hp : (Polynomial.aeval s) p = 0
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
x✝ : Algebra K L := FractionRing.liftAlgebra R L
⊢ minpoly K ((algebraMap S L) s) ∣
    map (algebraMap R K) p -
      map (algebraMap R K) (minpoly R s) * (map (algebraMap R K) p /ₘ map (algebraMap R K) (minpoly R s))
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x) = 0 ∨ y - x = 0
⊢ ¬y - x = 0

Tactic:
by rwa [sub_eq_zero]

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
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
⊢ g ∈ lifts (algebraMap R K)

Tactic:
let g' := integerNormalization R⁰ g

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
f : R[X]
hf : f.IsPrimitive
g : K[X]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
⊢ g ∈ lifts (algebraMap R K)