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

Goal state before:
pp: case refine_1
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
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
hx' : ↑I = spanSingleton R⁰ x
⊢ x ≠ 0

pp: case refine_2
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
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x ?refine_1) = ↑I

Tactic:
· intro x_eq; apply Units.ne_zero I; simp [hx', x_eq]

Goal state after:
case refine_2
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
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
hx' : ↑I = spanSingleton R⁰ x
⊢ spanSingleton R⁰ ↑(Units.mk0 x ⋯) = ↑I
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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type ?u.120} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ x ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal ↔
    x ∈ q.asIdeal

Tactic:
rw [← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), iff_comm,
      ← Ideal.IsPrime.mul_mem_left_iff (x := algebraMap _ _ r), ← Algebra.smul_def, e]

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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ 1 ⊗ₜ[R] s ∈ q.asIdeal ↔
    1 ⊗ₜ[R] s ∈
      ((fun q ↦
            {
              asIdeal :=
                RingHom.ker
                  (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                      (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
              isPrime := ⋯ })
          ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal

R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ q.asIdeal

R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉
    ((fun q ↦
          {
            asIdeal :=
              RingHom.ker
                (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                    (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
            isPrime := ⋯ })
        ((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩) q)).asIdeal
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : Group.IsSolvable (Perm X)
⊢ ↑5 ≤ Cardinal.lift.{?u.26, u_3} (Cardinal.mk X)

Tactic:
Cardinal.lift_id

Goal state after:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : Group.IsSolvable (Perm X)
⊢ ↑5 ≤ Cardinal.mk X
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
⊢ rankAtStalk M = 0 ↔ Subsingleton M

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ rankAtStalk_eq_zero_of_subsingleton⟩
  simp_rw [← support_eq_empty_iff (R := R), Set.eq_empty_iff_forall_notMem]
  intro p
  rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_apply]

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✝¹ : Flat R N
inst✝ : Module.Finite R N
⊢ rankAtStalk (M × N) = rankAtStalk M + rankAtStalk N

Tactic:
by
  ext p
  let e : LocalizedModule p.asIdeal.primeCompl (M × N) ≃ₗ[Localization.AtPrime p.asIdeal]
      LocalizedModule p.asIdeal.primeCompl M × LocalizedModule p.asIdeal.primeCompl N :=
    IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap _ _)
      (.prodMap (mkLinearMap _ M) (mkLinearMap _ N)) |>.extendScalarsOfIsLocalization
      p.asIdeal.primeCompl _
  simp [rankAtStalk, e.finrank_eq]

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.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

Tactic:
lTensor_surjective_iff

Goal state after:
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.Surjective ⇑f ↔ Function.Surjective ⇑f
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.Injective ⇑f ∧ Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f

Tactic:
lTensor_surjective_iff

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
A : Type u_4
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
inst✝³ : Module.Invertible R M
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Module.Invertible R A
inv : A →ₗ[R] R :=
  ↑(linearEquiv R A) ∘ₗ LinearMap.lTensor (Dual R A) (LinearMap.mul' R A) ∘ₗ ↑(leftCancelEquiv A (linearEquiv R A)).symm
s : Finset (Dual R A × A)
hs : (linearEquiv R A).symm 1 = ∑ i ∈ s, i.1 ⊗ₜ[R] i.2
⊢ (inv ∘ₗ Algebra.linearMap R A) 1 = LinearMap.id 1

Tactic:
by simp [inv, hs, sum_tmul, map_sum, ← (LinearEquiv.symm_apply_eq _).1 hs]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset
  have hcard := hB'.encard_sdiff_comm hB
  rw [insert_subset_iff, ← sdiff_eq_empty, sdiff_sdiff_comm, sdiff_eq_empty,
    subset_singleton_iff_eq] at hIB'
  obtain ⟨hfB, (h | h)⟩ := hIB'
  · rw [h, encard_empty, encard_eq_zero, eq_empty_iff_forall_notMem] at hcard
    exact (hcard f ⟨hfB, hf⟩).elim
  rw [h, encard_singleton, encard_eq_one] at hcard
  obtain ⟨x, hx⟩ := hcard
  obtain (rfl : f = x) := hx.subset ⟨hfB, hf⟩
  simp_rw [← h, ← singleton_union, ← hx, _root_.sdiff_sdiff_right_self, inf_eq_inter, inter_comm B,
    sdiff_union_inter]
  exact hB'

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
⊢ ∀ X ⊆ E, ExistsMaximalSubsetProperty Indep X

Tactic:
simp_rw [hE, show Indep = M.Indep from funext (by simp [hI])]

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
⊢ ∀ X ⊆ M.E, ExistsMaximalSubsetProperty M.Indep X
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Tactic:
rw [IsBasis, maximal_subset_iff]
  tauto

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 : Finset α
⊢ (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I

Tactic:
simp only [IndepMatroid.ofFinset]

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 : Finset α
⊢ (IndepMatroid.ofFinitaryCardAugment E (fun I ↦ ∀ (J : Finset α), ↑J ⊆ I → Indep J) ⋯ ⋯ ⋯ ⋯ ⋯).Indep ↑I ↔ Indep I
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
hf : InjOn f (f ⁻¹' N.E)
⊢ (N.comap f).Indep I ↔ N.Indep (f '' I)

Tactic:
by
  rw [comap_indep_iff, and_iff_left_iff_imp]
  refine fun hi ↦ hf.mono <| subset_trans ?_ (preimage_mono hi.subset_ground)
  apply subset_preimage_image

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
⊢ e ∈ M.loops

Tactic:
convert! hef using 1

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
h : f ∈ M.E → f ∈ M.loops
⊢ M.loops = M.closure {f}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk (X ∪ {e}) = M.eRk (insert e X)

Tactic:
union_singleton

Goal state after:
α : Type u_1
M : Matroid α
e : α
X : Set α
⊢ M.eRk (insert e X) = M.eRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
⊢ M.eRk (X ∪ {e}) = M.eRk (insert e X)

Tactic:
union_singleton

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
⊢ M.eRk (insert e X) = M.eRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis' I X
e : α
⊢ M.eRk (insert e I) = M.eRk (insert e X)

Tactic:
by
  rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (X ∪ {e}) = M.eRk (insert e X)

Tactic:
union_singleton

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (insert e X) = M.eRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIX : M.IsBasis I X
e : α
⊢ M.eRk (insert e I) = M.eRk (insert e X)

Tactic:
by
  rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X.Finite
hXE : X ⊆ M.E
⊢ M.eRk X < X.encard ↔ M.Dep X

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ eRk_lt_encard_of_dep_of_finite hX h⟩
  rw [← not_indep_iff, indep_iff_eRk_eq_encard_of_finite hX]
  exact h.ne

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ ∀ (x : α), (∀ (t : Set α), M.IsFlat t → X ∩ M.E ⊆ t → x ∈ t) ↔ x ∈ M.E ∧ ∀ a ⊆ M.E, X ∩ M.E ⊆ a → M.IsFlat a → x ∈ a

Tactic:
exact fun x ↦ ⟨fun h ↦ ⟨h _ M.ground_isFlat inter_subset_right, fun F _ hXF hF ↦ h F hF hXF⟩,
    fun ⟨_, h⟩ F hF hXF ↦ h F hF.subset_ground hXF hF⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ M.closure X ∪ {e} = insert e (M.closure X)

Tactic:
union_singleton

Goal state after:
α : Type u_1
M : Matroid α
e : α
X : Set α
he : M.IsColoop e
⊢ insert e (M.closure X) = insert e (M.closure X)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
I X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis' I X
⊢ #↑I = M.cRk X

Tactic:
by
  rw [cRk, (isBase_restrict_iff'.2 hIX).cardinalMk_eq_cRank]

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

Goal state before:
pp: α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (X ∪ {e}) = M.cRk (insert e X)

Tactic:
union_singleton

Goal state after:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (insert e X) = M.cRk (insert e X)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ C ∩ K ≠ {e}

Tactic:
by
  intro he
  have heC : e ∈ C := (he.symm.subset rfl).1
  simp_rw [isCocircuit_iff_minimal_compl_nonspanning, minimal_iff_forall_ssubset, not_not] at hK
  have' hKe := hK.2 (t := K \ {e}) (sdiff_singleton_ssubset.2 (he.symm.subset rfl).2)
  apply hK.1
  rw [spanning_iff_ground_subset_closure]
  nth_rw 1 [← hKe.closure_eq, sdiff_sdiff_eq_sdiff_union]
  · refine (M.closure_subset_closure (subset_union_left (t := C))).trans ?_
    rw [union_assoc, singleton_union, insert_eq_of_mem heC, ← closure_union_congr_right
      (hC.closure_sdiff_singleton_eq e), union_eq_self_of_subset_right]
    rw [← he, sdiff_self_inter]
    exact sdiff_subset_sdiff_left hC.subset_ground
  rw [← he]
  exact inter_subset_left.trans hC.subset_ground

Goal state after:
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
hf : Transcendental R f
⊢ Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)

Tactic:
classical
  rw [transcendental_iff_injective] at hf ⊢
  let g := MvPolynomial.mapAlgHom (R := R) (σ := s) (Polynomial.aeval (R := R) f)
  replace hf : Function.Injective g := MvPolynomial.map_injective _ hf
  let u := (Subalgebra.val _).comp
    ((optionEquivRight R s).symm |>.trans
      (renameEquiv R (Set.subtypeInsertEquivOption h).symm) |>.trans
      (supportedEquivMvPolynomial _).symm).toAlgHom |>.comp
    g |>.comp
    ((optionEquivLeft R s).symm.trans (optionEquivRight R s)).toAlgHom
  let v := ((Polynomial.aeval (R := supported R s)
    (Polynomial.aeval (X i : MvPolynomial σ R) f)).restrictScalars R).comp
      (Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm).toAlgHom
  replace hf : Function.Injective u := by
    simp only [AlgHom.coe_comp, Subalgebra.coe_val,
      AlgEquiv.coe_toAlgHom, AlgEquiv.coe_trans, Function.comp_assoc, u]
    apply Subtype.val_injective.comp
    simp only [EquivLike.comp_injective]
    apply hf.comp
    simp only [EquivLike.comp_injective, EquivLike.injective]
  have h1 : Polynomial.aeval (X i : MvPolynomial σ R) = ((Subalgebra.val _).comp
      (supportedEquivMvPolynomial _).symm.toAlgHom |>.comp
      (Polynomial.aeval (X ⟨i, s.mem_insert i⟩ : MvPolynomial ↑(insert i s) R))) := by
    ext1; simp
  have h2 : u = v := by
    simp only [u, v, g]
    ext1
    · ext1
      simp [Set.subtypeInsertEquivOption, Subalgebra.algebraMap_eq, optionEquivLeft_symm_apply]
    · simp [Set.subtypeInsertEquivOption, h1, optionEquivLeft_symm_apply]
  simpa only [h2, v, AlgHom.coe_comp, AlgEquiv.coe_toAlgHom,
    EquivLike.injective_comp, AlgHom.coe_restrictScalars'] using hf

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ M.Indep M.E

Tactic:
indep_iff_forall_subset_not_isCircuit

Goal state after:
α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ (M ↾ X).RankFinite ↔ M.cRk X < ℵ₀

Tactic:
rankFinite_iff_cRank_lt_aleph0,

Goal state after:
α : Type u
M : Matroid α
X : Set α
⊢ (M ↾ X).cRank < ℵ₀ ↔ M.cRk X < ℵ₀
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
X : Set α
⊢ toENat (M.cRk X) = M.eRk X

Tactic:
rw [cRk, toENat_cRank_eq, eRk]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ AlgebraicIndependent R x ↔ (AlgebraicIndependent R fun i ↦ x ↑i) ∧ AlgebraicIndepOn (↥(adjoin R (x '' sᶜ))) x s

Tactic:
by
  convert! ← iff_adjoin_image _; apply compl_compl

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f X ∩ M.E)
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)

Tactic:
rw [insert_inter_of_mem hfE] at hef

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∉ M.closure (X ∩ M.E)
hef : e ∈ M.closure (insert f (X ∩ M.E))
hfE : f ∈ M.E
heE : e ∈ M.E
⊢ f ∈ M.closure (insert e X ∩ M.E)
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
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i ↦ ↑i) → s.card ≤ n
⊢ ∀ (s : Set A), AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n

Tactic:
intro s li

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
H : ∀ (s : Finset A), (AlgebraicIndependent R fun i ↦ ↑i) → s.card ≤ n
s : Set A
li : AlgebraicIndependent R Subtype.val
⊢ Cardinal.mk ↑s ≤ ↑n
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
s : { s // AlgebraicIndepOn R _root_.id s }
⊢ #↑↑s ≤ ⨆ ι, #↑↑ι

Tactic:
choose t ht using exists_isTranscendenceBasis_superset s.2

Goal state after:
R : Type u_1
A : Type w
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : { s // AlgebraicIndepOn R _root_.id s }
t : Set A
ht : ↑s ⊆ t ∧ IsTranscendenceBasis R Subtype.val
⊢ #↑↑s ≤ ⨆ ι, #↑↑ι
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
A : Type w
x : ι → A
y : ι' → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'

Tactic:
rw [← lift_inj.{_, w}, lift_lift, lift_lift, ← lift_lift.{w, u'}, hx.lift_cardinalMk_eq_trdeg,
    ← lift_lift.{w, u}, hy.lift_cardinalMk_eq_trdeg, lift_lift, lift_lift]

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G), ∀ i ∈ B.toFilterBasis, a ∈ (fun y ↦ a * y) '' id i

Tactic:
intro a U U_in

Goal state after:
case hpure
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ B.toFilterBasis
⊢ a ∈ (fun y ↦ a * y) '' id U
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ : G
⊢ ∀ (a : G),
    ∀ i ∈ B.toFilterBasis,
      ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id i ∈ map (fun y ↦ x * y) B.filter

Tactic:
intro a U U_in

Goal state after:
case hopen
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
x₀ a : G
U : Set G
U_in : U ∈ B.toFilterBasis
⊢ ∀ᶠ (x : G) in map (fun y ↦ a * y) B.filter, (fun y ↦ a * y) '' id U ∈ map (fun y ↦ x * y) B.filter
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_4
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ (x₀ : G), Tendsto (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)

Tactic:
intro x₀
    rw [basis.tendsto_iff basis]
    intro U U_in
    exact conj x₀ U_in

Goal state after:
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
⊢ finInsepDegree F E = finInsepDegree F K

Tactic:
by
  simpa only [Cardinal.toNat_lift] using! congr_arg Cardinal.toNat
    (lift_insepDegree_eq_of_equiv F E K i)

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

Goal state before:
pp: case h_splits
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
⊢ Polynomial.map (↑f) (minpoly K x) ∣ Polynomial.map (↑f) (Polynomial.map (algebraMap F K) p)

Tactic:
Polynomial.map_dvd_map'

Goal state after:
case h_splits
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
⊢ minpoly K x ∣ Polynomial.map (algebraMap F K) p
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set Gal(L/K)
⊢ s ∈ 𝓝 1 ↔ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

Tactic:
GroupFilterBasis.nhds_one_eq

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
s : Set Gal(L/K)
⊢ s ∈ (galGroupBasis K L).filter ↔ ∃ E, FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s