mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case e'_5
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ i ∈ Finset.map (↑e).toEmbedding (support x) with i.1 = i, (monomial (e.symm i)) (coeff (e.symm i) x) =
    (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x))

pp: case a.convert_4
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x)) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker

Tactic:
· rw [map_sum, Finset.mul_sum]
      refine Finset.sum_congr rfl fun j hj ↦ ?_
      obtain rfl := (Finset.mem_filter.mp hj).2
      obtain ⟨i, j⟩ := j
      clear hj hi
      have : (Q.toComp P).toAlgHom (monomial j (coeff (e.symm (i, j)) x)) =
          monomial (e.symm (0, j)) (coeff (e.symm (i, j)) x) :=
        toComp_toAlgHom_monomial ..
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
          this]
      rw [monomial_mul, ← map_add, Prod.mk_add_mk, add_zero, zero_add, one_mul]

Goal state after:
case a.convert_4
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ (monomial (e.symm (i, 0))) 1 *
      (Q.toComp P).toAlgHom.toRingHom
        (∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x)) ∈
    Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type w
P : Generators R S ι
σ : Type u_1
u : σ → ι
hu : Function.Injective u
x : ↥P.ker
j : σ
⊢ (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (D R P.toExtension.Ring) ↑x)) (u j) =
    (aeval P.val) ((pderiv (u j)) ↑x)

Tactic:
simp only [toExtension_Ring, P.cotangentSpaceBasis_repr_tmul, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case inl
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
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
h✝ : Flat R ↥M
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
exact H.linearIndependent_mul_of_flat_left hm hn

Goal state after:
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
⊢ (LinearMap.codRestrict l.range l ⋯).ker = l.ker.subtype.range

Tactic:
LinearMap.ker_rangeRestrict,

Goal state after:
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
⊢ l.ker = l.ker.subtype.range
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 ∈ ⊥.colon {y}
⊢ b ∈ p

Tactic:
rw [mem_colon_singleton, mem_bot] at hb
      apply_fun f at hb
      rw [map_smul, map_zero, h, ← mul_smul, ← mem_bot R, ← mem_colon_singleton] at hb
      replace hb := hx.ge (Ideal.le_radical hb)
      contrapose hb
      exact p.primeCompl.mul_mem (p.primeCompl.pow_mem hb n) (p.primeCompl.pow_mem ha k)

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
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M

Tactic:
have hp' : S ≤ p'.primeCompl := fun x hx H ↦
    p.isPrime.ne_top (Ideal.eq_top_of_isUnit_mem _ H (IsLocalization.map_units _ ⟨x, hx⟩))

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case inr
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
h : Normal F L
φ : Nonempty (K →ₐ[F] L)
⊢ Normal F ↥(normalClosure F K L)

Tactic:
· exact (isNormalClosure_normalClosure F K L).normal

Goal state after:
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
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
⊢ Nonempty (↥(IntermediateField.adjoin F (⨆ x, (minpoly F x).rootSet L')) →ₐ[F] L)

Tactic:
refine nonempty_algHom_adjoin_of_splits fun x hx ↦ ?_

Goal state after:
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
inst✝² : Algebra.IsAlgebraic F K
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
x : L'
hx : x ∈ ⨆ x, (minpoly F x).rootSet L'
⊢ IsIntegral F x ∧ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B B₁ : Set α
hB : M.IsBase B
h : B.Infinite
hB₁ : M.IsBase B₁
⊢ B₁.Infinite

Tactic:
contrapose! h; exact hB₁.finite_of_finite h hB

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankInfinite
⊢ ¬M.RankFinite

Tactic:
by
  intro h; obtain ⟨B, hB⟩ := M.exists_isBase; exact hB.infinite hB.finite

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

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
⊢ ¬M.RankInfinite

Tactic:
by
  intro h; obtain ⟨B, hB⟩ := M.exists_isBase; exact hB.infinite hB.finite

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

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

Tactic:
by
    ext I
    by_cases hI : I ⊆ M₁.E
    · rwa [h]
    exact iff_of_false (fun hi ↦ hI hi.subset_ground)
      (fun hi ↦ hI (hi.subset_ground.trans_eq hE.symm))

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
    exact ⟨hIJ.trans hJE, ⟨B, hB, disjoint_of_subset_left hIJ hJB⟩⟩

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
A : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring A
inst✝² : Algebra R A
e : A ⊗[R] M ≃ₗ[A] A
inst✝¹ : Flat R M
inst✝ : FaithfulSMul R A
⊢ ⊤ * submoduleAlgebra e = ⊤

Tactic:
by
  rw [← Submodule.mulMap_range]
  convert!
    (Submodule.topEquiv.rTensor _ ≪≫ₗ (tensorSubmoduleAlgebraEquiv e).restrictScalars R).range
  ext; rfl

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

Goal state before:
pp: α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
⊢ uniqueBaseOn (I ∩ E ∩ R) R = uniqueBaseOn (I ∩ R) R

Tactic:
inter_eq_self_of_subset_left h

Goal state after:
α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
⊢ uniqueBaseOn (I ∩ R) R = uniqueBaseOn (I ∩ R) R
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
⊢ M✶.Indep (M.E \ B ∩ (M.E \ X))

pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))

Tactic:
· rw [dual_indep_iff_exists]
    exact ⟨B, hB, disjoint_of_subset_left inter_subset_left disjoint_sdiff_left⟩

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : e ∈ (M.E \ X) \ (M.E \ B ∩ (M.E \ X))
⊢ M✶.Dep (insert e (M.E \ B ∩ (M.E \ X)))
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
hI : M.IsBasis' I X
hJ : M.IsBasis' J X
⊢ I.encard = J.encard

Tactic:
rw [← isBase_restrict_iff'] at hI hJ; exact hI.encard_eq_encard_of_isBase hJ

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

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

Tactic:
choose Is hIs using fun i ↦ M.exists_isBasis' (Xs i)
  have hfin : (⋃ i, Is i).Finite := finite_iUnion <| fun i ↦ (h i).finite_of_isBasis' (hIs i)
  refine isRkFinite_inter_ground_iff.1 <| (M.isRkFinite_of_finite hfin).closure.subset ?_
  rw [iUnion_inter, iUnion_subset_iff]
  exact fun i ↦ (hIs i).isBasis_inter_ground.subset_closure.trans <| M.closure_subset_closure <|
    subset_iUnion ..

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ Minimal M.Dep C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

Tactic:
minimal_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M.Dep C ∧ ∀ ⦃t : Set α⦄, M.Dep t → t ⊆ C → C = t) ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
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})
⊢ M.IsCircuit (insert e I)

