awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
p : MvPolynomial (Fin n) R
s : Fin n → Set R
hs : ∀ (i : Fin n), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ s,
    Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
zero :
  ∀ {p : MvPolynomial (Fin 0) R} (s : Fin 0 → Set R) (hs : ∀ (i : Fin 0), (s i).Infinite)
    (h :
      ∀ x ∈ Set.pi (α := fun (i : Fin 0) ↦ R) Set.univ s,
        Eq (α := R) ((eval x : (a : MvPolynomial (Fin 0) R) → R) p : R) (0 : R)),
    p = 0
⊢ p = 0
have succ : ∀ (n : ℕ)
  (ih :
    ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R) (hs : ∀ (i : Fin n), (s i).Infinite)
      (h :
        ∀ x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ s,
          Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)),
      p = 0)
  {p : MvPolynomial (Fin (n + 1)) R} (s : Fin (n + 1) → Set R) (hs : ∀ (i : Fin (n + 1)), (s i).Infinite)
  (h :
    ∀ x ∈ Set.pi (α := fun (i : Fin (n + 1)) ↦ R) Set.univ s,
      Eq (α := R) ((eval x : (a : MvPolynomial (Fin (n + 1)) R) → R) p : R) (0 : R)),
  p = 0
Tactic: induction n with
  | zero =>
    apply (MvPolynomial.isEmptyRingEquiv R (Fin 0)).injective
    rw [map_zero]
    convert! h _ finZeroElim
  | succ n ih =>
    apply (finSuccEquiv R n).injective
    rw [map_zero]
    apply Polynomial.eq_zero_of_infinite_isRoot
    apply ((hs 0).image (C_injective ..).injOn).mono
    rintro _ ⟨r, hr, rfl⟩
    refine ih (s ·.succ) (fun _ ↦ hs _) fun x hx ↦ ?_
    rw [eval_polynomial_eval_finSuccEquiv]
    exact h _ fun i _ ↦ i.cases (by simpa using hr) (by simpa using hx)
Cleared hypotheses: n, p, s, hs, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
this :
  ∀ (p : MvPolynomial σ R),
    (∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
        Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)) →
      p = 0
⊢ p = q
have rw : ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
  Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (p - q) : R) (0 : R)
Tactic: rw [← sub_eq_zero, this (p - q)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
this :
  ∀ (p : MvPolynomial σ R),
    (∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
        Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)) →
      p = 0
x : (i : σ) → R
hx : x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (p - q) : R) (0 : R)
have simp_rw : HSub.hSub (α := R) (β := R) ((eval x : (a : MvPolynomial σ R) → R) p : R)
    ((eval x : (a : MvPolynomial σ R) → R) q : R) =
  0
Tactic: simp_rw [map_sub, h x hx, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
this :
  ∀ (p : MvPolynomial σ R),
    (∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
        Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)) →
      p = 0
x : (i : σ) → R
hx : x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s
simp_rw :
  HSub.hSub (α := R) (β := R) ((eval x : (a : MvPolynomial σ R) → R) p : R)
      ((eval x : (a : MvPolynomial σ R) → R) q : R) =
    0
⊢ Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) (p - q) : R) (0 : R)
have simp_rw₁ : HSub.hSub (α := R) (β := R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
    ((eval x : (a : MvPolynomial σ R) → R) q : R) =
  0
Tactic: simp_rw [map_sub, h x hx, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
⊢ p = q
have suffices : ∀ (p : MvPolynomial σ R),
  (∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
      Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)) →
    p = 0
Tactic: suffices ∀ p, (∀ x ∈ Set.pi .univ s, eval x p = 0) → p = 0 by
    rw [← sub_eq_zero, this (p - q)]
    intro x hx
    simp_rw [map_sub, h x hx, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
p : MvPolynomial σ R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p : R) (0 : R)
⊢ p = 0
have obtain : ∀ (n : ℕ) (f : Fin n → σ) (hf : Function.Injective f) (p : MvPolynomial (Fin n) R)
  (h :
    ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
      Eq.{u_1 + 1} (α := R)
        ((eval x : (a : MvPolynomial σ R) → R)
            ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
          R)
        (0 : R)),
  Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: obtain ⟨n, f, hf, p, rfl⟩ := exists_fin_rename p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
this : p = 0
⊢ Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw : Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) 0) 0
Tactic: rw [this, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
this : p = 0
rw : Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) 0) 0
⊢ Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw₁ : Eq (α := MvPolynomial σ R) 0 0
Tactic: rw [this, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
⊢ Eq (α := MvPolynomial σ R) ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have suffices : p = 0
Tactic: suffices p = 0 by rw [this, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
⊢ p = 0
have refine : ∀ (x : (i : Fin n) → R) (hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)),
  Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
Tactic: refine funext_fin (s ∘ f) (fun _ ↦ hs _) fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
⊢ Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
have choose : ∀ (g : (i : σ) → R) (hg : ∀ (i : σ), g i ∈ s i), Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
Tactic: choose g hg using fun i ↦ (hs i).nonempty
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
⊢ Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
have h₁ : Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R)
  ((eval (Function.extend f x g) : (a : MvPolynomial σ R) → R)
      ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
    R)
Tactic: convert! h (Function.extend f x g) fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
h₁ :
  Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R)
    ((eval (Function.extend f x g) : (a : MvPolynomial σ R) → R)
        ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
      R)
