mathlib-initiative/mathlib-tactics huggingface dataset:
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
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (finsuppLEquivDirectSum S M' ι).symm
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x)) =
    (Finsupp.mapRange.linearMap ε) x

Tactic:
Finsupp.mapRange.linearMap_apply,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (finsuppLEquivDirectSum S M' ι).symm
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x)) =
    Finsupp.mapRange ⇑ε ⋯ x
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ (r * y) • x = (y • a) ⊗ₜ[R] 1

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ (algebraMap R (S ⊗[R] p.ResidueField)) (r * y) * x = (y • a) ⊗ₜ[R] 1
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R✝
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R✝ S✝
p✝ : Ideal R✝
inst✝³ : p✝.IsPrime
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
H : Topology.IsEmbedding ⇑(preimageOrderIsoFiber R S p).symm := preimageHomeomorphFiber._proof_1 R S p
⊢ Continuous (preimageOrderIsoFiber R S p).toFun

Tactic:
convert!
        (H.toHomeomorphOfSurjective (preimageOrderIsoFiber R S p).symm.surjective).symm.continuous
      ext1 x
      obtain ⟨x, rfl⟩ := (H.toHomeomorphOfSurjective
        (preimageOrderIsoFiber R S p).symm.surjective).surjective x
      simp only [Equiv.toFun_as_coe, RelIso.coe_fn_toEquiv, Homeomorph.symm_apply_apply]
      simp

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
⊢ Module.Finite R M ∧ Projective R M

Tactic:
classical
  let aux := finsuppRight R _ M N S ≪≫ₗ Finsupp.mapRange.linearEquiv e
  let f' : (S →₀ R) →ₗ[R] M := TensorProduct.rid R M ∘ₗ f.lTensor M ∘ₗ aux.symm
  let g' : M →ₗ[R] S →₀ R := aux ∘ₗ g.lTensor M ∘ₗ (TensorProduct.rid R M).symm
  have : Function.Surjective f' := by simpa [f'] using LinearMap.lTensor_surjective _ this
  refine ⟨.of_surjective f' this, .of_split g' f' <| LinearMap.ext fun m ↦ ?_⟩
  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 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✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : 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 := ⋯
β_in_Fγ : β ∈ F⟮γ⟯
⊢ F⟮α, β⟯ ≤ F⟮γ⟯

Tactic:
adjoin_le_iff

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✝ : 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 • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ {α, β} ⊆ ↑F⟮γ⟯
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
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ∑ x_1, f x x_1 • b x_1 = ↑(LinearMap.id x)

Tactic:
Algebra.smul_def,

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
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
x : ↥↑I
⊢ ∑ x_1, (algebraMap R A) (f x x_1) * b x_1 = ↑(LinearMap.id 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 := ⋯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ F⟮α, β⟯ ≤ F⟮α + x • β⟯

Tactic:
adjoin_le_iff

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
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: case neg
α : 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 → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
⊢ False

Tactic:
obtain ⟨f, hfJ, hfI₀, hfi⟩ := indep_aug (indep_subset hI hI₀I) hI₀fin hJ hJfin hcard

Goal state after:
case neg
α : 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 → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀ : ∀ x ∈ B₀ \ I₀, ¬Indep (insert x I₀)
E₀ : Set α := insert e (I₀ ∪ B₀)
hE₀fin : E₀.Finite
J : Set α
hJmax : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) j → id J ⊆ id j → id j ⊆ id J
hB₀J : B₀ ⊆ J
hJ : Indep J
hJss : J ⊆ E₀
heI₀ : e ∉ I₀
heI₀i : Indep (insert e I₀)
heJ : e ∉ J
hJfin : J.Finite
hcard : I₀.ncard < J.ncard
f : α
hfJ : f ∈ J
hfI₀ : f ∉ I₀
hfi : Indep (insert f I₀)
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N✝ N : Matroid β
f : α → β
I B : Set α
hI : N.Indep (f '' I)
hIinj : InjOn f I
hImax : ¬Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) I
hBmax : Maximal (fun I ↦ N.Indep (f '' I) ∧ InjOn f I) B
I' : Set α
hII' : I ⊂ I'
hI' : N.Indep (f '' I')
hI'inj : InjOn f I'
h₁ : ¬(N ↾ range f).IsBase (f '' I)
h₂ : (N ↾ range f).IsBase (f '' B)
e : α
he : e ∈ B
hei : N.Indep (f '' insert e I) ∧ f '' insert e I ⊆ range f
he' : f e ∉ f '' I
heI : e ∉ I
⊢ ∃ x ∈ B \ I, N.Indep (f '' insert x I) ∧ InjOn f (insert x I)

