awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
a : ι
⊢ Prod.mk a ⁻¹' I =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)
have h : ∀ (x : α),
  x ∈ Prod.mk a ⁻¹' I ↔
    Membership.mem (γ := Set α)
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I) :
        Set α)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
⊢ (Matroid.sum' M).E = ⋃ (i : ι), Prod.mk i '' (M i).E
have h : ∀ (x : ι × α), x ∈ (Matroid.sum' M).E ↔ Membership.mem (γ := Set (ι × α)) (⋃ (i : ι), Prod.mk i '' (M i).E) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (Matroid.sum' M).IsBase B ↔ ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)
have simp : (∀ (i : ι),
    (M i).IsBase
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B))) ↔
  ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)
Tactic: simp only [Matroid.sum', mapEquiv_isBase_iff, Equiv.sigmaEquivProd_symm_apply, sigma_isBase_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).IsBase
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B))) ↔
    ∀ (i : ι), (M i).IsBase (Prod.mk i ⁻¹' B)
have h : ∀ (a : ι),
  Prod.mk a ⁻¹' B =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B)
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
B : Set (ι × α)
a : ι
⊢ Prod.mk a ⁻¹' B =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B)
have h : ∀ (x : α),
  x ∈ Prod.mk a ⁻¹' B ↔
    Membership.mem (γ := Set α)
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' B) :
        Set α)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
⊢ (Matroid.sum' M).IsBasis I X ↔ ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
have simp : (∀ (i : ι),
    (M i).IsBasis
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))
      (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X))) ↔
  ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
Tactic: simp only [Matroid.sum', mapEquiv_isBasis_iff, Equiv.sigmaEquivProd_symm_apply, sigma_isBasis_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
⊢ (∀ (i : ι),
      (M i).IsBasis
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X))) ↔
    ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
have h : ∀ (a : ι),
  Prod.mk a ⁻¹' I =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I X : Set (ι × α)
h :
  ∀ (a : ι),
    Prod.mk a ⁻¹' I =
      preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
        ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I)
⊢ (∀ (i : ι),
      (M i).IsBasis
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' I))
        (preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) i)
          ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X))) ↔
    ∀ (i : ι), (M i).IsBasis (Prod.mk i ⁻¹' I) (Prod.mk i ⁻¹' X)
