mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorPower.Pairing

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j

pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : ¬j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j

Tactic:
· subst h
      simp only [Function.update_self]

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
i j : Fin n
v : Fin n → M
h : ¬j = i
⊢ (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j
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
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : I ^ n * (h.toFinset.erase I).inf id ^ n ≤ ann
this : ∀ K ≤ I, K ∈ ann.minimalPrimes → K = I
⊢ ¬(h.toFinset.erase I).inf id ^ n ≤ I

Tactic:
simpa [hI.isPrime.pow_le_iff hn0, hI.isPrime.inf_le', imp_not_comm, not_imp_not]

Goal state after:
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
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : 1 < s.card
⊢ False

Tactic:
← Fintype.card_coe,

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
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : 1 < Fintype.card ↥s
⊢ False
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: case neg
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}
⊢ ∃ y, N.colon {y • x} ≤ I

Tactic:
by_contra! h'

Goal state after:
case neg
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}
h' : ∀ (y : ↥K), ¬N.colon {y • x} ≤ I
⊢ False
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case right
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
ι : Type u
v : ι → M
h : Function.Bijective ⇑(linearCombination k (⇑((TensorProduct.mk R k M) 1) ∘ v))
⊢ Submodule.span R (Set.range v) = ⊤

Tactic:
refine span_eq_top_of_tmul_eq_basis _ (.mk h.1 ?_) fun _ ↦ ?_

Goal state after:
case right.refine_1
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
ι : Type u
v : ι → M
h : Function.Bijective ⇑(linearCombination k (⇑((TensorProduct.mk R k M) 1) ∘ v))
⊢ ⊤ ≤ Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))

case right.refine_2
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsLocalRing R
inst✝¹ : Module.Finite R M
inst✝ : Flat R M
ι : Type u
v : ι → M
h : Function.Bijective ⇑(linearCombination k (⇑((TensorProduct.mk R k M) 1) ∘ v))
x✝ : ι
⊢ 1 ⊗ₜ[R] v x✝ = (Basis.mk ⋯ ?right.refine_1) x✝
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝² : Free R (N ⧸ l.range)
this✝¹ : Projective R ↥l.range
this✝ : Exact ⇑l.ker.subtype ⇑(LinearMap.codRestrict l.range l ⋯)
this : (∃ l_1, LinearMap.codRestrict l.range l ⋯ ∘ₗ l_1 = LinearMap.id) ↔ ∃ l_1, l_1 ∘ₗ l.ker.subtype = LinearMap.id
⊢ ∃ l', l' ∘ₗ l.ker.subtype = LinearMap.id

Tactic:
exact this.mp (Module.projective_lifting_property _ _ (fun ⟨x, y, e⟩ ↦ ⟨y, Subtype.ext e⟩))

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case neg.refine_1
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
h : ∀ a ∈ p.primeCompl, ∀ (y : M) (k : ℕ), f y ≠ a ^ k • x
b : R
hb : b ∈ p
⊢ b ∈ (⊥.colon {g x}).radical

Tactic:
rw [hx] at hb
      refine Ideal.radical_mono (fun b hb ↦ ?_) hb
      rw [mem_colon_singleton, mem_bot] at hb ⊢
      rw [← map_smul, hb, map_zero]

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