Tactic:
exact ⟨e, ⟨he, heI⟩, hei.1, (injOn_insert heI).2 ⟨hIinj, he'⟩⟩

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

Goal state before:
pp: α : Type u_1
R : Set α
M : Matroid α
hR : R ⊂ M.E
⊢ M ↾ R <r M

Tactic:
by
  refine (M.restrict_isRestriction R hR.subset).isStrictRestriction_of_ne (fun h ↦ ?_)
  rw [← h, restrict_ground_eq] at hR
  exact hR.ne rfl

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ N <r M

Tactic:
rw [← h.eq_restrict]

Goal state after:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ M ↾ N.E <r M
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ N <r M

Tactic:
rw [← h.eq_restrict]
  exact restrict_isStrictRestriction (h.subset.ssubset_of_ne hne)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : N.IsBasis I X
hNM : N ≤r M
⊢ M.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM; exact ((isBasis_restrict_iff hR).1 hI).1

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

Goal state before:
pp: α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
⊢ M.IsRkFinite (⋃ i, Xs i)

Tactic:
choose Is hIs using fun i ↦ M.exists_isBasis' (Xs i)

Goal state after:
α : Type u_1
M : Matroid α
ι : Type u_2
inst✝ : Finite ι
Xs : ι → Set α
h : ∀ (i : ι), M.IsRkFinite (Xs i)
Is : ι → Set α
hIs : ∀ (i : ι), M.IsBasis' (Is i) (Xs i)
⊢ M.IsRkFinite (⋃ i, Xs 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
hBI : f '' B ⊆ I
I₀ : Set α
hI₀ : M.Indep I₀
hbij : BijOn f I₀ I
⊢ f '' B = I

Tactic:
rw [← hbij.image_eq, hf.image_subset_image_iff hB.subset_ground hI₀.subset_ground] at 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 '' B = I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Set α
f : α → β
hf : InjOn f (loopyOn E).E
⊢ (loopyOn E).map f hf = loopyOn (f '' E)

Tactic:
simp [eq_loopyOn_iff]

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

Goal state before:
pp: case inl
α : Type u_1
M : Matroid α
C I : Set α
e : α
hC : M.IsCircuit C
hI : M.Indep I
hCs : C ⊆ insert e I
hCI : C ⊆ I
⊢ C = M.fundCircuit e I

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
⊢ C = M.fundCircuit e I

Tactic:
· exact (hC.not_indep (hI.subset hCI)).elim

Goal state after:
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
⊢ C = M.fundCircuit e I
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

Tactic:
simp_rw [isLoop_iff_forall_mem_compl_isBase, mem_sdiff, and_iff_right he]

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

Goal state before:
pp: α : Type u_1
E : Set α
M N : Matroid α
hM : M.E = E
hN : N.E = E
h : M.restrictSubtype E = N.restrictSubtype E
⊢ M = N

Tactic:
subst hM

Goal state after:
α : Type u_1
M N : Matroid α
hN : N.E = M.E
h : M.restrictSubtype M.E = N.restrictSubtype M.E
⊢ M = N
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsLoop e ↔ M.closure {e} = M.loops

Tactic:
rw [isLoop_iff_closure_eq_loops_and_mem_ground, and_iff_left he]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk (M.closure X) = M.eRk X

Tactic:
by
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.closure_eq_closure, ← hI.indep.isBasis_closure.encard_eq_eRk, hI.encard_eq_eRk]

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

Goal state before:
pp: α : Type u
M : Matroid α
⊢ Monotone M.cRk

Tactic:
simp only [Monotone, cRk_le_iff]

Goal state after:
α : Type u
M : Matroid α
⊢ ∀ ⦃a b : Set α⦄, a ⊆ b → ∀ ⦃I : Set α⦄, M.IsBasis' I a → #↑I ≤ M.cRk b
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite

Tactic:
obtain ⟨J, hJC, hJfin, hJ⟩ := hi

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y I : Set α
hI : M.IsBasis I X
hY : I ⊆ Y
h : M.closure X = M.closure Y
hYE : Y ⊆ M.E
⊢ Y ⊆ M.closure Y

Tactic:
exact M.subset_closure Y

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

Goal state before:
pp: α : Type u_2
I E X : Set α
⊢ (freeOn I).closure (X ∩ E) ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I

Tactic:
freeOn_closure_eq,

