mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ finrank R ↥(⋀[R]^n M) = (finrank R M).choose n

Tactic:
let : LinearOrder (Module.Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
  let B := (Module.Free.chooseBasis R M).exteriorPower n
  rw [Module.finrank_eq_card_basis (Module.Free.chooseBasis R M), Module.finrank_eq_card_basis B,
    Fintype.card_eq_nat_card, powersetCard.card, Fintype.card_eq_nat_card]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
h₂ : r • f i = (r • 1) • f i
⊢ tprodCoeff R z (update f i (r • f i)) = tprodCoeff R (r • 1 * z) f

Tactic:
h₂

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
inst✝⁴ : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
r : R₁
inst✝³ : SMul R₁ R
inst✝² : IsScalarTower R₁ R R
inst✝¹ : SMul R₁ (s i)
inst✝ : IsScalarTower R₁ R (s i)
h₁ : r • z = r • 1 * z
h₂ : r • f i = (r • 1) • f i
⊢ tprodCoeff R z (update f i ((r • 1) • f i)) = tprodCoeff R (r • 1 * z) f
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
⊢ x = y

Tactic:
obtain ⟨M', hM, hFG, h⟩ :=
    TensorProduct.exists_finite_submodule_left_of_setFinite' {x, y} (Set.toFinite _)

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : Module.Finite R ↥M'
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥N) (inclusion hM)).range
⊢ x = y
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)
z : ⨂[R] (i : ι), s i
⊢ ∀ (r : R) (f : (i : ι) → s i), φ₁ (tprodCoeff R r f) = φ₂ (tprodCoeff R r f)

