mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R ↑s) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
i : ↥K
hi : i ∈ ↑s
⊢ z • (Submodule.subtype K) i • x ∈ N

Tactic:
← mem_colon_singleton

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R ↑s) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
i : ↥K
hi : i ∈ ↑s
⊢ z ∈ N.colon {(Submodule.subtype K) i • x}
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : f y = a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {y}).radical
n : ℕ
hb : (b ^ n * a ^ k) • x ∈ ⊥
⊢ b ∈ p

Tactic:
← mem_colon_singleton

Goal state after:
case pos.refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
M'' : Type u_4
inst✝¹ : AddCommMonoid M''
inst✝ : Module R M''
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
p : Ideal R
toIsPrime✝ : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : f y = a ^ k • x
b : R
x✝ : b ∈ (⊥.colon {y}).radical
n : ℕ
hb : b ^ n * a ^ k ∈ ⊥.colon {x}
⊢ b ∈ p
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
hJ : ∃ K, J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
⊢ Submodule.IsPrincipal J

Tactic:
obtain ⟨K, hJK0, hK⟩ := hJ

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)
⊢ Submodule.IsPrincipal J
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y} * ⊤
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}

Tactic:
Ideal.mul_top

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * I' = Ideal.span {y}
⊢ ∃ x, x ≠ 0 ∧ I' = Ideal.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))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ Ideal.span {x} = Ideal.span {x} * ⊤

Tactic:
Ideal.mul_top

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ Ideal.span {x} = Ideal.span {x}
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J

Tactic:
refine ⟨IsLocalization.mk' _ x ⟨y, hy'⟩, ?_, ?_⟩

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ mk' (FractionRing R) x ⟨y, hy'⟩ ≠ 0

case refine_2.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hx : x ≠ 0
hy : y ≠ 0
h : Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
hy' : y ∈ R⁰
⊢ spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy'⟩) * ↑↑I = ↑↑J
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: 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
inst✝ : Subsingleton (ClassGroup R)
I : Ideal R
hI : IsUnit ↑I
⊢ Submodule.IsPrincipal I

Tactic:
have hsub :
      ((I : FractionalIdeal R⁰ K) : Submodule R K).IsPrincipal :=
    ClassGroup.isPrincipal_coeSubmodule_of_isUnit (I := (I : FractionalIdeal R⁰ K)) hI

Goal state after:
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
inst✝ : Subsingleton (ClassGroup R)
I : Ideal R
hI : IsUnit ↑I
hsub : (↑↑I).IsPrincipal
⊢ Submodule.IsPrincipal I
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
inst✝⁶ : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → AddCommMonoid (M' i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → Module R (M' i)
inst✝¹ : (i : ι) → Module S (M' i)
inst✝ : ∀ (i : ι), IsScalarTower R S (M' i)
f : (i : ι) → M i →ₗ[R] M' i
hf : ∀ (i : ι), IsBaseChange S (f i)
⊢ IsBaseChange S (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)

Tactic:
cases nonempty_fintype ι
  apply of_equiv <| piRight R S _ M ≪≫ₗ .piCongrRight fun i ↦ (hf i).equiv
  intro x
  ext i
  simp [equiv_tmul]

Goal state after:
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 : derivedSeries (↥⁅H, H⁆) n = ⊥
⊢ derivedSeries (↥H) (n + 1) = ⊥

Tactic:
← map_subtype_inj,

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, H⁆.subtype ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map H.subtype ⊥
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 : derivedSeries (↥⁅H, H⁆) n = ⊥
⊢ derivedSeries (↥H) (n + 1) = ⊥

Tactic:
rw [← map_subtype_inj, Subgroup.map_bot] at 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)) = ⊥
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G n.succ = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

Tactic:
· rwa [h]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
⊢ Function.Injective ⇑(rTensorInv P Q e)

Tactic:
simpa [rTensorInv] using (rTensorInv_leftInverse _ _ <| TensorProduct.comm R N M ≪≫ₗ e).injective

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Bijective ⇑(LinearMap.rTensor M f) ↔ Function.Bijective ⇑f

Tactic:
by
  simp_rw [Function.Bijective, rTensor_injective_iff, rTensor_surjective_iff]

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
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯

Tactic:
have hα := Algebra.IsSeparable.isIntegral F α

Goal state after:
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 α
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
ne : Nonempty (K →ₐ[F] L)
h : Normal F L
⊢ normalClosure F K L = ⨆ x, adjoin F ((minpoly F x).rootSet L)

Tactic:
by
  have ⟨φ⟩ := ne
  refine h.toIsAlgebraic.of_injective φ φ.injective
    |>.normalClosure_eq_iSup_adjoin_of_splits fun x ↦ ?_
  rw [← minpoly.algHom_eq _ φ.injective]
  apply h.splits

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