Tactic:
refine hI.insert_isCircuit_of_forall (fun heI ↦ ?_) he h

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
⊢ False
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
⊢ M.eRk (X ∩ R) = M.eRk X

Tactic:
inter_eq_self_of_subset_left h

Goal state after:
α : Type u_1
X : Set α
M : Matroid α
R : Set α
h : X ⊆ R
⊢ M.eRk X = M.eRk X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
⊢ M.eRk (M.E \ (X ∪ Y)) + M.eRk (M.E \ (X ∩ Y)) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)

Tactic:
by
  rw [← sdiff_inter_sdiff, sdiff_inter]
  apply M.eRk_submod

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.subtypeClosure ⟨⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E, ⋯⟩ = M.subtypeClosure ⟨⋃ i, Xs i ∩ M.E, ⋯⟩

Tactic:
convert! M.subtypeClosure.closure_iSup_closure (fun i ↦ ⟨Xs i ∩ M.E, inter_subset_right⟩) <;>
  simp [← iUnion_inter, subtypeClosure]

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
h : ∀ (C : Set α), M.IsCircuit C → C.Finite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
x : α
hx : x ∈ I
⊢ x ∈ M.E

Tactic:
simpa using (hI {x} (by simpa) (finite_singleton _)).subset_ground

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

Goal state before:
pp: case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ True ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

Tactic:
true_iff,

Goal state after:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
h : e ∈ I
⊢ e ∈ M.E \ M.closure I ∨ e ∈ I
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ Minimal (fun X ↦ ¬M.Spanning (M.E \ X)) (M.E \ M.closure (B \ {e}))

Tactic:
minimal_subset_iff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
⊢ ¬M.Spanning (M.E \ (M.E \ M.closure (B \ {e}))) ∧
    ∀ ⦃t : Set α⦄, ¬M.Spanning (M.E \ t) → t ⊆ M.E \ M.closure (B \ {e}) → M.E \ M.closure (B \ {e}) = t
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
isCocircuit_iff_minimal_compl_nonspanning

Goal state after:
α : Type u_1
M : Matroid α
K : Set α
⊢ Minimal (fun X ↦ ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
hCK : (C ∩ K).Nonempty
⊢ (C ∩ K).Nontrivial

Tactic:
obtain ⟨e, heCK⟩ := hCK
  rw [nontrivial_iff_ne_singleton heCK]
  exact hC.inter_isCocircuit_ne_singleton hK

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
⊢ ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)

Tactic:
by
  obtain ⟨I, hI⟩ := M.exists_isBasis (X ∩ M.E)
  have hI' := hI.isBasis_closure_right; rw [closure_inter_ground] at hI'
  exact ⟨_, hI, hI'⟩

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
ι' : Type u_4
y : ι' → A
hx : ¬AlgebraicIndependent R x
h : AlgebraicIndependent R (Sum.elim y x)
⊢ AlgebraicIndependent R x

Tactic:
apply h.comp _ Sum.inr_injective

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

Goal state before:
pp: α : Type u_2
M : Matroid α
B R : Set α
hR : R ⊆ M.E
hN : M.Spanning (M ↾ R).E
⊢ (M ↾ R).IsBase B ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E

Tactic:
Spanning.isBase_restrict_iff (show M.Spanning R from hN),

Goal state after:
α : Type u_2
M : Matroid α
B R : Set α
hR : R ⊆ M.E
hN : M.Spanning (M ↾ R).E
⊢ M.IsBase B ∧ B ⊆ R ↔ M.IsBase B ∧ B ⊆ (M ↾ R).E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
⊢ Minimal M.Spanning X

Tactic:
minimal_subset_iff,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
⊢ M.Spanning X ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ X → X = t
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
⊢ ∀ (x : α),
    f x ∈ M.E →
      (M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x)

Tactic:
intro x hxE

Goal state after:
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this : IsScalarTower (↥Rt) (↥St) A
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)

Tactic:
have : NoZeroDivisors St := (Set.image_eq_range _ _ ▸ ind.aevalEquiv)
    |>.symm.injective.noZeroDivisors _ (map_zero _) (map_mul _)

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rt) (↥St) A
this : NoZeroDivisors ↥St
⊢ Transcendental (↥(adjoin S (x '' t))) (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
⊢ trdeg R A = ⨆ ι, #↑↑ι

Tactic:
by
  refine (ciSup_le' fun s ↦ ?_).antisymm
    (ciSup_le' fun s ↦ le_ciSup_of_le bddAbove_of_small ⟨s, s.2.1⟩ le_rfl)
  choose t ht using exists_isTranscendenceBasis_superset s.2
  exact le_ciSup_of_le bddAbove_of_small ⟨t, ht.2⟩ (mk_le_mk_of_subset ht.1)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case mp
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
⊢ g • a ∈ s → a ∈ s

Tactic:
intro; apply s_subset

Goal state after:
case mp
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : g • a ∈ s
⊢ a ∈ (fixedBy α g)ᶜ
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
⊢ a ∈ s → g • a ∈ s

Tactic:
intro; apply s_subset

Goal state after:
case mpr
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
a_moved : a ∉ fixedBy α g
a✝ : a ∈ s
⊢ g • a ∈ (fixedBy α g)ᶜ
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
ι' : 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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
⊢ Algebra.IsAlgebraic (↥Rxy) A

Tactic:
let _ : Algebra Rxy Sy := by
    refine (Subalgebra.inclusion (T := Sy.restrictScalars Rx) <| adjoin_le ?_).toAlgebra
    rintro _ ⟨i, rfl⟩; exact subset_adjoin (s := range y) ⟨i, rfl⟩

Goal state after:
case inr
ι : Type u
ι' : 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✝ : NoZeroDivisors A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
this✝¹ : Nontrivial S
this✝ : Nontrivial A
Sy : Subalgebra S A := adjoin S (range y)
this : Algebra.IsAlgebraic (↥Sy) A
x✝ : Algebra ↥Rxy ↥Sy := (Subalgebra.inclusion ⋯).toAlgebra
⊢ Algebra.IsAlgebraic (↥Rxy) 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✝¹ : FaithfulSMul R A
inst✝ : Subsingleton A
s : Set A
⊢ ⋂₀ {F | s ⊆ F} = s

Tactic:
exact subset_antisymm (sInter_subset_of_mem <| subset_refl s) (subset_sInter fun _ ↦ id)

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
m n : ℕ
h : f m = f n
⊢ m = n

Tactic:
replace h : (MvPolynomial.X i) ^ (m + 1) = (MvPolynomial.X i) ^ (n + 1) := hi1 <| by
    simpa [f, -map_pow] using congr($h (algebraMap _ K (MvPolynomial.X (R := F) i)))

Goal state after:
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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
m n : ℕ
h : MvPolynomial.X i ^ (m + 1) = MvPolynomial.X i ^ (n + 1)
⊢ m = n
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case zero
F : Type u
inst✝¹ : Field F
f : F[X]
n : ℕ
inst✝ : CharZero F
⊢ ((expand F (1 ^ n)) f).natSepDegree = f.natSepDegree

Tactic:
simp only [one_pow, expand_one]

Goal state after: