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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
k : ℕ
a' : (Fin l →₀ R) →ₗ[R] Fin k →₀ R
y' : (Fin k →₀ R) →ₗ[R] M
ha'y' : x' = y' ∘ₗ a'
ha' : a' f' = 0
j : Fin k
⊢ (a' (∑ x, Finsupp.single x ((equivFunOnFinite.symm f) x))) j = 0

Tactic:
univ_sum_single

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
tfae_4_to_5 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) →
    ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
h₅ : ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0
l : ℕ
f : Fin l → R
x : Fin l → M
hfx : ∑ i, f i • x i = 0
f' : Fin l →₀ R := equivFunOnFinite.symm f
x' : (Fin l →₀ R) →ₗ[R] M := linearCombination R x
this : x' f' = 0
k : ℕ
a' : (Fin l →₀ R) →ₗ[R] Fin k →₀ R
y' : (Fin k →₀ R) →ₗ[R] M
ha'y' : x' = y' ∘ₗ a'
ha' : a' f' = 0
j : Fin k
⊢ (a' (equivFunOnFinite.symm f)) j = 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
by_cases h : (Submodule.span R {m}).annihilator = ⊤

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : (R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Flat R M
P : Type u_3
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R P
h₁ : P →ₗ[R] M
w✝ : ℕ
K : Submodule R (Fin w✝ → R)
ϕ : P ≃ₗ[R] (Fin w✝ → R) ⧸ K
hK : K.FG
this : Module.Finite R ↥K
⊢ (h₁ ∘ₗ ↑ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0

Tactic:
simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a
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
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
⊢ Nontrivial Mₚ'

Tactic:
let Mₚ'' := Mₚ ⧸ I.map (algebraMap R Rₚ) • (⊤ : Submodule Rₚ Mₚ)

Goal state after:
case a
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
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
⊢ Nontrivial Mₚ'
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
hs₂ : span R (⇑((mk R 𝓀 ↥N) 1) '' t) = ⊤
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
⊢ span R t = ⊤

Tactic:
← map_span,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
hs₂ : Submodule.map ((mk R 𝓀 ↥N) 1) (span R t) = ⊤
ht₁ : ⇑((mk R 𝓀 ↥N) 1) '' t = s
⊢ span R t = ⊤
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.succAbove i) •
        (-1) ^ ↑(i.predAbove j) • (-1) ^ ↑?p • f (insertNth ?p (v j) (i.removeNth (j.removeNth v))) +
      (-1) ^ ↑j • f (j.removeNth v) =
    0

pp: case p
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
⊢ Fin (m + 1)

Tactic:
insertNth_removeNth,

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.succAbove i) • (-1) ^ ↑(i.predAbove j) • (-1) ^ ↑i • f (update (j.removeNth v) i (v j)) +
      (-1) ^ ↑j • f (j.removeNth v) =
    0
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
k : Fin (n + 1)
x✝ : k ≠ i ∧ k ≠ j
hki : k ≠ i
hkj : k ≠ j
⊢ (-1) ^ ↑k • (f (v k)) (k.removeNth v) = 0

Tactic:
rcases exists_succAbove_eq hki.symm with ⟨i, rfl⟩

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
j k : Fin (n + 1)
hkj : k ≠ j
i : Fin n
hvij : v (k.succAbove i) = v j
hij : k.succAbove i ≠ j
x✝ : k ≠ k.succAbove i ∧ k ≠ j
hki : k ≠ k.succAbove i
⊢ (-1) ^ ↑k • (f (v k)) (k.removeNth v) = 0
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁶ : CommSemiring R
N₁ : Type u_6
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : Module R N₁
N₂ : Type u_7
inst✝³ : AddCommMonoid N₂
inst✝² : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝¹ : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
⊢ ∀ [inst : DecidableEq (ι₁ ⊕ ι₂)] (m : (i : ι₁ ⊕ ι₂) → N i) (i : ι₁ ⊕ ι₂) (c : R) (x : N i),
    ((a fun i₁ ↦ Function.update m i (c • x) (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ ↦ Function.update m i (c • x) (Sum.inr i₂)) =
      c • (a fun i₁ ↦ Function.update m i x (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ ↦ Function.update m i x (Sum.inr i₂)

Tactic:
by
    rintro _ m (i₁ | i₂) p q
    · let := Classical.decEq ι₁; simp
    · let := Classical.decEq ι₂; simp

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R M
⊢ Subsingleton (k ⊗[R] M) ↔ Subsingleton M

Tactic:
rw [← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← Submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top,
    ← map_tensorProduct_mk_eq_top (M := M), Submodule.map_bot]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
h : i = j
⊢ ⇑(cast R M h) = _root_.cast ⋯

Tactic:
by
  subst h
  rw [cast_refl]
  rfl

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
⊢ IsOpen[inst✝] (f ⁻¹' s)

Tactic:
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_
    rcases h x with ⟨U, hU, hxU, eq⟩
    exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩

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

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y

Tactic:
exact ⟨f (Classical.arbitrary X), hf.eq_const _⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
⊢ (range f).Finite

Tactic:
let : TopologicalSpace Y := ⊥

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ (range f).Finite
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
⊢ IsBaseChange S (lmap ε)

Tactic:
by
  classical
  apply of_equiv <| directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ (ibc i).equiv
  intros; ext
  simp [coe_directSumRight, coe_congrLinearEquiv, equiv_tmul]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : Pic R
⊢ M = N ↔ Nonempty (M.AsModule ≃ₗ[R] N.AsModule)

Tactic:
by
  rw [← mk_eq_iff, mk_eq_self]

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

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

Tactic:
apply Normal.of_isSplittingField (∏ i ∈ s, minpoly F i.2)

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
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
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ Polynomial.map (algebraMap (↥F⟮α + c • β⟯) E) p = EuclideanDomain.gcd ?_1 ?_2

Tactic:
convert! (gcd_map (algebraMap F⟮γ⟯ E)).symm

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
use α + x • β

Goal state after:
case h
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ = F⟮α + x • β⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : (x - y) • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
replace β_in_K := smul_mem _ β_in_K (x := (x - y)⁻¹)

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : (x - y)⁻¹ • (x - y) • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
D : Set α
hD : M.Dep D
⊢ D.Nonempty

Tactic:
by
  rw [nonempty_iff_ne_empty]; rintro rfl; exact hD.not_indep M.empty_indep

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
x✝ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B ⊆ B'
⊢ M.IsBase B

Tactic:
rwa [h' hB'.indep hBB']

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

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
⊢ ∃ B, Maximal M.Indep B

Tactic:
obtain ⟨B, -, hB⟩ := M.indep_maximal M.E rfl.subset ∅ M.indep_empty <| empty_subset _

Goal state after:
α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal (fun K ↦ M.Indep K ∧ K ⊆ M.E) B
⊢ ∃ B, Maximal M.Indep B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I✝ B✝ X : Set α
M : Matroid α
I J : Set α
hJE : J ⊆ M.E
B : Set α
hB : M.IsBase B
hJB : Disjoint J B
hIJ : I ⊆ J
⊢ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B

Tactic:
exact ⟨hIJ.trans hJE, ⟨B, hB, disjoint_of_subset_left hIJ hJB⟩⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBasis B M.E ↔ M.IsBase B

Tactic:
rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
    maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
    and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]

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
I : Set α
hI : M.IsBasis I (M.E \ X)
⊢ ∃ J, I' ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J

Tactic:
obtain ⟨B', hB', hIB', hB'IB⟩ := hI.indep.exists_isBase_subset_union_isBase hB

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
I : Set α
hI : M.IsBasis I (M.E \ X)
B' : Set α
hB' : M.IsBase B'
hIB' : I ⊆ B'
hB'IB : B' ⊆ I ∪ B
⊢ ∃ J, I' ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B) K ∧ K ⊆ X) J
Module: Mathlib.Combinatorics.Matroid.Constructions

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

Tactic:
freeOn_isBasis_iff,

Goal state after:
α : Type u_1
E I X : Set α
⊢ I = X ∩ (freeOn E).E ∧ X ∩ (freeOn E).E ⊆ E ↔ I = X ∩ E
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis' I X ↔ M.IsBasis' I (X ∩ R) ∧ I ⊆ R

Tactic:
simp_rw [IsBasis', maximal_iff, restrict_indep_iff, subset_inter_iff, and_imp]
  tauto

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

Goal state before:
pp: α : Type u_1
I : Set α
⊢ uniqueBaseOn I I = freeOn I

Tactic:
rw [uniqueBaseOn, freeOn_restrict rfl.subset]

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 α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (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:
hJfin

Goal state after:
α : 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 α
hI : ∀ (J : Finset α), ↑J ⊆ I → Indep J
hIfin : I.Finite
hJ : ∀ (J_1 : Finset α), ↑J_1 ⊆ J → Indep J_1
hJfin : J.Finite
⊢ I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ ∀ (J : Finset α), ↑J ⊆ insert e I → Indep J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : α → β
hf : InjOn f M.E
I : Set β
⊢ (∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = (fun a ↦ M.E.domRestrict f a) '' I₀) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
domRestrict_apply,

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 = (fun a ↦ f ↑a) '' I₀) ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (M.mapEquiv f).Indep I ↔ M.Indep (⇑f.symm '' I)

Tactic:
rw [mapEquiv_eq_map, map_indep_iff]

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f.symm '' I)
Module: Mathlib.Combinatorics.Matroid.Map

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

Tactic:
comap_isBase_iff

Goal state after:
α : Type u_1
X : Set α
M : Matroid α
B : Set ↑X
⊢ (M ↾ X).IsBasis ↑B ↑(X ↓∩ (M ↾ X).E) ∧ InjOn Subtype.val B ∧ B ⊆ X ↓∩ (M ↾ X).E ↔ M.IsBasis' (Subtype.val '' B) X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ SurjOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
by simp [SurjOn]

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

Goal state before:
pp: α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E

Tactic:
← hM,

Goal state after:
α : Type u_1
E : Set α
M : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

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

Tactic:
rw [mem_closure_iff_exists_isCircuit (by simp [hzI])] at hcl

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
J : Set α
x : ι → α
I : ι → Set α
z : α
hxI : ∀ (i : ι), x i ∉ I i
hC : ∀ (i : ι), M.IsCircuit (insert (x i) (I i))
hJx : M.IsCircuit (J ∪ range x)
hzJ : z ∈ J
hzI : ∀ (i : ι), z ∉ I i
hι : Nonempty ι
hcl : ∃ C ⊆ insert z ((⋃ i, I i) ∪ J \ {z}), M.IsCircuit C ∧ z ∈ C
⊢ ∃ C' ⊆ J ∪ ⋃ i, I i, M.IsCircuit C' ∧ z ∈ C'
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)
⊢ I.encard = 0 ↔ X ∩ M.E ⊆ M.loops

Tactic:
encard_eq_zero

Goal state after:
α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
⊢ I = ∅ ↔ X ∩ M.E ⊆ M.loops
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Tactic:
rw [← hIX.eRk_eq_eRk_union, union_comm, ← hIY.eRk_eq_eRk_union, ← hIi.encard_eq_eRk,
    ← hIX.encard_eq_eRk, ← hIY.encard_eq_eRk, union_comm, ← encard_union_add_encard_inter, add_comm]

Goal state after:
α : Type u_1
M : Matroid α
X Y Ii : Set α
hIi : M.IsBasis' Ii (X ∩ Y)
IX : Set α
hIX : M.IsBasis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.IsBasis' IY Y
hIY' : Ii ⊆ IY
⊢ M.eRk (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard