awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
c : C
m : M
⊢ Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (c ⊗ₜ[A] Submodule.Quotient.mk (1 ⊗ₜ[R] m))
    (((cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule) :
          C ⊗[B] (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) :
        (a : C ⊗[B] (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (c ⊗ₜ[B] (fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (1 ⊗ₜ[R] m)))

Tactic:
simp [fAB, baseChangeMkQ]

Premises used: Module.Grassmannian.baseChangeMkQ
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
⊢ fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC

Tactic:
have hcomp : fAC = e.toLinearMap.comp fBC := by
    apply LinearMap.ext
    intro z
    induction z using TensorProduct.induction_on with
    | zero => simp [fAC, fBC, e]
    | tmul c m =>
      simp only [fAC, fBC, e, baseChangeMkQ, LinearMap.comp_apply, cancelBaseChange_symm_tmul,
         LinearMap.baseChange_tmul, Submodule.mkQ_apply, LinearEquiv.coe_trans, LinearEquiv.coe_coe,
         LinearEquiv.coe_baseChange, LinearMap.quotKerEquivOfSurjective_apply_mk]
      simp [fAB, baseChangeMkQ]
    | add x y hx hy =>
      simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_add] at *
      rw [hx, hy]
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
hcomp : fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC
h : x ∈ fAC.ker ↔ x ∈ (map g (map f N)).toSubmodule
h₁ : x ∈ fAC.ker ↔ x ∈ fBC.ker
h₂ : x ∈ ((↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC).ker ↔ x ∈ fBC.ker
h₃ h₄ : x ∈ fBC.ker ↔ x ∈ fBC.ker
⊢ x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule

Tactic:
rw [hfAC_ker_eq, hfBC_ker_eq, hcomp, LinearEquiv.ker_comp]

Premises used: LinearEquiv.ker_comp
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A_1 : Type w
inst_3 : CommRing A_1
inst_4 : Algebra R A_1
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A_1 →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
A : CommAlgCat.{w, u} R
w :
  ∀ (N : G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))),
    Eq (α := G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (𝟙 A))) :
            (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
          N :
        G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))) :
            (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
          N :
        G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
⊢ ↾map (CommAlgCat.Hom.hom (𝟙 A)) = 𝟙 G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))

Tactic:
ext N : 1
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A_1 : Type w
inst_3 : CommRing A_1
inst_4 : Algebra R A_1
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A_1 →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
A : CommAlgCat.{w, u} R
N : G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))
⊢ Eq (α := G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (𝟙 A))) :
          (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))) :
          (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))

Tactic:
map_id k A N

Premises used: Module.Grassmannian.map, Module.Grassmannian.map_id
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A_1 : Type w
inst_3 : CommRing A_1
inst_4 : Algebra R A_1
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A_1 →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
A : CommAlgCat.{w, u} R
N : G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))
⊢ Eq (α := G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (𝟙 A))) :
          (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w))) :
          (a : G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w))) → G(k, (↑A : Type w) ⊗[R] M; (↑A : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑A : Type w) M; (↑A : Type w)))

Tactic:
exact map_id k A N

Premises used: Module.Grassmannian.map_id
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f_1 : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g_1 : B →ₐ[R] C
X Y Z : CommAlgCat.{w, u} R
f : X ⟶ Y
g : Y ⟶ Z
w :
  ∀ (N : G(k, TensorProduct.{u, w, v} R (↑X : Type w) M; (↑X : Type w))),
    Eq (α := G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (f ≫ g))) :
            (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
          N :
        G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g)) :
            (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
          N :
        G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
⊢ Eq (α :=
    G(k, TensorProduct.{u, w, v} R (↑X : Type w) M; (↑X : Type w)) ⟶
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    (↾map (CommAlgCat.Hom.hom (f ≫ g))) (↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g))

Tactic:
ext N : 1
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f_1 : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g_1 : B →ₐ[R] C
X Y Z : CommAlgCat.{w, u} R
f : X ⟶ Y
g : Y ⟶ Z
N : G(k, TensorProduct.{u, w, v} R (↑X : Type w) M; (↑X : Type w))
⊢ Eq (α := G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (f ≫ g))) :
          (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g)) :
          (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))

Tactic:
map_comp k f.hom g.hom N