have h₁ : ∀ (a : ι),
  Prod.mk a ⁻¹' X =
    preimage (β := (_ : ι) × α) (Sigma.mk (β := fun (i : ι) ↦ α) a)
      ((fun (a : ι × α) ↦ Sigma.mk (β := fun (x : ι) ↦ α) a.1 a.2) '' X)
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sum' M).Finitary
have this : (Matroid.sigma (α := fun (i : ι) ↦ α) M).Finitary
Tactic: have := Finitary.sigma h
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
h : Pairwise.{u_2} (α := ι) (Function.onFun.{u_2 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ (M i).E)
⊢ (Matroid.disjointSigma M h).E = ⋃ (i : ι), (M i).E
have h₁ : ∀ (x : α), x ∈ (Matroid.disjointSigma M h).E ↔ Membership.mem (γ := Set α) (⋃ (i : ι), (M i).E) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
I : Set (α ⊕ β)
⊢ (M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
have simp : M.Indep
      (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
        (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
          ((Equiv.ulift : (a : bif false then ULift.{u, v} β else ULift.{v, u} α) → α) a : α))
        (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
            (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
            ((fun (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                    (a : ULift.{v, u} α ⊕ ULift.{u, v} β) → (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                  a) ''
              (fun (a : α ⊕ β) ↦
                  Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                    (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                I) :
          Set (bif false then ULift.{u, v} β else ULift.{v, u} α))) ∧
    N.Indep
      (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
        (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
          ((Equiv.ulift : (a : bif true then ULift.{u, v} β else ULift.{v, u} α) → β) a : β))
        (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
            (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) true)
            ((fun (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                    (a : ULift.{v, u} α ⊕ ULift.{u, v} β) → (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                  a) ''
              (fun (a : α ⊕ β) ↦
                  Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                    (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                I) :
          Set (bif true then ULift.{u, v} β else ULift.{v, u} α))) ↔
  M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
Tactic: simp only [Matroid.sum, mapEquiv_indep_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply,
    Equiv.symm_symm, sigma_indep_iff, Bool.forall_bool]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u
β : Type v
M : Matroid α
N : Matroid β
B : Set (α ⊕ β)
⊢ (M.sum N).IsBase B ↔ M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)
have simp : M.IsBase
      (image (α := bif false then ULift.{u, v} β else ULift.{v, u} α)
        (fun (a : bif false then ULift.{u, v} β else ULift.{v, u} α) ↦
          ((Equiv.ulift : (a : bif false then ULift.{u, v} β else ULift.{v, u} α) → α) a : α))
        (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
            (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) false)
            ((fun (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                    (a : ULift.{v, u} α ⊕ ULift.{u, v} β) → (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                  a) ''
              (fun (a : α ⊕ β) ↦
                  Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                    (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                B) :
          Set (bif false then ULift.{u, v} β else ULift.{v, u} α))) ∧
    N.IsBase
      (image (α := bif true then ULift.{u, v} β else ULift.{v, u} α)
        (fun (a : bif true then ULift.{u, v} β else ULift.{v, u} α) ↦
          ((Equiv.ulift : (a : bif true then ULift.{u, v} β else ULift.{v, u} α) → β) a : β))
        (preimage (β := (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
            (Sigma.mk (β := fun (i : Bool) ↦ bif i then ULift.{u, v} β else ULift.{v, u} α) true)
            ((fun (a : ULift.{v, u} α ⊕ ULift.{u, v} β) ↦
                (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β) :
                    (a : ULift.{v, u} α ⊕ ULift.{u, v} β) → (i : Bool) × bif i then ULift.{u, v} β else ULift.{v, u} α)
                  a) ''
              (fun (a : α ⊕ β) ↦
                  Sum.map (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
                    (⇑(Equiv.symm Equiv.ulift) : (a : β) → ULift.{u, v} β) a) ''
                B) :
          Set (bif true then ULift.{u, v} β else ULift.{v, u} α))) ↔
  M.IsBase (Sum.inl ⁻¹' B) ∧ N.IsBase (Sum.inr ⁻¹' B)
Tactic: simp only [Matroid.sum, mapEquiv_isBase_iff, Equiv.sumCongr_symm, Equiv.sumCongr_apply,
    Equiv.symm_symm, sigma_isBase_iff, Bool.forall_bool]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
⊢ M.disjointSum N h = N.disjointSum M ⋯
have hE : ∀ (x : α), x ∈ (M.disjointSum N h).E ↔ x ∈ (N.disjointSum M sorry).E
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
hE : ∀ (x : α), x ∈ (M.disjointSum N h).E ↔ x ∈ (N.disjointSum M ⋯).E
⊢ M.disjointSum N h = N.disjointSum M ⋯
have h₁ : ∀ ⦃I : Set α⦄, I ⊆ (M.disjointSum N h).E → ((M.disjointSum N h).Indep I ↔ (N.disjointSum M sorry).Indep I)
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (hypothesis)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : (M.disjointSum N h).Indep I
⊢ ∃ (IM : Set α) (IN : Set α), M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
have hI₁ : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
Tactic: rw [disjointSum_indep_iff] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ (IM : Set α) (IN : Set α), M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
have refine : I = I ∩ M.E ∪ I ∩ N.E
Tactic: refine ⟨_, _, hI.1, hI.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E
have rw : I = I ∩ (M.E ∪ N.E)
Tactic: rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
rw : I = I ∩ (M.E ∪ N.E)
⊢ I = I ∩ M.E ∪ I ∩ N.E
have rw₁ : I = I
Tactic: rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (hypothesis)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : (M.disjointSum N h).IsBase B
⊢ ∃ (BM : Set α) (BN : Set α), M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN
have hB₁ : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
Tactic: rw [disjointSum_isBase_iff] at hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ ∃ (BM : Set α) (BN : Set α), M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN
have refine : B = B ∩ M.E ∪ B ∩ N.E
Tactic: refine ⟨_, _, hB.1, hB.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ B = B ∩ M.E ∪ B ∩ N.E
have rw : B = B ∩ (M.E ∪ N.E)
Tactic: rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hB.2.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Matroid.Sum (goal)
Goal:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
rw : B = B ∩ (M.E ∪ N.E)
⊢ B = B ∩ M.E ∪ B ∩ N.E
have rw₁ : B = B
Tactic: rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hB.2.2]
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
this :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
⊢ P = 0
have that : Injective (α := MvPolynomial τ R) (β := MvPolynomial σ R)
  (⇑(rename (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → MvPolynomial σ R)
Tactic: have that := MvPolynomial.rename_injective (R := R) e.symm (e.symm.injective)
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
this :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
that :
  Injective (α := MvPolynomial τ R) (β := MvPolynomial σ R)
    (⇑(rename (⇑e.symm : (a : τ) → σ)) : (a : MvPolynomial τ R) → MvPolynomial σ R)
⊢ P = 0
have that₁ : Eq (α := Ideal (MvPolynomial τ R))
  (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥
Tactic: rw [RingHom.injective_iff_ker_eq_bot] at that
Cleared hypotheses: that
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
this :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
that :
  Eq (α := Ideal (MvPolynomial τ R))
    (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥
⊢ P = 0
have rwa : ∀
  (this :
    Membership.mem (γ := Ideal (MvPolynomial τ R))
      (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) P)
  (that :
    Eq (α := Ideal (MvPolynomial τ R))
      (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥),
  P = 0
Tactic: rwa [← RingHom.mem_ker, that] at this
Cleared hypotheses: this, that
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
this :
  Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
that :
  Eq (α := Ideal (MvPolynomial τ R))
    (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥
rwa :
  ∀
    (this :
      Membership.mem (γ := Ideal (MvPolynomial τ R))
        (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) P)
    (that :
      Eq (α := Ideal (MvPolynomial τ R))
        (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥),
    P = 0
⊢ P = 0
have rwa₁ : ∀ (this : Membership.mem (γ := Ideal (MvPolynomial τ R)) ⊥ P)
  (that :
    Eq (α := Ideal (MvPolynomial τ R))
      (RingHom.ker (F := MvPolynomial τ R →ₐ[R] MvPolynomial σ R) (rename (⇑e.symm : (a : τ) → σ))) ⊥),
  P = 0
Tactic: rwa [← RingHom.mem_ker, that] at this
Cleared hypotheses: this, that
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
⊢ P = 0
have of_equiv : Eq (α := MvPolynomial σ R)
  ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
  (0 : MvPolynomial σ R)
Tactic: suffices MvPolynomial.rename e.symm P = 0 by
      have that := MvPolynomial.rename_injective (R := R) e.symm (e.symm.injective)
      rw [RingHom.injective_iff_ker_eq_bot] at that
      rwa [← RingHom.mem_ker, that] at this
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
⊢ Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have of_equiv : ∀ (i : σ),
  degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) <
    #(S ((e : (a : σ) → τ) i))
Tactic: apply h _ (fun i ↦ S (e i))
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
of_equiv :
  ∀ (i : σ),
    degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) <
      #(S ((e : (a : σ) → τ) i))
⊢ Eq (α := MvPolynomial σ R)
    ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have of_equiv₁ : ∀ (x : σ → R),
  (∀ (i : σ), x i ∈ S ((e : (a : σ) → τ) i)) →
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P : MvPolynomial σ R) :
        R)
      (0 : R)
Tactic: apply h _ (fun i ↦ S (e i))
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
i : σ
⊢ degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) <
    #(S ((e : (a : σ) → τ) i))
have h₁ : degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P) =
  degreeOf ((e : (a : σ) → τ) i) P
Tactic: convert! Hdeg (e i)
-- Lean 4 proof step from Mathlib.Combinatorics.Nullstellensatz (goal)
Goal:
R : Type u_1
inst : CommRing R
σ_1 : Type u_2
inst_1 : Finite σ_1
inst_2 : IsDomain R
σ τ : Type u_2
e : σ ≃ τ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R) (Hdeg : ∀ (i : σ), degreeOf i P < #(S i))
    (Heval :
      ∀ (x : σ → R),
        (∀ (i : σ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) P : R) (0 : R)),
    P = 0
P : MvPolynomial τ R
S : τ → Finset R
Hdeg : ∀ (i : τ), degreeOf i P < #(S i)
Heval :
  ∀ (x : τ → R), (∀ (i : τ), x i ∈ S i) → Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial τ R) → R) P : R) (0 : R)
i : σ
| degreeOf.{u_1, u_2} (R := R) i ((rename (⇑e.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) P)
have rw : degreeOf ((e : (a : σ) → τ) i) P
Tactic: rw [← e.symm_apply_apply i, degreeOf_rename_of_injective e.symm.injective]