awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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 })
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have 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 })
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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 })
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have 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 })
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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 })
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have 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 })
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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 })
⊢ lift.{w, v} (trdeg R S) + lift.{v, w} (trdeg S A) = lift.{v, w} (trdeg R A)
have 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 }
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]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ trdeg R S + trdeg S A = trdeg R A
have rw : lift.{v, v} (trdeg R S) + lift.{v, v} (trdeg S A) = lift.{v, v} (trdeg R A)
Tactic: rw [← (trdeg R S).lift_id, ← (trdeg S A).lift_id, ← (trdeg R A).lift_id]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have this : Nontrivial.{v} ↥(adjoin R (v '' (insert i s \ {j})))
Tactic: have := H₂.nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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})))
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have this₁ : Nontrivial S
Tactic: have := (adjoin R (v '' (insert i s \ {j}))).subtype_injective.nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have this₁ : IsDomain S
Tactic: have := (isDomain_iff_noZeroDivisors_and_nontrivial S).mpr ⟨‹_›, ‹_›⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have this₁ : Nontrivial R
Tactic: have := Module.nontrivial R S
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have H₃ : v j ∈ (matroid R S).closure (v '' (insert i s \ {j}))
Tactic: rw [← mem_algebraicClosure, ← SetLike.mem_coe, ← matroid_closure_eq] at H₂
Cleared hypotheses: H₂, this
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have inj : InjOn v s
Tactic: have inj := injOn_iff_injective.mpr H₁.1.injective
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have H' : (matroid R S).IsBase (v '' s)
Tactic: have H' := image_eq_range .. ▸ matroid_isBase_iff.mpr H₁.to_subtype_range
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have inl : ∀ (hj' : j ∉ s), 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
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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 : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have inr : ∀ (hj : j ∈ s), 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
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have 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 : ι)
Tactic: cases hj.resolve_right hj'
Cleared hypotheses: j, hj, this_1, H₂, hj'
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
Tactic: have Hj := H'.indep.notMem_closure_diff_of_mem ⟨j, hj, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})
have rw : v j ∈ (matroid R S).closure (v '' (s \ {j}))
Tactic: rw [← image_singleton, ← inj.image_diff_subset (singleton_subset_iff.mpr hj)]
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ v j ∈ (matroid R S).closure (v '' (s \ {j}))
have 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}))
Tactic: rwa [insert_eq_of_mem hi] at H₂
Cleared hypotheses: H₂, this, inj, H', hj, Hj, hi
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (hypothesis)
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})
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have hi : 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₂
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have inr : ∀ (eq : v i = v j), 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)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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 : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have inr₁ : ∀ (ne : v i ≠ v j), 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)
-- Lean 4 proof step from Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis (goal)
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
eq : v i = v j
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)
have h : ∀ (x : ι) (hxj : x ∉ {j}) (hj_2 : j ∈ insert x s) (this : Nontrivial.{v} ↥(adjoin R (v '' (insert x s \ {j}))))
  (H₂ : v j ∈ (matroid R S).closure (v '' (insert x s \ {j}))) (hi : x ∉ s) (eq : v x = v j),
  v (↑(Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x sorry) : ι) =
    Function.comp (α := (↑(insert x s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
      (⇑((Equiv.image (Equiv.swap j x) s).trans
              (Equiv.setCongr (s := (⇑(Equiv.swap j x) : (a : ι) → ι) '' s) (t := insert x s \ {j}) sorry)).symm :
        (a : (↑(insert x s \ {j}) : Type u)) → (↑s : Type u))
      (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x sorry)
Tactic: convert!
      H₁.comp_equiv <|
        .symm <|
          ((Equiv.swap j i).image s).trans <|
            .setCongr <| Equiv.image_swap_of_mem_of_notMem hj hi with
      ⟨x, rfl | hxi, hxj⟩
Cleared hypotheses: i, hj_1, this_1, H₂, hi, eq