Goal state after:
α : Type u_2
I E X : Set α
⊢ X ∩ E ∩ I ∩ E ∪ E \ (freeOn I).E = X ∩ I ∩ E ∪ E \ I
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
⊢ AlgebraicIndependent S x

Tactic:
nontriviality S

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
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✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
a✝ : Nontrivial S
⊢ AlgebraicIndependent S x
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ind : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x ↔ Algebra.IsAlgebraic (↥(adjoin R (range x))) A

Tactic:
by
  refine ⟨(·.isAlgebraic), fun alg ↦ ⟨ind, fun s ind_s hxs ↦ of_not_not fun hxs' ↦ ?_⟩⟩
  have : ¬ s ⊆ range x := (hxs' <| hxs.antisymm ·)
  have ⟨a, has, hax⟩ := not_subset.mp this
  rw [show range x = Subtype.val '' range (Set.inclusion hxs) by
    rw [← range_comp, val_comp_inclusion, Subtype.range_val]] at alg
  refine ind_s.transcendental_adjoin (s := range (inclusion hxs)) (i := ⟨a, has⟩) ?_ (alg.1 _)
  simpa using hax

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

Goal state before:
pp: case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Nonempty { x // x ∈ B }
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Subsingleton R
this : ¬Nonempty { x // x ∈ I }
⊢ False

Tactic:
have ⟨b, hb⟩ := B_base

Goal state after:
case inl
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
I B : Set A
I_ind : AlgebraicIndepOn R _root_.id I
B_base : Nonempty { x // x ∈ B }
h : ∀ x ∈ B \ I, ¬AlgebraicIndepOn R _root_.id (insert x I)
h✝ : Subsingleton R
this : ¬Nonempty { x // x ∈ I }
b : A
hb : b ∈ B
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ (matroid R A).closure s = s

Tactic:
by
  simp_rw [Matroid.closure, matroid_isFlat_of_subsingleton, true_and, matroid_e, inter_univ]
  exact subset_antisymm (sInter_subset_of_mem <| subset_refl s) (subset_sInter fun _ ↦ id)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ f.natSepDegree ≤ g.natSepDegree

Tactic:
natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F)

Goal state after:
F : Type u
inst✝ : Field F
f g : F[X]
h1 : f ∣ g
h2 : g ≠ 0
⊢ (f.aroots (AlgebraicClosure F)).toFinset.card ≤ (g.aroots (AlgebraicClosure F)).toFinset.card
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
⊢ ↑H ∈ 𝓝 x

Tactic:
have : Filter.Tendsto (fun y ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g) :=
    (continuous_id.mul_const _).tendsto' _ _ (mul_inv_cancel_left _ _)

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
this : Filter.Tendsto (fun y ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)
⊢ ↑H ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.OpenSubgroup

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W

Tactic:
rcases isOpen_prod_iff.mp (continuous_mul.isOpen_preimage W <| WClopen.2) x 1 this with
    ⟨U, V, Uopen, Vopen, xmemU, onememV, prodsub⟩

Goal state after:
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W
U V : Set G
Uopen : IsOpen[inst✝³] U
Vopen : IsOpen[inst✝³] V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' W
⊢ ∃ t ∈ 𝓝[W] x, ∃ T ∈ 𝓝 1, t * T ⊆ W
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
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Nat.card Gal(E/F) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
by
  tfae_have 1 → 2 := fun h ↦ OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm
  tfae_have 1 → 3 := fun _ ↦ card_aut_eq_finrank F E
  tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E
  tfae_have 2 → 1 := of_fixedField_eq_bot F E
  tfae_have 3 → 1 := of_card_aut_eq_finrank F E
  tfae_have 4 → 1 := fun ⟨h, hp1, _⟩ ↦ of_separable_splitting_field hp1
  tfae_finish

Goal state after:
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
⊢ minpoly R s ∣ p

Tactic:
by
  let K := FractionRing R
  let L := FractionRing S
  let _ : Algebra K L := FractionRing.liftAlgebra R L
  have : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (p %ₘ minpoly R s) := by
    rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
    refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_
    · rw [← map_aeval_eq_aeval_map, hp, map_zero]
      rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
    apply dvd_mul_of_dvd_left
    rw [isIntegrallyClosed_eq_field_fractions K L hs]
  rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
    map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this
  rw [← modByMonic_eq_zero_iff_dvd (minpoly.monic hs)]
  exact Polynomial.eq_zero_of_dvd_of_degree_lt this (degree_modByMonic_lt p <| minpoly.monic hs)

Goal state after: