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

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ support R (M ⧸ I • ⊤) ⊆ zeroLocus ↑I

Tactic:
rw [support_eq_zeroLocus]
      apply PrimeSpectrum.zeroLocus_anti_mono_ideal
      rw [Submodule.annihilator_quotient]
      exact fun x hx ↦ Submodule.mem_colon.mpr fun p hp ↦ Submodule.smul_mem_smul hx hp

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ -((-1) ^ ↑j • (-1) ^ (↑i * 2) • f (j.removeNth v)) + (-1) ^ ↑j • f (j.removeNth v) = 0

pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i

Tactic:
pow_mul',

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ -((-1) ^ ↑j • ((-1) ^ 2) ^ ↑i • f (j.removeNth v)) + (-1) ^ ↑j • f (j.removeNth v) = 0

R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : j ∈ Finset.Ici i
⊢ (-1) ^ ↑i • (-1) ^ ↑j • ((f (v i.castSucc)) (i.castSucc.removeNth v j)) (j.removeNth (i.castSucc.removeNth v)) +
      (-1) ^ (↑j + 1) • (-1) ^ ↑i • ((f (v j.succ)) (j.succ.removeNth v i)) (i.removeNth (j.succ.removeNth v)) =
    (-1) ^ (↑i + ↑j) •
      (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
        ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))

Tactic:
Finset.mem_Ici

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
⊢ (-1) ^ ↑i • (-1) ^ ↑j • ((f (v i.castSucc)) (i.castSucc.removeNth v j)) (j.removeNth (i.castSucc.removeNth v)) +
      (-1) ^ (↑j + 1) • (-1) ^ ↑i • ((f (v j.succ)) (j.succ.removeNth v i)) (i.removeNth (j.succ.removeNth v)) =
    (-1) ^ (↑i + ↑j) •
      (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
        ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
⊢ N = ⊤

Tactic:
let : IsScalarTower R k (M ⧸ (𝔪 • ⊤ : Submodule R M)) :=
      inferInstanceAs (IsScalarTower R (R ⧸ 𝔪) (M ⧸ 𝔪 • (⊤ : Submodule R M)))

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
this✝ : Module k (M ⧸ 𝔪 • ⊤) :=
  { smul := map_tensorProduct_mk_eq_top._aux_1_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower R k (M ⧸ 𝔪 • ⊤) := map_tensorProduct_mk_eq_top._proof_1_9
⊢ N = ⊤
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ Submodule.span R (Set.range (⇑(map f) ∘ ⇑(tprod R))) =
    Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}

Tactic:
apply congrArg

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ Set.range (⇑(map f) ∘ ⇑(tprod R)) = {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
i j : Fin (Nat.succ 0).succ
hij : ![a, b] i = ![a, b] j
⊢ i = j

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case «0».«0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
hij : ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩) = ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

case «0».«1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
hij : ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩) = ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩)
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩

case «1».«0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
hij : ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩) = ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

case «1».«1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
hij : ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩) = ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
S T : Finset R
hSJ : ↑S ⊆ ↑J
hTK : ↑T ⊆ ↑K
hx : x ∈ Submodule.span R (↑S * ↑T)
⊢ x ∈ span (↑J * ↑T)

Tactic:
exact span_mono (Set.mul_subset_mul_right hSJ) hx

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
⊢ J * span {g} = span {x}

Tactic:
refine le_antisymm
      (mul_le.mpr fun b hb z hz ↦ ?_)
      ((span_singleton_le_iff_mem _).mpr hxJg)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : z ∈ span {g}
⊢ b * z ∈ span {x}
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
⊢ I.num ≠ 0

Tactic:
ne_eq,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hI : I ≠ 0
⊢ ¬I.num = 0
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: case hf
R : Type u_1
S✝ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Algebra R S✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
this✝ : Module (Localization S) M' := ⋯
this : Module (Localization S) N' := ⋯
⊢ IsBaseChange (Localization S) f

pp: case hg
R : Type u_1
S✝ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Algebra R S✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
this✝ : Module (Localization S) M' := ⋯
this : Module (Localization S) N' := ⋯
⊢ IsBaseChange (Localization S) g

