awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
eq : v i = v j
⊢ IsTranscendenceBasis.{u, u_1, v} (ι := (↑(insert i s \ {j}) : Type u)) R (A := S)
    ((fun (x : (↑s : Type u)) ↦ v (↑x : ι)) ∘
      (⇑((Equiv.image (Equiv.swap j i) s).trans
              (Equiv.setCongr (s := (⇑(Equiv.swap j i) : (a : ι) → ι) '' s) (t := insert i s \ {j}) ⋯)).symm :
        (a : (↑(insert i s \ {j}) : Type u)) → (↑s : Type u)))

Tactic:
H₁.comp_equiv <|
        .symm <|
          ((Equiv.swap j i).image s).trans <|
            .setCongr <| Equiv.image_swap_of_mem_of_notMem hj hi

Premises used: Equiv.image_swap_of_mem_of_notMem, Equiv.trans, Equiv.swap, Equiv.setCongr, IsTranscendenceBasis.comp_equiv, Equiv.image, Equiv.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_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
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 ⋯) : ι) =
      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}) ⋯)).symm :
          (a : (↑(insert x s \ {j}) : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x ⋯)
h₁ :
  ∀ (x : ι) (hxj : x ∉ {j}) (hxi : x ∈ s),
    v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x ⋯) : ι) =
      Function.comp (α := (↑(insert i s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
        (⇑((Equiv.image (Equiv.swap j i) s).trans
                (Equiv.setCongr (s := (⇑(Equiv.swap j i) : (a : ι) → ι) '' s) (t := insert i s \ {j}) ⋯)).symm :
          (a : (↑(insert i s \ {j}) : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x ⋯)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

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⟩

Premises used: Equiv.image_swap_of_mem_of_notMem, Equiv.trans, Equiv.swap, IsTranscendenceBasis.comp_equiv, Equiv.image, 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 ι
j : ι
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_1 : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
x : ι
hxj : x ∉ {j}
hj : 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 ⋯) : ι) =
    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}) ⋯)).symm :
        (a : (↑(insert x s \ {j}) : Type u)) → (↑s : Type u))
      (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x ⋯)

Tactic:
simp [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_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
x : ι
hxj : x ∉ {j}
hxi : x ∈ s
⊢ v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x ⋯) : ι) =
    Function.comp (α := (↑(insert i s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
      (⇑((Equiv.image (Equiv.swap j i) s).trans
              (Equiv.setCongr (s := (⇑(Equiv.swap j i) : (a : ι) → ι) '' s) (t := insert i s \ {j}) ⋯)).symm :
        (a : (↑(insert i s \ {j}) : Type u)) → (↑s : Type u))
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x ⋯)

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne hxj (ne_of_mem_of_not_mem hxi hi)]

Premises used: Equiv.swap_apply_of_ne_of_ne, ne_of_mem_of_not_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})
hi : i ∉ s
eq : v i = v j
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 ⋯) : ι) =
      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}) ⋯)).symm :
          (a : (↑(insert x s \ {j}) : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ insert x s \ {j}) x ⋯)
h₁ h₂ :
  ∀ (x : ι) (hxj : x ∉ {j}) (hxi : x ∈ s),
    v (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x ⋯) : ι) =
      Function.comp (α := (↑(insert i s \ {j}) : Type u)) (fun (x : (↑s : Type u)) ↦ v (↑x : ι))
        (⇑((Equiv.image (Equiv.swap j i) s).trans
                (Equiv.setCongr (s := (⇑(Equiv.swap j i) : (a : ι) → ι) '' s) (t := insert i s \ {j}) ⋯)).symm :
          (a : (↑(insert i s \ {j}) : Type u)) → (↑s : Type u))
        (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s \ {j}) x ⋯)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
classical
    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⟩
    · simp [eq]
    · simp [Equiv.swap_apply_of_ne_of_ne hxj (ne_of_mem_of_not_mem hxi hi)]

Premises used: IsTranscendenceBasis.comp_equiv, 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
ne : v i ≠ v j
his : v i ∈ v '' s
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})

Tactic:
Matroid.closure_subset_closure _ ?_ H₂

Premises used: Matroid.closure_subset_closure
-- 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
ne : v i ≠ v j
his : v i ∈ v '' s
refine : v '' (insert i s \ {j}) ⊆ v '' s \ {v j}
⊢ v j ∈ (matroid R S).closure (v '' s \ {v j})

Tactic:
refine Matroid.closure_subset_closure _ ?_ H₂

Premises used: Matroid.closure_subset_closure
-- 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 ι
j : ι
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_1 : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
k : ι
hkj : k ∉ {j}
hj : j ∈ insert k s
this : Nontrivial.{v} ↥(adjoin R (v '' (insert k s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert k s \ {j}))
hi : k ∉ s
ne : v k ≠ v j
his : v k ∈ v '' s
⊢ v k ∈ v '' s \ {v j}

Tactic:
⟨his, ne⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro
-- 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 ι
j : ι
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_1 : j ∈ s
Hj : v j ∉ (matroid R S).closure (v '' s \ {v j})
k : ι
hkj : k ∉ {j}
hj : j ∈ insert k s
this : Nontrivial.{v} ↥(adjoin R (v '' (insert k s \ {j})))
H₂ : v j ∈ (matroid R S).closure (v '' (insert k s \ {j}))
hi : k ∉ s
ne : v k ≠ v j
his : v k ∈ v '' s
⊢ v k ∈ v '' s \ {v j}

Tactic:
exact ⟨his, ne⟩
-- 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
ne : v i ≠ v j
his : v i ∈ v '' s
k : ι
hkj : k ∉ {j}
hks : k ∈ s
⊢ v k ∈ v '' s \ {v j}

Tactic:
⟨⟨k, hks, rfl⟩, inj.ne hks hj hkj⟩

Premises used: Set.Mem, Set.diff, setOf, And.intro, Exists.intro, Set.InjOn.ne, 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
ne : v i ≠ v j
his : v i ∈ v '' s
k : ι
hkj : k ∉ {j}
hks : k ∈ s
⊢ v k ∈ v '' s \ {v j}

Tactic:
exact ⟨⟨k, hks, rfl⟩, inj.ne hks hj hkj⟩
-- 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
ne : v i ≠ v j
⊢ v i ∉ v '' s

Tactic:
have hi' : v i ∉ v '' s := fun his ↦ Hj <| by
    refine Matroid.closure_subset_closure _ ?_ H₂
    rintro x ⟨k, ⟨rfl | hks, hkj⟩, rfl⟩
    · exact ⟨his, ne⟩
    · exact ⟨⟨k, hks, rfl⟩, inj.ne hks hj hkj⟩
-- 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
ne : v i ≠ v j
hi' : v i ∉ v '' s
⊢ InjOn v (insert i s)

Tactic:
have : (insert i s).InjOn v := (injOn_insert hi).mpr ⟨inj, hi'⟩
-- 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_4 : 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
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ Injective.{u + 1, v + 1} (β := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
injOn_iff_injective.1 (this.mono diff_subset)

Premises used: Set.diff_subset, Set.injOn_iff_injective, Iff.mp, Set.InjOn.mono, Set.restrict
-- 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_4 : 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
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ Injective.{u + 1, v + 1} (β := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
exact injOn_iff_injective.1 (this.mono diff_subset)

Premises used: Set.diff_subset, Set.injOn_iff_injective, Iff.mp, Set.InjOn.mono
-- 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_4 : 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
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
inr : (matroid R S).IsBase (v '' (insert i s \ {j}))
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i s \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
rw [← isTranscendenceBasis_subtype_range (by exact injOn_iff_injective.1 (this.mono diff_subset)),
    ← matroid_isBase_iff, ← image_eq_range]

Premises used: isTranscendenceBasis_subtype_range, Set.image_eq_range, AlgebraicIndependent.matroid_isBase_iff
-- 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_4 : 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
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
inr :
  ∀ (H₂ : v j ∈ (matroid R S).closure (insert (v i) (v '' s) \ {v 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)
    (ne : v i ≠ v j) (hi' : v i ∉ v '' s) (this : InjOn v (insert i s)),
    (matroid R S).IsBase (insert (v i) (v '' s) \ {v j})
⊢ (matroid R S).IsBase (v '' (insert i s \ {j}))

Tactic:
rw [this.image_diff_subset (singleton_subset_iff.mpr (.inr hj)), image_singleton,
    image_insert_eq] at H₂ ⊢

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.image_singleton, Set.InjOn.image_diff_subset, Set.image_insert_eq, Or.inr
-- 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 (insert (v i) (v '' s) \ {v j})
this_4 : 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
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ (matroid R S).IsBase (insert (v i) (v '' s) \ {v j})

Tactic:
H'.isBase_insert_diff_of_mem_closure H₂ (.inr ⟨j, hj, rfl⟩)

Premises used: Matroid.IsBase.isBase_insert_diff_of_mem_closure, And.intro, Exists.intro, Or.inr, 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 (insert (v i) (v '' s) \ {v j})
this_4 : 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
ne : v i ≠ v j
hi' : v i ∉ v '' s
this : InjOn v (insert i s)
⊢ (matroid R S).IsBase (insert (v i) (v '' s) \ {v j})

Tactic:
exact H'.isBase_insert_diff_of_mem_closure H₂ (.inr ⟨j, hj, rfl⟩)

Premises used: Matroid.IsBase.isBase_insert_diff_of_mem_closure, And.intro, Exists.intro, Or.inr, 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
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
inl :
  ∀ (H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
inr : ∀ (ne : j ≠ i), IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)

Tactic:
obtain rfl | ne := eq_or_ne j i

Premises used: eq_or_ne, 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
j : ι
v : ι → S
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)

Tactic:
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
j : ι
v : ι → S
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)
⊢ IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ j }) ↦ v (↑x : ι)

Tactic:
exact 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
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : { x : ι // x ≠ i }) ↦ v (↑x : ι)
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
⊢ ∀ (H₂ : IsAlgebraic (↥(adjoin R (v '' (insert i {i}ᶜ \ {j})))) (v j)),
    IsTranscendenceBasis.{u, u_1, v} R (A := S) fun (x : (↑(insert i {i}ᶜ \ {j}) : Type u)) ↦ v (↑x : ι)

Tactic:
have := H₁.of_isAlgebraic_adjoin_insert_diff {i}ᶜ i j v (.inr ne)