Tactic:
rw [coeIdeal_mul, coeIdeal_span_singleton]
      rw [← mul_inv_cancel_iff_isUnit] at hI
      have ha0' := spanSingleton_mul_inv (R₁ := R) (FractionRing R)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors
          (mem_nonZeroDivisors_iff_ne_zero.mpr ha0))
      replace h :=
        congrArg
          (fun t =>
            spanSingleton R⁰ ((algebraMap R (FractionRing R)) a) * I * t)
          h.symm
      rwa [mul_mul_mul_comm, ← spanSingleton_inv, ha0', one_mul, mul_assoc, hI, mul_one] at h

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
⊢ IsEmbedding (tensorProductTo R S T)

Tactic:
refine ⟨?_, fun p₁ p₂ e ↦
    (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm
      (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
⊢ IsInducing (tensorProductTo R S T)
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
P : ClassGroup R → Prop
h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P ((mk K) I)
x : ClassGroup R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ P ↑I

Tactic:
by
    have : I = (Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv)
      (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv I) := by
      simp [← Units.val_inj]
    rw [congr_arg (QuotientGroup.mk (s := (toPrincipalIdeal R (FractionRing R)).range)) this]
    exact h _

Goal state after:
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
I : (FractionalIdeal R⁰ K)ˣ
⊢ (mk K) I = 1 ↔ (↑↑I).IsPrincipal

Tactic:
← (ClassGroup.equiv K).injective.eq_iff

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
I : (FractionalIdeal R⁰ K)ˣ
⊢ (equiv K) ((mk K) I) = (equiv K) 1 ↔ (↑↑I).IsPrincipal
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : Pic R
⊢ (mapAlgebra R R) x✝ = (MonoidHom.id (Pic R)) x✝

Tactic:
exact mapAlgebra_self_apply

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B X : Set α
M : Matroid α
⊢ ∀ ⦃I J : Set α⦄, (J ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint J B) → I ⊆ J → I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B

Tactic:
rintro I J ⟨hJE, B, hB, hJB⟩ hIJ

Goal state after:
α : Type u_1
M✝ : Matroid α
I✝ B✝ X : Set α
M : Matroid α
I J : Set α
hJE : J ⊆ M.E
B : Set α
hB : M.IsBase B
hJB : Disjoint J B
hIJ : I ⊆ J
⊢ I ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint I B
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

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

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
B' : Set α
hB' : M.IsBase B'
hI' : M.IsBasis (B' ∩ (R ∩ M.E)) (R ∩ M.E)
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
hBIB' : B ⊆ I ∪ B'
⊢ ∃ x ∈ (B' ∩ (R ∩ M.E)) \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ ¬M.RankPos ↔ M = loopyOn M.E

Tactic:
rw [rankPos_iff, not_iff_comm, empty_isBase_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
⊢ M ↾ I = freeOn I ↔ M.Indep I

Tactic:
rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
    and_iff_left Subset.rfl]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
⊢ False

Tactic:
obtain ⟨f, hf, hne⟩ := hInt.exists_ne e

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ False
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case refine_3
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hecl : e ∈ M.closure I
heI : e ∉ I
aux : ⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} ⊆ I
⊢ ∀ (f : α), (∀ t ⊆ I, e ∈ M.closure t → f ∈ t) → e ∉ M.closure (⋂₀ {J | J ⊆ I ∧ e ∈ M.closure J} \ {f})

Tactic:
exact fun f hf hecl ↦ (hf _ (sdiff_subset.trans aux) hecl).2 rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
h : M.loops = E
h' : M.E = E
⊢ M = loopyOn E

Tactic:
rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']

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

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
x✝ : M.loops = E ∧ M.E = E
h : M.loops = E
h' : M.E = E
⊢ M = loopyOn E

Tactic:
rw [← h', ← closure_empty_eq_ground_iff, ← loops, h, h']

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < C.encard
he : e ∈ C
hlp : M.IsLoop e
⊢ False

Tactic:
rw [hlp.eq_of_isCircuit_mem hC he, encard_singleton] at h

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
hC : M.IsCircuit C
h : 1 < 1
he : e ∈ C
hlp : M.IsLoop e
⊢ False
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}
⊢ M.IsNonloop f

Tactic:
rw [isNonloop_iff, and_comm]

Goal state after:
α : Type u_1
M : Matroid α
e f : α
he : M.IsNonloop e
hef : e ∈ M.closure {f}
⊢ f ∈ M.E ∧ ¬M.IsLoop f
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:
simp_rw [(M.isColoop_tfae e).out 0 4, and_iff_left he]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
hC₁ : M.IsCircuit C₁
hC₂ : M.IsCircuit C₂
h : C₁ ≠ C₂
e : α
⊢ ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit C

Tactic:
by
  have hnss : ¬ (C₁ ⊆ C₂) := fun hss ↦ h <| hC₁.eq_of_subset_isCircuit hC₂ hss
  obtain ⟨f, hf₁, hf₂⟩ := not_subset.1 hnss
  by_cases he₁ : e ∈ C₁
  · by_cases he₂ : e ∈ C₂
    · obtain ⟨C, hC, hC', -⟩ := hC₁.strong_elimination hC₂ he₁ he₂ hf₁ hf₂
      exact ⟨C, hC, hC'⟩
    exact ⟨C₂, subset_sdiff_singleton subset_union_right he₂, hC₂⟩
  exact ⟨C₁, subset_sdiff_singleton subset_union_left he₁, hC₁⟩

Goal state after:
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
he : C ∩ K = {e}
⊢ False

Tactic:
have heC : e ∈ C := (he.symm.subset rfl).1

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
he : C ∩ K = {e}
heC : e ∈ C
⊢ False
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]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
hf : Function.Injective ⇑g
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))