⊢ Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)
have convert! : ∀ (i : σ), Membership.mem (γ := Set σ) Set.univ i → Function.extend f x g i ∈ s i
Tactic: convert! h (Function.extend f x g) fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
h_2 : Membership.mem (γ := Set σ) Set.univ i
⊢ Function.extend f x g i ∈ s i
have inl : ∀ (i : Fin n), Membership.mem (γ := Set σ) Set.univ (f i) → Function.extend f x g (f i) ∈ s (f i)
Tactic: obtain ⟨i, rfl⟩ | nex := em (∃ x, f x = i)
Cleared hypotheses: i, h_2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
h_2 : Membership.mem (γ := Set σ) Set.univ i
inl : ∀ (i : Fin n), Membership.mem (γ := Set σ) Set.univ (f i) → Function.extend f x g (f i) ∈ s (f i)
⊢ Function.extend f x g i ∈ s i
have inr : ∀ (nex : ¬∃ (x : Fin n), f x = i), Function.extend f x g i ∈ s i
Tactic: obtain ⟨i, rfl⟩ | nex := em (∃ x, f x = i)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : Fin n
h_2 : Membership.mem (γ := Set σ) Set.univ (f i)
⊢ Function.extend f x g (f i) ∈ s (f i)
have inl : x i ∈ s (f i)
Tactic: rw [hf.extend_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
h_2 : Membership.mem (γ := Set σ) Set.univ i
nex : ¬∃ (x : Fin n), f x = i
inr inr₁ : Function.extend f x g i ∈ s i
⊢ Function.extend f x g i ∈ s i
have inr₂ : (if h : ∃ (a : Fin n), f a = i then x (Classical.choose (p := fun (x : Fin n) ↦ f x = i) h) else g i) ∈ s i
Tactic: simp_rw [Function.extend, dif_neg nex, hg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Funext (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
σ : Type u_2
p_1 q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h_1 :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R) ((eval x : (a : MvPolynomial σ R) → R) p_1 : R) ((eval x : (a : MvPolynomial σ R) → R) q : R)
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h :
  ∀ x ∈ Set.pi (α := fun (i : σ) ↦ R) Set.univ s,
    Eq.{u_1 + 1} (α := R)
      ((eval x : (a : MvPolynomial σ R) → R)
          ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R)
      (0 : R)
x : (i : Fin n) → R
hx : x ∈ Set.pi (α := fun (i : Fin n) ↦ R) Set.univ (s ∘ f)
g : (i : σ) → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
h_2 : Membership.mem (γ := Set σ) Set.univ i
nex : ¬∃ (x : Fin n), f x = i
inr inr₁ : Function.extend f x g i ∈ s i
inr₂ : (if h : ∃ (a : Fin n), f a = i then x (Classical.choose (p := fun (x : Fin n) ↦ f x = i) h) else g i) ∈ s i
⊢ Function.extend f x g i ∈ s i
have inr₃ : g i ∈ s i
Tactic: simp_rw [Function.extend, dif_neg nex, hg]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →ₐ[R] MvPolynomial σ R) (bind₁ X) (AlgHom.id R (MvPolynomial σ R))
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial σ R) ((bind₁ X : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ R) (bind₂ C) (RingHom.id (MvPolynomial σ R))
have hC : ∀ (x : R),
  Eq (α := MvPolynomial σ R) ((RingHom.comp (bind₂ C) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
    ((RingHom.comp (RingHom.id (MvPolynomial σ R)) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
hC :
  ∀ (x : R),
    Eq (α := MvPolynomial σ R) ((RingHom.comp (bind₂ C) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
      ((RingHom.comp (RingHom.id (MvPolynomial σ R)) C : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ R) (bind₂ C) (RingHom.id (MvPolynomial σ R))
have hX : ∀ (i : σ) (m : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := R) (coeff m ((bind₂ C : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))
    (coeff m ((RingHom.id (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i)))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ R)
    ((aeval id : (a : MvPolynomial (MvPolynomial τ R) R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial (MvPolynomial τ R) R) p) :
      MvPolynomial τ R)
    ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
have rw : Eq (α := MvPolynomial τ R) ((aeval (id ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
  ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
Tactic: rw [aeval_rename, Function.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
f : σ → MvPolynomial τ R
p : MvPolynomial σ R
rw :
  Eq (α := MvPolynomial τ R) ((aeval (id ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
    ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((aeval id : (a : MvPolynomial (MvPolynomial τ R) R) → MvPolynomial τ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial (MvPolynomial τ R) R) p) :
      MvPolynomial τ R)
    ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
have rw₁ : Eq (α := MvPolynomial τ R) ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
  ((aeval f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
Tactic: rw [aeval_rename, Function.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → MvPolynomial υ R
⊢ (bind₁ g).comp (bind₁ f) = bind₁ fun (i : σ) ↦ (bind₁ g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i)
have hf : ∀ (i : σ),
  Eq (α := MvPolynomial υ R)
    (((bind₁ g).comp (bind₁ f) : (a : MvPolynomial σ R) → MvPolynomial υ R) (X i) : MvPolynomial υ R)
    ((bind₁ fun (i : σ) ↦ (bind₁ g : (a : MvPolynomial τ R) → MvPolynomial υ R) (f i) :
          (a : MvPolynomial σ R) → MvPolynomial υ R)
        (X i) :
      MvPolynomial υ R)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Monad (goal)
Goal:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* MvPolynomial σ T
⊢ (bind₂ g).comp (bind₂ f) = bind₂ ((bind₂ g).comp f)
have hC : ∀ (x : R),
  Eq (α := MvPolynomial σ T) ((((bind₂ g).comp (bind₂ f)).comp C : (a : R) → MvPolynomial σ T) x : MvPolynomial σ T)
    (((bind₂ ((bind₂ g).comp f)).comp C : (a : R) → MvPolynomial σ T) x : MvPolynomial σ T)
Tactic: ext : 2