Goal state before:
pp: case inl
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
he : B₂ \ B₁ = ∅
⊢ (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

Tactic:
exch.antichain hB₂ hB₁ (sdiff_eq_empty.mp he)

Goal state after:
case inl
α : Type u_1
IsBase : Set α → Prop
B₁ B₂ : Set α
exch : ExchangeProperty IsBase
hB₁ : IsBase B₁
hB₂ : IsBase B₂
he : B₂ \ B₁ = ∅
⊢ (B₁ \ B₁).encard ≤ (B₁ \ B₁).encard
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: case pos
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

pp: case neg
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I

Tactic:
· rwa [h]

Goal state after:
case neg
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h : ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)
I : Set α
hI : ¬I ⊆ M₁.E
⊢ M₁.Indep I ↔ M₂.Indep I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard + 1 ≤ B'.ncard
⊢ False

Tactic:
hB'.ncard_eq_ncard_of_isBase hB,

Goal state after:
α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : B.ncard + 1 ≤ B.ncard
⊢ False
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp.refine_2
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)ˣ
h✝ : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
this : R ∙ ↑(e' 1) * ↑(e 1) = 1
r : Rˣ
hr : ↑(e' 1) * ↑(e 1) = (algebraMap R A) ↑r
⊢ ∃ c, c * (↑e 1).1 = 1

Tactic:
exact ⟨algebraMap R A r.inv * e' 1, by simp [mul_assoc, hr, ← map_mul]⟩

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

Goal state before:
pp: α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), IsBase B → B ⊆ E

Tactic:
simp_rw [hE, hB]

Goal state after:
α : Type u_1
M✝ M : Matroid α
E : Set α
IsBase Indep : Set α → Prop
hE : E = M.E
hB : ∀ (B : Set α), IsBase B ↔ M.IsBase B
hI : ∀ (I : Set α), Indep I ↔ M.Indep I
⊢ ∀ (B : Set α), M.IsBase B → B ⊆ M.E
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ finrank F ↥F⟮α⟯ = finrank F ↥⊤

Tactic:
refine ⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩

Goal state after:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
h : F⟮α⟯ = ⊤
⊢ finrank F ↥F⟮α⟯ = finrank F ↥⊤
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
⊢ B ∈ {B | M✶.IsBase B} ↔ B ∈ (fun X ↦ M.E \ X) '' {B | M.IsBase B}

Tactic:
simp only [mem_ofPred_eq, mem_image, dual_isBase_iff']

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ x, M.IsBase x ∧ M.E \ x = B
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
⊢ M₁ = M₂✶ ↔ M₂ = M₁✶

Tactic:
rw [← dual_inj, dual_dual, eq_comm]

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

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
R I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ : Matroidᵣ α
⊢ M₁.toMatroid ≤r M₂.toMatroid → M₂.toMatroid ≤r M₁.toMatroid → M₁ = M₂

Tactic:
by
    rintro ⟨R, hR, h⟩ ⟨R', hR', h'⟩
    rw [h', restrict_ground_eq] at hR
    rw [h, restrict_ground_eq] at hR'
    rw [← Matroidᵣ.coe_inj, h, h', hR.antisymm hR', restrict_idem]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (M.mapEquiv f).IsBasis I X ↔ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)

Tactic:
rw [mapEquiv_eq_map, map_isBasis_iff']

Goal state after:
α : Type u_3
β : Type u_4
M : Matroid α
f : α ≃ β
I X : Set β
⊢ (∃ I₀ X₀, M.IsBasis I₀ X₀ ∧ I = ⇑f '' I₀ ∧ X = ⇑f '' X₀) ↔ M.IsBasis (⇑f.symm '' I) (⇑f.symm '' X)
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ M.IsNonloop e

Tactic:
rw [← not_isLoop_iff (hI.subset_ground h)]; exact fun he ↦ (he.notMem_of_indep hI) h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk X + M.eRk Y ≤ X.encard + M.eRk Y

Tactic:
grw [M.eRk_le_encard]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C

Tactic:
(M.isColoop_tfae e).out 0 4,

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : K ⊆ M.coloops
⊢ M.closure X ∩ K = X ∩ K

Tactic:
nth_rw 1 [← inter_eq_self_of_subset_right hK]
  rw [← inter_assoc, closure_inter_coloops_eq, inter_assoc, inter_eq_self_of_subset_right hK]

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

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

Tactic:
insert_eq_of_mem heI

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I
Module: Mathlib.Combinatorics.Matroid.Closure

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

Tactic:
by
  rw [mem_sdiff, hI.mem_closure_iff_of_notMem heI, dep_iff, not_and, not_imp_not, insert_subset_iff,
    and_iff_left hI.subset_ground]
  exact ⟨fun h ↦ ⟨h.subset_ground (mem_insert e I), fun _ ↦ h⟩, fun h ↦ h.2 h.1⟩

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
hNM : N ≤r M
inst✝ : N.Loopless
⊢ N ≤r M.removeLoops

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM.exists_eq_restrict

Goal state after:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
hNM : M ↾ R ≤r M
inst✝ : (M ↾ R).Loopless
⊢ M ↾ R ≤r M.removeLoops
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ M.Indep (J ∪ I) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)

Tactic:
hJ.union_indep_iff_forall_notMem_closure_right hI,

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
⊢ (∀ e ∈ I \ J, e ∉ M.closure (J ∪ I \ {e})) ↔ ∀ e ∈ I \ J, e ∉ M.closure (I \ {e} ∪ J)
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
⊢ trdeg R A = trdeg R A'

Tactic:
rw [← (trdeg R A).lift_id, e.lift_trdeg_eq, lift_id]

Goal state after:
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
hx : AlgebraicIndependent R x
i : ι
⊢ hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i)) = Polynomial.C (hx.aevalEquiv (X i))

