mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective ⇑(mulLeftMap N m)

Tactic:
mulLeftMap_eq_mulMap_comp,

Goal state after:
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
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective
    ⇑(M.mulMap N ∘ₗ
        LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
φ : MultilinearMap R s E
f : (i : ι) → s i
⊢ (0, f).1 • φ (0, f).2 = 0

Tactic:
by simp_rw [zero_smul]

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
I : Ideal R
hI : ↑I * (↑I)⁻¹ = 1
a : R
K : Ideal R
ha0 : a ≠ 0
ha0' :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * (spanSingleton R⁰ ((algebraMap R (FractionRing R)) a))⁻¹ = 1
h :
  spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * ↑I *
      (spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)⁻¹ * ↑K) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * ↑I * (↑I)⁻¹
⊢ ↑I * ↑K = spanSingleton R⁰ ((algebraMap R (FractionRing R)) a)

Tactic:
rwa [mul_mul_mul_comm, ← spanSingleton_inv, ha0', one_mul, mul_assoc, hI, mul_one] at h

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) ∣ n

Tactic:
rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow]

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

Goal state before:
pp: case h
R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
u : (FractionalIdeal R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ ↑v = ↑u
hu : (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u = I
⊢ spanSingleton S⁰ ↑((Units.map ↑(IsFractionRing.ringEquivOfRingEquiv f).toRingHom) v) = ↑I

Tactic:
← hu

Goal state after:
case h
R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, (∃ x_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I
u : (FractionalIdeal R⁰ K)ˣ
v : Kˣ
huv : spanSingleton R⁰ ↑v = ↑u
hu : (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u = I
⊢ spanSingleton S⁰ ↑((Units.map ↑(IsFractionRing.ringEquivOfRingEquiv f).toRingHom) v) =
    ↑((Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) u)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥

Tactic:
rw [← hn]

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ ⊥

Tactic:
rw [← hn]

Goal state after:
case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ derivedSeries G 0
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ ⊥

Tactic:
rw [← hn]

Goal state after:
case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ derivedSeries G 0
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N = ↑((LinearEquiv.rTensor N (linearEquivDual e)).symm ≪≫ₗ e)

Tactic:
rw [LinearEquiv.coe_trans, LinearEquiv.eq_comp_toLinearMap_symm]; ext; rfl

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) *
      finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    (rankAtStalk M * rankAtStalk N) p

Tactic:
← rankAtStalk_eq_finrank_tensorProduct,

Goal state after:
R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ rankAtStalk M p * finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    (rankAtStalk M * rankAtStalk N) p
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ rankAtStalk M p * finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] N) =
    (rankAtStalk M * rankAtStalk N) p

Tactic:
← rankAtStalk_eq_finrank_tensorProduct,

Goal state after:
R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
e : Localization.AtPrime p.asIdeal ⊗[R] (M ⊗[R] N) ≃ₗ[Localization.AtPrime p.asIdeal]
  Localization.AtPrime p.asIdeal ⊗[R] M ⊗[Localization.AtPrime p.asIdeal] (Localization.AtPrime p.asIdeal ⊗[R] N) :=
  (AlgebraTensorModule.assoc R R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal) M N).symm ≪≫ₗ
    (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal)
        (Localization.AtPrime p.asIdeal ⊗[R] M) N).symm