Tactic:
· rw [← isLocalizedModule_iff_isBaseChange S]
    infer_instance

Goal state after:
case hg
R : Type u_1
S✝ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Algebra R S✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
this✝ : Module (Localization S) M' := ⋯
this : Module (Localization S) N' := ⋯
⊢ IsBaseChange (Localization S) g
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: case hg
R : Type u_1
S✝ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Algebra R S✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
this✝ : Module (Localization S) M' := ⋯
this : Module (Localization S) N' := ⋯
⊢ IsBaseChange (Localization S) g

Tactic:
· rw [← isLocalizedModule_iff_isBaseChange S]
    infer_instance

Goal state after:
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
N : Type (max v u) := Dual R M
e : M ⊗[R] N ≃ₗ[R] R := TensorProduct.comm R M N ≪≫ₗ linearEquiv R M
S : Finset (M × N)
hS : e.symm 1 = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
f : (↥S →₀ N) →ₗ[R] R := (Finsupp.lsum R) fun i ↦ ↑e ∘ₗ (TensorProduct.mk R M N) (↑i).1
this✝ : Function.Surjective ⇑f
g : R →ₗ[R] ↥S →₀ N
hg : f ∘ₗ g = LinearMap.id
aux : M ⊗[R] (↥S →₀ N) ≃ₗ[R] ↥S →₀ R := finsuppRight R R M N ↥S ≪≫ₗ Finsupp.mapRange.linearEquiv e
f' : (↥S →₀ R) →ₗ[R] M := ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M f ∘ₗ ↑aux.symm
g' : M →ₗ[R] ↥S →₀ R := ↑aux ∘ₗ LinearMap.lTensor M g ∘ₗ ↑(TensorProduct.rid R M).symm
this : Function.Surjective ⇑f'
m : M
⊢ (f' ∘ₗ g') m = LinearMap.id m

Tactic:
simp [f', g', show f (g 1) = 1 from DFunLike.congr_fun hg 1]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case hf
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 • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ (aeval (γ - c • β)) f = 0

Tactic:
add_sub_cancel_right,

Goal state after:
case hf
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 • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ (aeval α) f = 0
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
i : (i : ι) × ↥(t i)
x✝ : i ∈ s
⊢ adjoin F ((minpoly F i.snd).rootSet K) ≤ t i.fst

Tactic:
rw [adjoin_le_iff, ← ((h i.1).splits i.2).image_rootSet (t i.1).val]

Goal state after:
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
i : (i : ι) × ↥(t i)
x✝ : i ∈ s
⊢ ⇑(t i.fst).val '' (minpoly F i.snd).rootSet ↥(t i.fst) ⊆ ↑(t i.fst)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case inl
α : Type u_1
M✝ M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ M.Nonempty

Tactic:
exact False.elim <| RankPos.empty_not_isBase hB

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

Goal state before:
pp: case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
B : Set α
hB : M₁.IsBase B
hIB : I ⊆ B
⊢ M₂.Indep I

Tactic:
exact (hM₁ hB).subset hIB

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

Goal state before:
pp: α : Type u_1
E I X : Set α
⊢ I = X ∩ (freeOn E).E ∧ X ∩ (freeOn E).E ⊆ E ↔ I = X ∩ E

Tactic:
freeOn_ground,

Goal state after:
α : Type u_1
E I X : Set α
⊢ I = X ∩ E ∧ X ∩ E ⊆ E ↔ I = X ∩ E
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 α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)

Tactic:
rintro I B hI hImax hBmax
      suffices hcard : I.encard < B.encard by
        obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
        exact ⟨e, ⟨heB, heI⟩, hi⟩
      refine lt_of_not_ge fun hle ↦ ?_
      obtain ⟨x, hxnot, hxI⟩ := exists_insert_of_not_maximal indep_subset hI hImax
      have hlt : B.encard < (insert x I).encard := by
        rwa [encard_insert_of_notMem hxnot, ← not_le, ENat.add_one_le_iff, not_lt]
        rw [encard_ne_top_iff]
        obtain ⟨n, hn⟩ := indep_bdd
        exact finite_of_encard_le_coe (hn _ hI)
      obtain ⟨y, -, hyB, hi⟩ := indep_aug hBmax.prop hxI hlt
      exact hBmax.not_prop_of_ssuperset (ssubset_insert hyB) hi

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

Goal state before:
pp: α : Type u_1
N M : Matroid α
inst✝ : M.RankFinite
h : N ≤r M
⊢ N.RankFinite

Tactic:
obtain ⟨R, -, rfl⟩ := h
  infer_instance

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

Goal state before:
pp: α : Type u_1
N M : Matroid α
inst✝ : M.Finitary
h : N ≤r M
⊢ N.Finitary

Tactic:
obtain ⟨R, -, rfl⟩ := h
  infer_instance

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
⊢ ∀ ⦃I J : Set α⦄,
    (∀ (J : Finset α), ↑J ⊆ I → Indep J) →
      I.Finite →
        (∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1) →
          J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J

Tactic:
by
      intro I J hI hIfin hJ hJfin hIJ
      rw [ncard_eq_toFinset_card _ hIfin, ncard_eq_toFinset_card _ hJfin] at hIJ
      have aug := indep_aug (hI _ (by simp)) (hJ _ (by simp)) hIJ
      simp only [Finite.mem_toFinset] at aug
      obtain ⟨e, heJ, heI, hi⟩ := aug
      exact ⟨e, heJ, heI, fun K hK ↦ indep_subset hi <| Finset.coe_subset.1 (by simpa)⟩

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 β
⊢ (M.mapSetEmbedding { toFun := M.E.domRestrict f, inj' := ⋯ }).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
mapSetEmbedding_indep_iff',

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 β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑{ toFun := M.E.domRestrict f, inj' := ⋯ } '' I₀) ↔
    ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
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 '' B = I

Tactic:
hB.eq_of_subset_indep hI₀ hBI,

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
⊢ f '' I₀ = I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
hC : M.IsCircuit C
he : e ∈ C
⊢ M.IsBasis (C \ {e}) C

Tactic:
by
  nth_rw 2 [← insert_eq_of_mem he]
  rw [← insert_sdiff_singleton, (hC.sdiff_singleton_indep he).isBasis_insert_iff,
    insert_sdiff_singleton, insert_eq_of_mem he]
  exact Or.inl hC.dep

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

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

Tactic:
by
  rw [restrictSubtype, comap_isBase_iff]
  simp [Subtype.val_injective.injOn, isBasis_restrict_iff',
    isBasis'_iff_isBasis_inter_ground]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE

Tactic:
tfae_have 5 → 4 := by
    refine fun ⟨h, heE⟩ B hB ↦ by_contra fun heB ↦ ?_
    rw [← hB.closure_eq] at heE
    obtain ⟨C, -, hC, heC⟩ := (mem_closure_iff_exists_isCircuit heB).1 heE
    exact h hC heC

Goal state after:
α : Type u_1
M : Matroid α
e : α
tfae_1_iff_2 : M.IsColoop e ↔ e ∈ M.coloops
tfae_1_iff_3 : M.IsColoop e ↔ M.IsCocircuit {e}
tfae_1_iff_4 : M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
tfae_3_to_5 : M.IsCocircuit {e} → (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E
tfae_5_to_4 : (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E → ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
⊢ [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B,
      (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X,
      ¬M.Spanning (M.E \ {e})].TFAE
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : M.Dep X
⊢ M.eRk X ≠ X.encard

Tactic:
ne_eq,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.RankFinite
hX : M.Dep X
⊢ ¬M.eRk X = X.encard
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
exact h.isNonloop.not_isLoop

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

Goal state before:
pp: α : Type u_1
X : Set α
⊢ (freeOn X).eRk (freeOn X).E = X.encard

Tactic:
freeOn_ground,

Goal state after:
α : Type u_1
X : Set α
⊢ (freeOn X).eRk X = X.encard
Module: Mathlib.Combinatorics.Matroid.Loop

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

Tactic:
ext e
  rw [removeLoops_eq_restrict, restrict_isNonloop_iff, mem_ofPred, and_self]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure (X ∩ M.E))
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
rw [closure_inter_ground] at hI'

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
hI' : M.IsBasis I (M.closure X)
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)