Tactic:
· intro r f
    rw [tprodCoeff_eq_smul_tprod, φ₁.map_smul, φ₂.map_smul]
    apply congr_arg
    exact MultilinearMap.congr_fun H f

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
s : Finset ι
f : ι → R
hfv : ∑ i ∈ s, f i • v i = 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
induction s using Finset.induction generalizing v i with
  | empty => exact (Finset.notMem_empty _ hi).elim
  | insert n s hn ih => ?_
  rw [← Finset.sum_coe_sort] at hfv
  have ⟨l, a, y, hay, hfa⟩ := Flat.isTrivialRelation_of_sum_smul_eq_zero hfv
  have : v n ∉ 𝔪 • (⊤ : Submodule R M) := by
    simpa only [← LinearMap.ker_tensorProductMk] using! h.ne_zero n
  set n : ↥(insert n s) := ⟨n, Finset.mem_insert_self ..⟩ with n_def
  obtain ⟨j, hj⟩ : ∃ j, IsUnit (a n j) := by
    contrapose! this
    rw [show v n = _ from hay n]
    exact sum_mem fun _ _ ↦ Submodule.smul_mem_smul (this _) ⟨⟩
  let a' (i : ι) : R := if hi : _ then a ⟨i, hi⟩ j else 0
  have a_eq i : a i j = a' i.1 := by simp_rw [a', dif_pos i.2]
  have hfn : f n = -(∑ i ∈ s, f i * a' i) * hj.unit⁻¹ := by
    rw [← hj.mul_left_inj, mul_assoc, hj.val_inv_mul, mul_one, eq_neg_iff_add_eq_zero]
    convert! hfa j
    simp_rw [a_eq, Finset.sum_coe_sort _ (fun i ↦ f i * a' i), s.sum_insert hn, n_def]
  let c (i : ι) : R := -(if i = n then 0 else a' i) * hj.unit⁻¹
  specialize ih (v + (c · • v n)) ?_ ?_
  · convert! (linearIndependent_add_smul_iff (c := Ideal.Quotient.mk _ ∘ c) (i := n.1) ?_).mpr h
    · ext; simp [tmul_add]; rfl
    simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
  · rw [Finset.sum_coe_sort _ (fun i ↦ f i • v i), s.sum_insert hn, add_comm, hfn] at hfv
    simp_rw [Pi.add_apply, smul_add, s.sum_add_distrib, c, smul_smul, ← s.sum_smul, ← mul_assoc,
      ← s.sum_mul, mul_neg, s.sum_neg_distrib, ← hfv]
    congr 4
    exact s.sum_congr rfl fun i hi ↦ by rw [if_neg (ne_of_mem_of_not_mem hi hn)]
  obtain hi | hi := Finset.mem_insert.mp hi
  · rw [hi, hfn, Finset.sum_eq_zero, neg_zero, zero_mul]
    intro i hi; rw [ih i hi, zero_mul]
  · exact ih i hi

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

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

Tactic:
rw [hx] at hb

Goal state after:
case pos.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
a : R
ha : a ∈ p.primeCompl
y : M
k : ℕ
h : f y = a ^ k • x
b : R
hb : b ∈ (⊥.colon {x}).radical
⊢ b ∈ (⊥.colon {y}).radical
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
l' : M →ₗ[R] ↥l.ker
this : Module.Finite R ↥l.ker
hl' : LinearMap.lTensor k l' ∘ₗ LinearMap.lTensor k l.ker.subtype = LinearMap.id
⊢ Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)

Tactic:
exact Function.HasLeftInverse.injective ⟨l'.lTensor k, DFunLike.congr_fun hl'⟩

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

Goal state after:
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 ∈ (⊥.colon {x}).radical
⊢ b ∈ (⊥.colon {g x}).radical
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
⊢ IsInducing (tensorProductTo R S T)

Tactic:
refine ⟨(continuous_tensorProductTo ..).le_induced.antisymm (isBasis_basic_opens.le_iff.mpr ?_)⟩

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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
⊢ ∀ U ∈ Set.range basicOpen, IsOpen[TopologicalSpace.induced (tensorProductTo R S T) instTopologicalSpaceProd] ↑U
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✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : FractionalIdeal R⁰ K
hI : (↑(I ^ n)).IsPrincipal
⊢ (↑I).IsPrincipal

Tactic:
obtain (rfl | ⟨u, rfl⟩) := GroupWithZero.eq_zero_or_unit I
  · simp [bot_isPrincipal]
  rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← hn,
    Nat.dvd_gcd_iff]
  refine ⟨?_, orderOf_dvd_card⟩
  rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff]
  exact_mod_cast hI

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
inst✝ : Subsingleton (ClassGroup R)
I : FractionalIdeal R⁰ K
hI : IsUnit I
⊢ (↑I).IsPrincipal

Tactic:
rcases hI with ⟨I, rfl⟩

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 : (FractionalIdeal R⁰ K)ˣ
⊢ (↑↑I).IsPrincipal
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
hf : Function.Surjective ⇑f
⊢ Projective R M

Tactic:
have (I : Ideal R) (hI : I.IsMaximal) :=
    letI := H I hI
    Module.projective_lifting_property (LocalizedModule.map I.primeCompl f) LinearMap.id
    (LocalizedModule.map_surjective _ _ hf)

Goal state after:
R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
hf : Function.Surjective ⇑f
this : ∀ (I : Ideal R) (hI : I.IsMaximal), ∃ h, (LocalizedModule.map I.primeCompl) f ∘ₗ h = LinearMap.id
⊢ Projective R M
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ (range f).Finite

Tactic:
have := discreteTopology_bot Y

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this✝ : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ (range f).Finite
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅⊤, ⊤⁆ < ⊤

Tactic:
exact commutator_lt_top_of_nontrivial H

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✝ : FinitePresentation R M
⊢ (∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)) ↔
    Projective R M

Tactic:
exact ⟨fun H ↦ Module.projective_of_localization_maximal fun I hI ↦
    have := H ⟨I, hI.isPrime⟩; .of_free, fun H x ↦ Module.free_of_flat_of_isLocalRing⟩

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
⊢ ∃ p, IsSplittingField F K p