⊢ rankAtStalk M p * rankAtStalk N p = (rankAtStalk M * rankAtStalk N) p
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K K' : IntermediateField F L
inst✝ : Normal F L
h : K ≤ K'
⊢ normalClosure F (↥K) L ≤ normalClosure F (↥K') L

Tactic:
rw [normalClosure_def', normalClosure_def']
  exact iSup_mono (fun f ↦ map_mono f h)

Goal state after:
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, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
x✝² : A
x✝¹ : ↥↑I
x✝ : ↥S
⊢ ((AlgebraTensorModule.curry (↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f)) x✝²) x✝¹ x✝ =
    ((AlgebraTensorModule.curry ((LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m)) x✝²) x✝¹ x✝

Tactic:
simp [(Algebra.smul_def ..).trans (Algebra.commutes ..), hf, m, mul_assoc]

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✝³ : FiniteDimensional F E
inst✝² : Algebra.IsSeparable F E
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra F L
hL : ∀ (x : E), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ Fintype.card (E →ₐ[F] L) = finrank F E

Tactic:
by
  rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_splits F E L hL]

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

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

Tactic:
iff_false_intro he.1.2,

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
exact fun e heJ heI ↦ ⟨he e ⟨heJ, heI⟩, hJ.subset_ground heJ⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C I : Set α
hC : M.IsCircuit C
⊢ M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · obtain ⟨e, he⟩ := exists_of_ssubset
      (h.subset.ssubset_of_ne (by rintro rfl; exact hC.dep.not_indep h.indep))
    exact ⟨e, he.1, h.eq_of_subset_indep (hC.sdiff_singleton_indep he.1)
      (subset_sdiff_singleton h.subset he.2) sdiff_subset⟩
  rintro ⟨e, he, rfl⟩
  exact hC.sdiff_singleton_isBasis he

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

Goal state before:
pp: α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep I

Tactic:
restrictSubtype_indep_iff,

Goal state after:
α : Type u_1
X I : Set α
M : Matroid α
hIX : I ⊆ X
⊢ M.Indep ↑(X ↓∩ I) ↔ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case h₂
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
J : Set α
hJI : J ⊆ I
heJ : M.closure {e} ∩ R ⊆ M.closure J
⊢ {e} ⊆ M.closure J

Tactic:
exact subset_trans (by simpa [M.mem_closure_of_mem' (mem_singleton e) (hR heR)]) heJ

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ M.Indep {e} ↔ M.IsNonloop e

Tactic:
rw [isNonloop_iff, ← singleton_dep, dep_iff, not_and, not_imp_not, singleton_subset_iff]

Goal state after:
α : Type u_1
M : Matroid α
e : α
⊢ M.Indep {e} ↔ (e ∈ M.E → M.Indep {e}) ∧ e ∈ M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard

Tactic:
have hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X) := by
    simpa using hB'.inter_isBasis_iff_compl_inter_isBasis_dual.1 hI

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
B : Set α
hB : M✶.IsBasis B M.E
hI : M✶.IsBasis (B ∩ X) X
hB' : M✶.IsBase B
hd : M.IsBasis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ e ∈ M.closure I \ I

Tactic:
rw [mem_sdiff, hI.mem_closure_iff, or_and_right, and_not_self_iff, or_false,
    iff_self_and, imp_not_comm]

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ I → ¬M.Dep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
X : Set α
⊢ M.cRk (M.closure X) = M.cRk X

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.isBasis_closure_right.cardinalMk_eq_cRk, ← hI.cardinalMk_eq_cRk]

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

Goal state before:
pp: case inl
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ toENat #↑B = B.encard

Tactic:
toENat_cardinalMk

Goal state after:
case inl
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ B.encard = B.encard
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
K : Type u_3
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : Algebra K A
inst✝ : IsScalarTower R K A
hinj : Injective ⇑(algebraMap R K)
ai : AlgebraicIndependent K x
⊢ AlgebraicIndependent R x

Tactic:
have : (aeval x : MvPolynomial ι K →ₐ[K] A).toRingHom.comp (MvPolynomial.map (algebraMap R K)) =
      (aeval x : MvPolynomial ι R →ₐ[R] A).toRingHom := by
    ext <;> simp [algebraMap_eq_smul_one]
  change Injective (aeval x).toRingHom
  rw [← this, RingHom.coe_comp]
  exact Injective.comp ai (MvPolynomial.map_injective _ hinj)

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

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A

Tactic:
let e := Rx.equivMapOfInjective f (FaithfulSMul.algebraMap_injective S A)

Goal state after:
ι : Type u
R : Type u_1
S : Type v
A : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Nontrivial R
inst✝² : NoZeroDivisors S
inst✝¹ : Algebra.IsAlgebraic S A
inst✝ : FaithfulSMul S A
x : ι → S
hx : IsTranscendenceBasis R x
f : S →ₐ[R] A := IsScalarTower.toAlgHom R S A
Rx : Subalgebra R S := adjoin R (range x)
e : ↥Rx ≃ₐ[R] ↥(Subalgebra.map f Rx) := Rx.equivMapOfInjective f ⋯
⊢ Algebra.IsAlgebraic (↥(Subalgebra.map f Rx)) A
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✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
ht : Algebra.IsAlgebraic (↥(adjoin R t)) A
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val

Tactic:
← matroid_spanning_iff

Goal state after:
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
this✝² : Nontrivial ↥(adjoin R t)
this✝¹ : Nontrivial A
this✝ : IsDomain A
this : FaithfulSMul R A
ht : (matroid R A).Spanning t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : f.Splits
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun x ↦ X - C x) f.roots).prod
h2 : f.roots.card ≠ 0
y : F
h3 : f.roots = f.roots.card • {y}
⊢ f = (X - C y) ^ f.roots.card