Tactic:
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]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
f : R[X]
g : MvPolynomial (↑s) R[X] →ₐ[R] MvPolynomial (↑s) R[X] := mapAlgHom (Polynomial.aeval f)
u : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (((supported R (insert i s)).val.comp
            ↑(((optionEquivRight R ↑s).symm.trans (renameEquiv R (Set.subtypeInsertEquivOption h).symm)).trans
                (supportedEquivMvPolynomial (insert i s)).symm)).comp
        g).comp
    ↑((optionEquivLeft R ↑s).symm.trans (optionEquivRight R ↑s))
v : (MvPolynomial (↑s) R)[X] →ₐ[R] MvPolynomial σ R :=
  (AlgHom.restrictScalars R (Polynomial.aeval ((Polynomial.aeval (X i)) f))).comp
    ↑(Polynomial.mapAlgEquiv (supportedEquivMvPolynomial s).symm)
hf : Function.Injective ⇑u
⊢ Function.Injective ⇑(Polynomial.aeval ((Polynomial.aeval (X i)) f))
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
inst✝ : IsEmpty ι
⊢ AlgebraicIndependent R x ↔ Injective ⇑(algebraMap R A)

Tactic:
algebraicIndependent_iff_injective_aeval,

Goal state after:
ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsEmpty ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(algebraMap R A)
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
hx : AlgebraicIndependent R x
a : A
⊢ (AlgebraicIndependent R fun o ↦ o.elim a x) ↔ Transcendental (↥(adjoin R (range x))) a

Tactic:
algebraicIndependent_iff_injective_aeval,

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
a : A
⊢ Injective ⇑(aeval fun o ↦ o.elim a x) ↔ Transcendental (↥(adjoin R (range x))) a
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
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i ↦ (aeval x) (f i)) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval f) p = 0
⊢ p = 0

Tactic:
exact H p (by rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero])

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
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
⊢ (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom

Tactic:
ext <;> simp [algebraMap_eq_smul_one]

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

Goal state before:
pp: case e'_2.e'_2
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set ι
⊢ sᶜᶜ = s

Tactic:
apply compl_compl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : CommSemiring F
q : ℕ
f g : F[X]
hf : IsSeparableContraction q f g
⊢ ∃ m, g.natDegree * q ^ m = f.natDegree

Tactic:
obtain ⟨m, rfl⟩ := hf.2

Goal state after:
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ ∃ m_1, g.natDegree * q ^ m_1 = ((expand F (q ^ m)) g).natDegree
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.IsBase B
hBI : B ⊆ I
⊢ M.IsBase I

Tactic:
rwa [← hB.eq_of_subset_indep hI hBI]

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

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ M = M'

Tactic:
rw [← dual_inj, ext_iff_indep, dual_ground, dual_ground, and_iff_right h]

Goal state after:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M✶.Indep I ↔ M'✶.Indep I)
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 : ι
⊢ Polynomial.C (↑hx.aevalEquiv (X i)) = Polynomial.C (hx.aevalEquiv (X i))

Tactic:
RingHom.coe_coe

Goal state after:
ι : 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 : ι
⊢ Polynomial.C (hx.aevalEquiv (X i)) = Polynomial.C (hx.aevalEquiv (X i))
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✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
⊢ #ι = trdeg R A

Tactic:
← lift_id #ι,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι : Type w
x : ι → A
hx : IsTranscendenceBasis R x
⊢ lift.{w, w} #ι = trdeg R A
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
inst✝ : NoZeroDivisors A
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ #ι = #ι'

Tactic:
← lift_id #ι,

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

Goal state before:
pp: ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ ↑(algebraicClosure (↥(adjoin R (v '' (insert i s \ {j})))) S)
this : Nontrivial R
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
← matroid_closure_eq

Goal state after:
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
this✝² : Nontrivial ↥(adjoin R (v '' (insert i s \ {j})))
this✝¹ : Nontrivial S
this✝ : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
⊢ IsTranscendenceBasis R fun x ↦ v ↑x
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
linarith only [natSepDegree_le_natDegree f, h]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
n : ℕ
⊢ (X ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
by
  simp only [natSepDegree_pow, natSepDegree_X]

Goal state after: