awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
⊢ FaithfulSMul R A

Tactic:
have := (faithfulSMul_iff_algebraMap_injective R A).mpr hx.algebraMap_injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
⊢ (matroid R A).RankFinite

Tactic:
rw [← matroid_cRank_eq, ← Matroid.rankFinite_iff_cRank_lt_aleph0] at fin

Premises used: AlgebraicIndependent.matroid_cRank_eq, Matroid.rankFinite_iff_cRank_lt_aleph0
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).RankFinite
⊢ IsTranscendenceBasis R x

Tactic:
.of_subtype_range hx.injective <| matroid_indep_iff.mpr hx.to_subtype_range
    |>.isBase_of_cRank_le <| lift_le.mp <| (matroid_cRank_eq R A ▸ le).trans_eq
      (mk_range_eq_of_injective hx.injective).symm

Premises used: Iff.mpr, AlgebraicIndependent.matroid_indep_iff, IsTranscendenceBasis.of_subtype_range, Matroid.Indep.isBase_of_cRank_le, Iff.mp, AlgebraicIndependent.injective, Cardinal.lift_le, AlgebraicIndependent.to_subtype_range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
this : FaithfulSMul R A
fin : (matroid R A).RankFinite
⊢ IsTranscendenceBasis R x

Tactic:
exact .of_subtype_range hx.injective <| matroid_indep_iff.mpr hx.to_subtype_range
    |>.isBase_of_cRank_le <| lift_le.mp <| (matroid_cRank_eq R A ▸ le).trans_eq
      (mk_range_eq_of_injective hx.injective).symm

Premises used: Iff.mpr, AlgebraicIndependent.matroid_indep_iff, Matroid.Indep.isBase_of_cRank_le, Iff.mp, Cardinal.lift_le, AlgebraicIndependent.to_subtype_range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
ι : Type w
x : ι → A
hx : AlgebraicIndependent R x
fin : trdeg R A < ℵ₀
le : trdeg R A ≤ #ι
rwa : trdeg R A ≤ lift.{w, w} #ι
rwa₁ rwa₂ rwa₃ rwa₄ : trdeg R A ≤ #ι
⊢ lift.{w, w} (trdeg R A) ≤ lift.{w, w} #ι

Tactic:
rwa [lift_id, lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
inst_5 : Finite ι
hx : AlgebraicIndependent R x
le : lift.{u, w} (trdeg R A) ≤ lift.{w, u} #ι
⊢ lift.{w, u} #ι < lift.{u, w} ℵ₀

Tactic:
simp
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
A : Type w
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : NoZeroDivisors A
ι : Type w
inst_5 : Finite ι
x : ι → A
hx : AlgebraicIndependent R x
le : trdeg R A ≤ #ι
rwa : trdeg R A ≤ lift.{w, w} #ι
rwa₁ rwa₂ rwa₃ rwa₄ : trdeg R A ≤ #ι
⊢ lift.{w, w} (trdeg R A) ≤ lift.{w, w} #ι

Tactic:
rwa [lift_id, lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
have :
  ∀ (s : Set S)
    (hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))),
    lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
have ⟨s, hs⟩ := exists_isTranscendenceBasis R S
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
have :
  ∀ (t : Set A)
    (ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))),
    lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
⊢ 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
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
⊢ NoZeroDivisors S

Tactic:
have := (FaithfulSMul.algebraMap_injective S A).noZeroDivisors _ (map_zero _) (map_mul _)
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this : NoZeroDivisors S
⊢ Nontrivial S