Tactic:
rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
    Multiset.prod_singleton] at h1

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✝¹ : IsGalois F E
inst✝ : Finite Gal(E/F)
⊢ FiniteDimensional F E

Tactic:
by_contra H
  obtain ⟨K, h₁, h₂⟩ := exists_lt_finrank_of_infinite_dimensional H (Nat.card Gal(E/F))
  let K' := normalClosure F K E
  have : IsGalois F K' := ⟨⟩
  have := Nat.card_le_card_of_surjective _
    (AlgEquiv.restrictNormalHom_surjective (F := F) (K₁ := K') (E := E))
  rw [IsGalois.card_aut_eq_finrank] at this
  exact (this.trans_lt h₂).not_ge (finrank_le_of_le_right K.le_normalClosure)

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✝
H : Subgroup Gal(E✝/F)
K✝ : IntermediateField F E✝
K : Type u_3
L : Type u_4
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
E : IntermediateField K L
inst✝¹ : IsGalois K L
inst✝ : IsGalois K ↥E
⊢ E.fixingSubgroup.Normal

Tactic:
apply Subgroup.Normal.of_conjugate_fixed (fun σ ↦ ?_)
  rw [← map_fixingSubgroup, normal_iff_forall_map_eq'.mp inferInstance σ]

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
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
⊢ f ∈ Finset.univ → Nat.card (↥K⟮x⟯ →ₐ[K] E) = (minpoly K x).natDegree

Tactic:
_

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
key_equiv : (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) ≃ (f : K →ₐ[F] E) × (↥K⟮x⟯ →ₐ[K] E) :=
  id algHomEquivSigma
this✝ : ∀ (f : K →ₐ[F] E), Finite (↥K⟮x⟯ →ₐ[K] E)
this : FiniteDimensional F K
f : K →ₐ[F] E
a✝ : f ∈ Finset.univ
⊢ Nat.card (↥K⟮x⟯ →ₐ[K] E) = (minpoly K x).natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
⊢ f.Splits

Tactic:
← hu

Goal state after:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
⊢ ((UniqueFactorizationMonoid.factors f).prod * ↑u).Splits
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: case «1»
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
h : Nat.card Gal(K/F) = 1
this : 1 ≤ 2
⊢ IsCyclic Gal(K/F)

pp: case «2»
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
h : Nat.card Gal(K/F) = 2
this : 2 ≤ 2
⊢ IsCyclic Gal(K/F)

Tactic:
· exact @isCyclic_of_subsingleton _ _ (Finite.card_le_one_iff_subsingleton.mp h.le)

Goal state after:
case «2»
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
h : Nat.card Gal(K/F) = 2
this : 2 ≤ 2
⊢ IsCyclic Gal(K/F)
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L)
⊢ f ∈ ⊤ → f ⟨x, mem⟩ = ⟨x, mem⟩

Tactic:
_

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
x : K
hx : ∀ f ∈ L.fixingSubgroup, f x = x
mem : x ∈ (adjoin ↥L {x}).toIntermediateField
this : IntermediateField.fixedField ⊤ = ⊥
f : Gal(↥(adjoin ↥L {x}).toIntermediateField/↥L)
a✝ : f ∈ ⊤
⊢ f ⟨x, mem⟩ = ⟨x, mem⟩