Premises used: Module.Grassmannian.map, Module.Grassmannian.map_comp, CommAlgCat.Hom.hom
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f_1 : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g_1 : B →ₐ[R] C
X Y Z : CommAlgCat.{w, u} R
f : X ⟶ Y
g : Y ⟶ Z
N : G(k, TensorProduct.{u, w, v} R (↑X : Type w) M; (↑X : Type w))
⊢ Eq (α := G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom (f ≫ g))) :
          (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g)) :
          (a : G(k, (↑X : Type w) ⊗[R] M; (↑X : Type w))) → G(k, (↑Z : Type w) ⊗[R] M; (↑Z : Type w)))
        N :
      G(k, TensorProduct.{u, w, v} R (↑Z : Type w) M; (↑Z : Type w)))

Tactic:
exact map_comp k f.hom g.hom N

Premises used: Module.Grassmannian.map_comp, CommAlgCat.Hom.hom
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
⊢ (r • x).support ⊆ x.support

Tactic:
Function.support_const_smul_subset ..

Premises used: HahnSeries.support, Function.support_const_smul_subset
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
⊢ (r • x).coeff = r • x.coeff

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
a : Γ
⊢ (r • x).coeff a = r • x.coeff a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
x : R
coeff : ∀ (x_1 : Γ), (HSMul.hSMul (β := V⟦Γ⟧) x 0).coeff x_1 = HahnSeries.coeff 0 x_1
⊢ HSMul.hSMul (β := V⟦Γ⟧) x 0 = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V_1 : Type u_6
α : Type u_7
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
x : R
x_1 : Γ
⊢ (HSMul.hSMul (β := V⟦Γ⟧) x 0).coeff x_1 = coeff 0 x_1

Tactic:
simp only [coeff_smul, coeff_zero, smul_zero]

Premises used: HahnSeries.coeff_smul, smul_zero, HahnSeries.coeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
pos : ∀ (hrx : r • x = 0), ¬(r • x).orderTop < x.orderTop
neg : ∀ (hrx : ¬r • x = 0), ¬(r • x).orderTop < x.orderTop
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
by_cases hrx : r • x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
pos : ¬⊤ < x.orderTop
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
rw [hrx, orderTop_zero]

Premises used: HahnSeries.orderTop_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬⊤ < x.orderTop

Tactic:
not_top_lt

Premises used: not_top_lt
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : r • x = 0
⊢ ¬⊤ < x.orderTop

Tactic:
exact not_top_lt

Premises used: not_top_lt
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : ¬r • x = 0
neg : ¬⋯.min (s := (r • x).support) ⋯ < ⋯.min (s := x.support) ⋯
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
simp only [orderTop_of_ne_zero hrx, orderTop_of_ne_zero <| right_ne_zero_of_smul hrx,
      WithTop.coe_lt_coe]

Premises used: right_ne_zero_of_smul, HahnSeries.orderTop_of_ne_zero, WithTop.coe_lt_coe
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : ¬r • x = 0
⊢ ¬⋯.min (s := (r • x).support) ⋯ < ⋯.min (s := x.support) ⋯

Tactic:
Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right ..)

Premises used: Function.support_smul_subset_right, Set.IsWF.min_of_subset_not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
r : R
x : V⟦Γ⟧
hrx : ¬r • x = 0
⊢ ¬⋯.min (s := (r • x).support) ⋯ < ⋯.min (s := x.support) ⋯

Tactic:
exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right ..)

Premises used: Function.support_smul_subset_right, Set.IsWF.min_of_subset_not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
V : Type u_8
inst : Zero V
inst_1 : SMulZeroClass R V
Γ : Type u_9
inst_2 : LinearOrder Γ
r : R
x : V⟦Γ⟧
⊢ x.orderTop ≤ (r • x).orderTop

Tactic:
le_of_not_gt <| orderTop_smul_not_lt r x

Premises used: le_of_not_gt, HahnSeries.orderTop_smul_not_lt
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := right_ne_zero_of_smul h
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
hx : x ≠ 0
simp_all : ¬⋯.min (s := (r • x).support) ⋯ < ⋯.min (s := x.support) ⋯
⊢ ¬(r • x).order < x.order

Tactic:
simp_all only [order, dite_false]

Premises used: HahnSeries.order, dite_false
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬⋯.min (s := (r • x).support) ⋯ < ⋯.min (s := x.support) ⋯

Tactic:
Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right ..)

Premises used: Function.support_smul_subset_right, Set.IsWF.min_of_subset_not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : Zero Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
hx : x ≠ 0
⊢ ¬⋯.min (s := (r • x).support) ⋯ < ⋯.min (s := x.support) ⋯