Tactic:
have := (FaithfulSMul.algebraMap_injective R S).nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
A : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Nontrivial R
inst_8 : NoZeroDivisors A
inst_9 : FaithfulSMul R S
inst_10 : FaithfulSMul S A
s : Set S
hs : IsTranscendenceBasis.{v, u_1, v} (ι := { x : S // x ∈ s }) R (Subtype.val (p := fun (x : S) ↦ x ∈ s))
t : Set A
ht : IsTranscendenceBasis.{w, v, w} (ι := { x : A // x ∈ t }) S (Subtype.val (p := fun (x : A) ↦ x ∈ t))
this_1 : NoZeroDivisors S
this : Nontrivial S
rw : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
rw₁ : lift.{w, v} #{ x : S // x ∈ s } + lift.{v, w} #{ x : A // x ∈ t } = lift.{v, w} (trdeg R A)
rw₂ : lift.{w, v} #{ x : S // x ∈ s } + lift.{max w v, w} #{ x : A // x ∈ t } = lift.{max w v, w} (trdeg R A)
rw₃ : lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } = lift.{max w v, w} (trdeg R A)
rw₄ :
  lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } =
    lift.{w, max v w} #(Sum.{w, v} { x : A // x ∈ t } { x : S // x ∈ s })
rw₅ :
  lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } =
    lift.{w, max v w} (lift.{v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s })
rw₆ :
  lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } =
    lift.{w, max v w} (lift.{v, w} #{ x : A // x ∈ t }) + lift.{w, max v w} (lift.{w, v} #{ x : S // x ∈ s })
rw₇ :
  lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } =
    lift.{max v w, w} #{ x : A // x ∈ t } + lift.{w, max v w} (lift.{w, v} #{ x : S // x ∈ s })
rw₈ rw₉ :
  lift.{max w v, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s } =
    lift.{max v w, w} #{ x : A // x ∈ t } + lift.{w, v} #{ x : S // x ∈ s }
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)

Tactic:
rw [← hs.cardinalMk_eq_trdeg, ← ht.cardinalMk_eq_trdeg, ← lift_umax.{w}, add_comm,
    ← (hs.sumElim_comp ht).lift_cardinalMk_eq_trdeg, mk_sum, lift_add, lift_lift, lift_lift]

Premises used: Cardinal.lift_lift, IsTranscendenceBasis.lift_cardinalMk_eq_trdeg, add_comm, IsTranscendenceBasis.cardinalMk_eq_trdeg, Cardinal.mk_sum, IsTranscendenceBasis.sumElim_comp, Cardinal.lift_add
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
A : Type v
inst_4 : CommRing A
inst_5 : NoZeroDivisors A
inst_6 : Algebra R A
inst_7 : Algebra S A
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
inst_10 : IsScalarTower R S A
rw : lift.{v, v} (trdeg R S) + lift.{v, v} (trdeg S A) = lift.{v, v} (trdeg R A)
⊢ trdeg R S + trdeg S A = trdeg R A

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

Premises used: Algebra.trdeg, Cardinal.lift_id
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
A : Type v
inst_4 : CommRing A
inst_5 : NoZeroDivisors A
inst_6 : Algebra R A
inst_7 : Algebra S A
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
inst_10 : IsScalarTower R S A
⊢ lift.{v, v} (trdeg R S) + lift.{v, v} (trdeg S A) = lift.{v, v} (trdeg R A)

Tactic:
lift_trdeg_add_eq R S A

Premises used: lift_trdeg_add_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Nontrivial R
A : Type v
inst_4 : CommRing A
inst_5 : NoZeroDivisors A
inst_6 : Algebra R A
inst_7 : Algebra S A
inst_8 : FaithfulSMul R S
inst_9 : FaithfulSMul S A
inst_10 : IsScalarTower R S A
⊢ lift.{v, v} (trdeg R S) + lift.{v, v} (trdeg S A) = lift.{v, v} (trdeg R A)

Tactic:
exact lift_trdeg_add_eq R S A

Premises used: lift_trdeg_add_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
⊢ Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))

Tactic:
have := H₂.nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
⊢ Nontrivial S

Tactic:
have := (adjoin R (v '' (insert i s \ {j}))).subtype_injective.nontrivial
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this : Nontrivial S
⊢ IsDomain S

Tactic:
have := (isDomain_iff_noZeroDivisors_and_nontrivial S).mpr ⟨‹_›, ‹_›⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this : IsDomain S
⊢ Nontrivial R

Tactic:
have := Module.nontrivial R S
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
this : Nontrivial R
⊢ v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))

Tactic:
rw [← mem_algebraicClosure, ← SetLike.mem_coe, ← matroid_closure_eq] at H₂

Premises used: Subalgebra.mem_algebraicClosure, SetLike.mem_coe, AlgebraicIndependent.matroid_closure_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i s \ {j})))) (v j)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
this : Nontrivial R
H₃ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
⊢ Nontrivial R

Tactic:
rw [← mem_algebraicClosure, ← SetLike.mem_coe, ← matroid_closure_eq] at H₂

Premises used: Subalgebra.mem_algebraicClosure, SetLike.mem_coe, AlgebraicIndependent.matroid_closure_eq
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
⊢ InjOn v s

Tactic:
have inj := injOn_iff_injective.mpr H₁.1.injective
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
⊢ (matroid R S).IsBase (v '' s)

Tactic:
have H' := image_eq_range .. ▸ matroid_isBase_iff.mpr H₁.to_subtype_range
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
inl : ∀ (hj' : j ∉ s), IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
inr : ∀ (hj : j ∈ s), IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
obtain hj' | hj := (em (j ∈ s)).symm

Premises used: Membership.mem, em, Or.symm
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj' : j ∉ s
inl :
  ∀ (hj : i ∈ insert i s) (this : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {i}))))
    (H₂ : v i ∈ (matroid R S).closure (v '' (insert i s \ {i}))) (hj' : i ∉ s),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {i}) : Type u)) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
cases hj.resolve_right hj'

Premises used: Or.resolve_right
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial S
this_2 : IsDomain S
this_3 : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : i ∈ insert i s
this : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {i})))
H₂ : v i ∈ (matroid R S).closure (v '' (insert i s \ {i}))
hj' : i ∉ s
inl inl₁ inl₂ inl₃ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {i}) : Type u)) ↦ v (↑x : ι)

Tactic:
rwa [insert_diff_self_of_notMem hj']

Premises used: Set.insert_diff_self_of_notMem
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
⊢ v j ∉ (matroid R S).closure (v '' s \ {v j})

Tactic:
have Hj := H'.indep.notMem_closure_diff_of_mem ⟨j, hj, rfl⟩
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
rw : v j ∈ (matroid R S).closure (v '' (s \ {j}))
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})

Tactic:
rw [← image_singleton, ← inj.image_diff_subset (singleton_subset_iff.mpr hj)]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.image_singleton, Set.InjOn.image_diff_subset
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∈ s
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (H₂ : v j ∈ (matroid R S).closure (v '' (s \ {j}))) (this : Nontrivial R) (inj : InjOn v s)
    (H' : (matroid R S).IsBase (v '' s)) (hj : j ∈ s) (Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})) (hi : i ∈ s),
    v j ∈ (matroid R S).closure (v '' (s \ {j}))
⊢ v j ∈ (matroid R S).closure (v '' (s \ {j}))

Tactic:
rwa [insert_eq_of_mem hi] at H₂

Premises used: Set.insert_eq_of_mem
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
⊢ i ∉ s

Tactic:
have hi : i ∉ s := fun hi ↦ Hj <| by
    rw [← image_singleton, ← inj.image_diff_subset (singleton_subset_iff.mpr hj)]
    rwa [insert_eq_of_mem hi] at H₂
-- Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Goal:
ι : Type u
R : Type u_1
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FaithfulSMul R S
inst_4 : NoZeroDivisors S
s : Set ι
i j : ι
v : ι → S
hj_1 : j ∈ insert i s
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑s : Type u)) ↦ v (↑x : ι)
this_1 : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
this_2 : Nontrivial S
this_3 : IsDomain S
H₂ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
this : Nontrivial R
inj : InjOn v s
H' : (matroid R S).IsBase (v '' s)
hj : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
hi : i ∉ s
inr :
  ∀ (eq : v i = v j), IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
inr₁ :
  ∀ (ne : v i ≠ v j), IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
obtain eq | ne := eq_or_ne (v i) (v j)

Premises used: eq_or_ne