Tactic:
classical
  let s := Module.Basis.ofVectorSpace F K
  refine
    ⟨∏ x, minpoly F (s x), Polynomial.map_prod (algebraMap F K) _ _ ▸
      Splits.prod fun x _ => h.splits (s x), Subalgebra.toSubmodule.injective ?_⟩
  rw [Algebra.top_toSubmodule, eq_top_iff, ← s.span_eq, Submodule.span_le, Set.range_subset_iff]
  refine fun x =>
    Algebra.subset_adjoin
      (Multiset.mem_toFinset.mpr <|
        (mem_roots <|
              mt (Polynomial.map_eq_zero <| algebraMap F K).1 <|
                Finset.prod_ne_zero_iff.2 fun x _ => ?_).2 ?_)
  · exact minpoly.ne_zero (h.isIntegral (s x))
  rw [IsRoot.def, eval_map_algebraMap, map_prod]
  exact Finset.prod_eq_zero (Finset.mem_univ _) (minpoly.aeval _ _)

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
E : Type u_6
inst✝¹ : Field E
inst✝ : Algebra F E
h : Normal F E
x y : E
⊢ minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit Gal(E/F) y

Tactic:
refine ⟨fun he ↦ ?_, fun ⟨f, he⟩ ↦ he ▸ minpoly.algEquiv_eq f y⟩

Goal state after:
F : Type u_1
inst✝² : Field F
E : Type u_6
inst✝¹ : Field E
inst✝ : Algebra F E
h : Normal F E
x y : E
he : minpoly F x = minpoly F y
⊢ x ∈ MulAction.orbit Gal(E/F) y
Module: Mathlib.Combinatorics.Matroid.Basic

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

Tactic:
exact le_top.trans_eq hinf.symm

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
⊢ IsUnit (submoduleAlgebra e * submoduleAlgebra f)

Tactic:
have := eq_span_singleton_of_surjective <| LinearEquiv.surjective <|
    (congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ
    (mk_eq_one_iff.mp <| by simp_rw [mk_tensor, mk_eq_self, mul_inv_cancel]).some).symm ≪≫ₗ
    tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e)

Goal state after:
case mpr
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
M : Pic R
h : M ∈ relPic R A
e : A ⊗[R] M.AsModule ≃ₗ[A] A
f : A ⊗[R] M⁻¹.AsModule ≃ₗ[A] A
this :
  submoduleAlgebra e * submoduleAlgebra f =
    R ∙
      ↑(↑((TensorProduct.congr (submoduleAlgebraEquiv e) (submoduleAlgebraEquiv f) ≪≫ₗ ⋯.some).symm ≪≫ₗ
              tensorSubmoduleAlgebraEquivMul f (submoduleAlgebra e))
          1)
⊢ IsUnit (submoduleAlgebra e * submoduleAlgebra f)
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₂ M₃ : Matroidᵣ α
R : Set α
hR : R ⊆ M₂.toMatroid.E
h₁ : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
⊢ M₁.toMatroid ≤r M₃.toMatroid

Tactic:
h₂

Goal state after:
α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ M₃ : Matroidᵣ α
R R' : Set α
hR : R ⊆ (M₃.toMatroid ↾ R').E
h₁ : M₁.toMatroid = M₃.toMatroid ↾ R' ↾ R
hR' : R' ⊆ M₃.toMatroid.E
h₂ : M₂.toMatroid = M₃.toMatroid ↾ R'
⊢ M₁.toMatroid ≤r M₃.toMatroid
Module: Mathlib.Combinatorics.Matroid.Constructions

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

Tactic:
by
  rw [uniqueBaseOn_restrict', inter_right_comm, inter_eq_self_of_subset_left h]

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

Goal state before:
pp: α : Type u_1
M M' : Matroid α
h : M ≤r M'
h' : M' ≤r M
⊢ M = M'

Tactic:
by
  simpa using (ofMatroid_le_iff.2 h).antisymm (ofMatroid_le_iff.2 h')

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ N <r M

Tactic:
← h.eq_restrict

Goal state after:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ M ↾ N.E <r M
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
a : α
haX : a ∈ X
h : ∀ t ⊆ X, M.closure ∅ ⊆ M.closure t → a ∈ t
⊢ a = e

Tactic:
by simpa using h ∅ (empty_subset X) rfl.subset

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard = M.eRank

Tactic:
eRank_def,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard = M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRk ∅ = 0

Tactic:
rw [← M.empty_indep.isBasis_self.encard_eq_eRk, encard_empty]

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

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

Tactic:
eRank_def,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X ≤ M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
eRank_def,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk M.E ≤ M.eRk ((X ∪ M.E \ X) ∩ M.E)
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.eRk X < ⊤ ↔ M.IsRkFinite X

Tactic:
rw [lt_top_iff_ne_top, eRk_ne_top_iff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ↾ X).eRank = M.eRank

Tactic:
eRank_def,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ (M ↾ X).eRk (M ↾ X).E = M.eRank
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ x ∈ M.closure (B \ {e})

Tactic:
refine (M.closure_subset_closure (subset_sdiff_singleton ?_ ?_)) h_cct

Goal state after:
case inr.refine_1
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ M.fundCircuit x B \ {x} ⊆ B

case inr.refine_2
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.closure (M.fundCircuit x B \ {x})
⊢ e ∉ M.fundCircuit x B \ {x}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X : Set α
⊢ (loopyOn X).eRank = 0

Tactic:
eRank_def,

Goal state after:
α : Type u_1
X : Set α
⊢ (loopyOn X).eRk (loopyOn X).E = 0
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
X : Set α
⊢ (freeOn X).eRank = X.encard

Tactic:
eRank_def,

Goal state after:
α : Type u_1
X : Set α
⊢ (freeOn X).eRk (freeOn X).E = X.encard
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y X' : Set α
h : M.closure X = M.closure X'
⊢ M.closure (X ∪ Y) = M.closure (X' ∪ Y)

Tactic:
by
  rw [← M.closure_union_closure_left_eq, h, M.closure_union_closure_left_eq]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e f : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ M.closure (B \ {e})
hfE : f ∈ M.E
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
by
  obtain rfl | hne := eq_or_ne f e
  · simpa [he]
  have ⟨hi, hfB⟩ : M.Indep (insert f (B \ {e})) ∧ f ∉ B := by
    simpa [(hB.indep.sdiff _).notMem_closure_iff, hne] using hf
  exact hB.exchange_isBase_of_indep hfB hi

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

Goal state before:
pp: case neg
R : Type u_3
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : ¬Algebra.IsAlgebraic R A
⊢ ¬trdeg R A = 0 ↔ ¬Algebra.IsAlgebraic R A

Tactic:
rw [← Algebra.transcendental_iff_not_isAlgebraic] at h ⊢

Goal state after:
case neg
R : Type u_3
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Algebra.Transcendental R A
⊢ ¬trdeg R A = 0 ↔ Algebra.Transcendental R A
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
f : F[X]
irred : Irreducible f
inst✝ : CharZero F
⊢ HasSeparableContraction 1 f

Tactic:
exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩

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

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
N : Matroid α
hR : N ≤r M
hN : M.Spanning N.E
⊢ N.IsBase B ↔ M.IsBase B ∧ B ⊆ N.E

Tactic:
obtain ⟨R, hR : R ⊆ M.E, rfl⟩ := hR

Goal state after:
α : 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
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
s : Set (Set A)
hsn : s.Nonempty
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val

Tactic:
by
  let : Nonempty s := Nonempty.to_subtype hsn
  rw [sUnion_eq_iUnion]
  exact algebraicIndependent_iUnion_of_directed hs.directed_val (by simpa using h)

Goal state after:
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
s t : Set A
hst : s ⊆ t
hs : AlgebraicIndepOn R _root_.id s
⊢ ∃ u, s ⊆ u ∧ Maximal (fun x ↦ AlgebraicIndepOn R _root_.id x ∧ x ⊆ t) u

Tactic:
refine zorn_subset_nonempty { u : Set A | AlgebraicIndependent R ((↑) : u → A) ∧ u ⊆ t}
    (fun c hc chainc hcn ↦ ⟨⋃₀ c, ⟨?_, ?_⟩, fun _ ↦ subset_sUnion_of_mem⟩) s ⟨hs, hst⟩
  · exact algebraicIndependent_sUnion_of_directed hcn chainc.directedOn (fun x hxc ↦ (hc hxc).1)
  exact fun x ⟨w, hyc, hwy⟩ ↦ (hc hyc).2 hwy

Goal state after:
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
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
have ⟨t, ht⟩ := exists_isTranscendenceBasis S A

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
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)