Tactic:
exact Set.IsWF.min_of_subset_not_lt_min (Function.support_smul_subset_right ..)

Premises used: Function.support_smul_subset_right, Set.IsWF.min_of_subset_not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
V : Type u_8
inst : Zero V
inst_1 : SMulZeroClass R V
Γ : Type u_9
inst_2 : Zero Γ
inst_3 : LinearOrder Γ
r : R
x : V⟦Γ⟧
h : r • x ≠ 0
⊢ x.order ≤ (r • x).order

Tactic:
le_of_not_gt (order_smul_not_lt r x h)

Premises used: le_of_not_gt, HahnSeries.order_smul_not_lt
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : DecidableLT Γ
c : Γ
r : R
x : V⟦Γ⟧
coeff :
  ∀ (x_1 : Γ),
    HahnSeries.coeff ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) (r • x)) x_1 =
      (HSMul.hSMul (β := V⟦Γ⟧) r ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) x : V⟦Γ⟧)).coeff x_1
⊢ (truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) (r • x) = HSMul.hSMul (β := V⟦Γ⟧) r ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) x : V⟦Γ⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
V : Type u_8
inst_1 : Zero V
inst_2 : SMulZeroClass R V
inst_3 : DecidableLT Γ
c : Γ
r : R
x : V⟦Γ⟧
x_1 : Γ
⊢ coeff ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) (r • x)) x_1 =
    (HSMul.hSMul (β := V⟦Γ⟧) r ((truncLT c : (a : V⟦Γ⟧) → V⟦Γ⟧) x : V⟦Γ⟧)).coeff x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x y : R⟦Γ⟧
⊢ (x + y).support ⊆ x.support ∪ y.support

Tactic:
Function.support_add ..

Premises used: HahnSeries.support, Function.support_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x y : R⟦Γ⟧
⊢ (x + y).coeff = x.coeff + y.coeff

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x y : R⟦Γ⟧
a : Γ
⊢ (x + y).coeff a = x.coeff a + y.coeff a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
a : Γ
r s : R
coeff :
  HahnSeries.coeff ((single a : (a : R) → R⟦Γ⟧) (r + s)) =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
⊢ (single a : (a : R) → R⟦Γ⟧) (r + s) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
a : Γ
r s : R
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) (r + s)) =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff

Tactic:
Pi.single_add (f := fun _ => R) a r s

Premises used: Function.update, Pi.single_add, Pi.single, dite
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
a : Γ
r s : R
⊢ coeff ((single a : (a : R) → R⟦Γ⟧) (r + s)) =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff

Tactic:
exact Pi.single_add (f := fun _ => R) a r s

Premises used: Pi.single_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
a : Γ
r s : R
coeff coeff₁ :
  HahnSeries.coeff ((single a : (a : R) → R⟦Γ⟧) (r + s)) =
    (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
        ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)).coeff
⊢ (single a : (a : R) → R⟦Γ⟧) (r + s) =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) s : R⟦Γ⟧)

Tactic:
classical
  ext : 1; exact Pi.single_add (f := fun _ => R) a r s
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧
n : ℕ
⊢ (n • x).coeff = n • x.coeff

Tactic:
coeff_smul' _ _

Premises used: HahnSeries.coeff_smul'
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
coeff : ∀ (x_1 : Γ), HahnSeries.coeff ((x + y).map f) x_1 = (HAdd.hAdd (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1
⊢ (x + y).map f = HAdd.hAdd (α := S⟦Γ⟧) (x.map f) (y.map f)

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : AddMonoid R
inst_2 : AddMonoid S
f : R →+ S
x y : R⟦Γ⟧
x_1 : Γ
⊢ coeff ((x + y).map f) x_1 = (HAdd.hAdd (α := S⟦Γ⟧) (x.map f) (y.map f)).coeff x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ x.support.IsPWO

Tactic:
x.isPWO_support

Premises used: HahnSeries.isPWO_support
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
h : (Function.support.{u_1, u_3} (M := R) fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) = x.support
⊢ Set.IsPWO.{u_1} (α := Γ) (Function.support.{u_1, u_3} (M := R) fun (a : Γ) ↦ AddOpposite.unop (x.coeff a))

Tactic:
convert! x.isPWO_support

Premises used: HahnSeries.isPWO_support