Tactic:
rw [AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, aeval_X, Option.elim,
    Polynomial.map_C, RingHom.coe_coe]

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

Goal state before:
pp: case refine_2.none
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X none)) = (aeval fun o ↦ o.elim a x) (X none)

pp: case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i))) =
    (aeval fun o ↦ o.elim a x) (X (some i))

Tactic:
· rw [hx.mvPolynomialOptionEquivPolynomialAdjoin_X_none, aeval_X, Polynomial.aeval_X,
        Option.elim]

Goal state after:
case refine_2.some
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
i : ι
⊢ (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i))) =
    (aeval fun o ↦ o.elim a x) (X (some i))
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : Set α
x y : M
hx : x ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
hy : y ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
z : ↑s
⊢ x • ↑z = ↑z

Tactic:
hx z

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M α
s : Set α
x y : M
hx : x ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
hy : y ∈ {ϕ | ∀ (x : ↑s), ϕ • ↑x = ↑x}
z : ↑s
⊢ ↑z = ↑z
Module: Mathlib.GroupTheory.GroupAction.FixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
x✝ : M
hx : x✝ ∈ (fixingSubmonoid M s).carrier
z : ↑s
⊢ ↑z = x✝ • ↑z

Tactic:
hx z

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
x✝ : M
hx : x✝ ∈ (fixingSubmonoid M s).carrier
z : ↑s
⊢ ↑z = ↑z
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: 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 A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
← hs.cardinalMk_eq_trdeg,

Goal state after:
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 A
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis R Subtype.val
t : Set A
ht : IsTranscendenceBasis S Subtype.val
this✝ : NoZeroDivisors S
this : Nontrivial S
⊢ lift.{w, v} #{ x // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f g : F[X]
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
by_cases h : f * g = 0
  · simp only [h, natSepDegree_zero, zero_le]
  classical
  simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
⊢ f.natSepDegree ∣ f.natDegree

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
⊢ f.natSepDegree ∣ f.natDegree
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
⊢ ∃ n y, f = (expand F (q ^ n)) (X - C y)

Tactic:
obtain ⟨g, h1, n, rfl⟩ := hi.hasSeparableContraction q
    have h2 : g.natDegree = 1 := by
      rwa [natSepDegree_expand _ q, h1.natSepDegree_eq_natDegree] at h
    rw [((monic_expand_iff <| expChar_pow_pos F q n).mp hm).eq_X_add_C h2]
    exact ⟨n, -(g.coeff 0), by rw [map_neg, sub_neg_eq_add]⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ Module.rank (↥(separableClosure F F)) F = 1

Tactic:
Subsingleton.elim (separableClosure F F) ⊤,

Goal state after:
F : Type u
inst✝ : Field F
⊢ Module.rank (↥⊤) F = 1
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case h
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (algebraMap F E) y = x ^ q ^ n
⊢ X ^ q ^ n - C x ^ q ^ n = (X - C x) ^ q ^ n

Tactic:
← sub_pow_expChar_pow_of_commute _ _ (commute_X _)

Goal state after:
case h
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
h✝ : (minpoly F x).natSepDegree = 1
n : ℕ
y : F
h : minpoly F x = X ^ q ^ n - C y
hx : (algebraMap F E) y = x ^ q ^ n
⊢ (X - C x) ^ q ^ n = (X - C x) ^ q ^ n