awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
r : R'
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inl r) :
      tsze R' N)
    (inl r : tsze R' N)
rw₂ : Eq (α := tsze R' N) ((Algebra.ofId R' (tsze R' N) : (a : R') → tsze R' N) r : tsze R' N) (inl r : tsze R' N)
rw₃ : Eq (α := tsze R' N) ((algebraMap R' (tsze R' N) : (a : R') → tsze R' N) r : tsze R' N) (inl r : tsze R' N)
rw₄ rw₅ : Eq (α := tsze R' N) (inl r) (inl r)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inl r) : tsze R' N) (inl r : tsze R' N)

Tactic:
rw [map, liftEquivOfComm_apply, lift_apply_inl, Algebra.ofId_apply, algebraMap_eq_inl]

Premises used: Algebra.ofId_apply, TrivSqZeroExt.liftEquivOfComm_apply, TrivSqZeroExt.algebraMap_eq_inl, TrivSqZeroExt.lift_apply_inl, TrivSqZeroExt.map
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : M
rw :
  Eq (α := tsze R' N)
    ((((liftEquivOfComm :
                (a :
                    { f : M →ₗ[R'] tsze R' N //
                      ∀ (x y : M), (f : (a : M) → tsze R' N) x * (f : (a : M) → tsze R' N) y = 0 }) →
                  tsze R' M →ₐ[R'] tsze R' N)
              (Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            tsze R' M →ₐ[R'] tsze R' N) :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₁ :
  Eq (α := tsze R' N)
    ((lift (Algebra.ofId R' (tsze R' N))
            (↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                  ∀ (x y : M),
                    HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                        ((f : (a : M) → tsze R' N) y : tsze R' N) =
                      0)
                  (inrHom R' N ∘ₗ f) ⋯) :
              M →ₗ[R'] tsze R' N)
            ⋯ ⋯ ⋯ :
          (a : tsze R' M) → tsze R' N)
        (inr x) :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₂ :
  Eq (α := tsze R' N)
    (((↑(Subtype.mk (p := fun (f : M →ₗ[R'] tsze R' N) ↦
                ∀ (x y : M),
                  HMul.hMul (α := tsze R' N) (β := tsze R' N) ((f : (a : M) → tsze R' N) x : tsze R' N)
                      ((f : (a : M) → tsze R' N) y : tsze R' N) =
                    0)
                (inrHom R' N ∘ₗ f) ⋯) :
            M →ₗ[R'] tsze R' N) :
          (a : M) → tsze R' N)
        x :
      tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₃ :
  Eq (α := tsze R' N) ((inrHom R' N : (a : N) → tsze R' N) ((f : (a : M) → N) x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)
rw₄ rw₅ : Eq (α := tsze R' N) (inr ((f : (a : M) → N) x) : tsze R' N) (inr ((f : (a : M) → N) x) : tsze R' N)
⊢ Eq (α := tsze R' N) ((map f : (a : tsze R' M) → tsze R' N) (inr x) : tsze R' N)
    (inr ((f : (a : M) → N) x) : tsze R' N)

Tactic:
rw [map, liftEquivOfComm_apply, lift_apply_inr, LinearMap.comp_apply, inrHom_apply]

Premises used: LinearMap.comp_apply, TrivSqZeroExt.lift_apply_inr, TrivSqZeroExt.inrHom_apply, TrivSqZeroExt.liftEquivOfComm_apply, TrivSqZeroExt.map
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : tsze R' M
⊢ fst.{u, u_3} (M := N) ((map f : (a : tsze R' M) → tsze R' N) x) = x.fst

Tactic:
simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

Premises used: Algebra.ofId_apply, TrivSqZeroExt.lift_def, TrivSqZeroExt.algebraMap_eq_inl, TrivSqZeroExt.map
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
x : tsze R' M
⊢ Eq.{u_3 + 1} (α := N) (snd.{u, u_3} (R := R') ((map f : (a : tsze R' M) → tsze R' N) x) : N)
    ((f : (a : M) → N) x.snd : N)

Tactic:
simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

Premises used: Algebra.ofId_apply, TrivSqZeroExt.lift_def, TrivSqZeroExt.algebraMap_eq_inl, TrivSqZeroExt.map
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
⊢ Eq (α := R' →ₐ[R'] tsze R' N) (AlgHom.comp (map f) (inlAlgHom R' R' M)) (inlAlgHom R' R' N)

Tactic:
AlgHom.ext <| map_inl _

Premises used: AlgHom.ext, TrivSqZeroExt.map_inl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
⊢ AlgHom.toLinearMap (map f) ∘ₗ inrHom R' M = inrHom R' N ∘ₗ f

Tactic:
LinearMap.ext <| map_inr _

Premises used: TrivSqZeroExt.map_inr, LinearMap.ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
⊢ Eq (α := tsze R' M →ₐ[R'] R')
    (AlgHom.comp (fstHom R' R' N : tsze R' N →ₐ[R'] R') (map f : tsze R' M →ₐ[R'] tsze R' N)) (fstHom R' R' M)

Tactic:
AlgHom.ext <| fst_map _

Premises used: AlgHom.ext, TrivSqZeroExt.fst_map
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
f : M →ₗ[R'] N
⊢ sndHom R' N ∘ₗ AlgHom.toLinearMap (map f) = f ∘ₗ sndHom R' M

Tactic:
LinearMap.ext <| snd_map _

Premises used: LinearMap.ext, TrivSqZeroExt.snd_map
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
h :
  ∀ (m : M),
    Eq (α := tsze R' M) ((map LinearMap.id : (a : tsze R' M) → tsze R' M) (inr m) : tsze R' M)
      ((AlgHom.id R' (tsze R' M) : (a : tsze R' M) → tsze R' M) (inr m) : tsze R' M)
⊢ Eq (α := tsze R' M →ₐ[R'] tsze R' M) (map LinearMap.id) (AlgHom.id R' (tsze R' M))

Tactic:
apply algHom_ext

Premises used: TrivSqZeroExt.algHom_ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
⊢ ∀ (m : M),
    Eq (α := tsze R' M) ((map LinearMap.id : (a : tsze R' M) → tsze R' M) (inr m) : tsze R' M)
      ((AlgHom.id R' (tsze R' M) : (a : tsze R' M) → tsze R' M) (inr m) : tsze R' M)

Tactic:
simp only [map_inr, LinearMap.id_coe, id_eq, AlgHom.coe_id, forall_const]

Premises used: TrivSqZeroExt.map_inr, AlgHom.coe_id, LinearMap.id_coe, forall_const, id_eq
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
inst_9 : AddCommMonoid P
inst_10 : Module R' P
inst_11 : Module.{u, u_4} R'ᵐᵒᵖ P
inst_12 : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
h :
  ∀ (m : M),
    Eq (α := tsze R' P) ((map (g ∘ₗ f) : (a : tsze R' M) → tsze R' P) (inr m) : tsze R' P)
      ((AlgHom.comp (map g) (map f) : (a : tsze R' M) → tsze R' P) (inr m) : tsze R' P)
⊢ Eq (α := tsze R' M →ₐ[R'] tsze R' P) (map (g ∘ₗ f)) (AlgHom.comp (map g) (map f))

Tactic:
apply algHom_ext

Premises used: TrivSqZeroExt.algHom_ext
-- Module: Mathlib.Algebra.TrivSqZeroExt.Basic
Goal:
R' : Type u
M : Type v
inst : CommSemiring R'
inst_1 : AddCommMonoid M
inst_2 : Module R' M
inst_3 : Module.{u, v} R'ᵐᵒᵖ M
inst_4 : IsCentralScalar R' M
N : Type u_3
P : Type u_4
inst_5 : AddCommMonoid N
inst_6 : Module R' N
inst_7 : Module.{u, u_3} R'ᵐᵒᵖ N
inst_8 : IsCentralScalar R' N
inst_9 : AddCommMonoid P
inst_10 : Module R' P
inst_11 : Module.{u, u_4} R'ᵐᵒᵖ P
inst_12 : IsCentralScalar R' P
f : M →ₗ[R'] N
g : N →ₗ[R'] P
⊢ ∀ (m : M),
    Eq (α := tsze R' P) ((map (g ∘ₗ f) : (a : tsze R' M) → tsze R' P) (inr m) : tsze R' P)
      ((AlgHom.comp (map g) (map f) : (a : tsze R' M) → tsze R' P) (inr m) : tsze R' P)

Tactic:
simp only [map_inr, LinearMap.coe_comp, Function.comp_apply, AlgHom.coe_comp, forall_const]

Premises used: TrivSqZeroExt.map_inr, AlgHom.coe_comp, LinearMap.coe_comp, forall_const, Function.comp_apply
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : TrivSqZeroExt R M
obtain :
  ∀ (r : R) (m : M),
    Membership.mem (γ := Ideal (TrivSqZeroExt R M)) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) (r, m) ↔
      (r, m) = inr (snd (r, m))
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) x ↔ x = inr x.snd

Tactic:
obtain ⟨r, m⟩ := x
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
simp : r = 0 ↔ (r, m) = inr (snd (r, m))
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) (r, m) ↔
    (r, m) = inr (snd (r, m))

Tactic:
simp only [kerIdeal, RingHom.mem_ker, fstHom_apply, fst_mk]

Premises used: RingHom.mem_ker, TrivSqZeroExt.kerIdeal, TrivSqZeroExt.fstHom_apply, TrivSqZeroExt.fst_mk
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
hr : r = 0
rw : Eq (α := TrivSqZeroExt R M) (0, m) (inr (snd.{u_1, u_2} (R := R) (0, m)))
⊢ (r, m) = inr (snd (r, m))

Tactic:
rw [hr]
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
hr : r = 0
⊢ Eq (α := TrivSqZeroExt R M) (0, m) (inr (snd.{u_1, u_2} (R := R) (0, m)))

Tactic:
rfl
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
hrm : (r, m) = inr (snd (r, m))
rw : fst (r, m) = 0
rw₁ : Eq.{u_1 + 1} (α := R) (fst (inr (snd (r, m)))) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ r = 0

Tactic:
rw [← fst_mk r m, hrm, fst_inr]

Premises used: TrivSqZeroExt.fst_inr, TrivSqZeroExt.fst_mk
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
r : R
m : M
⊢ r = 0 ↔ (r, m) = inr (snd (r, m))

Tactic:
exact ⟨fun hr => by rw [hr]; rfl, fun hrm => by rw [← fst_mk r m, hrm, fst_inr]⟩
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
simp :
  ∀ (r : TrivSqZeroExt R M),
    r = inr r.snd → ∀ (s : TrivSqZeroExt R M), s = inr s.snd → Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (r * s)
⊢ HPow.hPow (α := Ideal (TrivSqZeroExt R M)) (β := ℕ) (kerIdeal R M : Ideal (TrivSqZeroExt R M)) 2 = ⊥

Tactic:
simp only [pow_two, eq_bot_iff, mul_le, mem_kerIdeal_iff_inr]

Premises used: pow_two, Ideal.mul_le, eq_bot_iff, TrivSqZeroExt.mem_kerIdeal_iff_inr
-- Module: Mathlib.Algebra.TrivSqZeroExt.Ideal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : TrivSqZeroExt R M
hx : x = inr x.snd
y : TrivSqZeroExt R M
hy : y = inr y.snd
rw : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (inr x.snd * y)
rw₁ : Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (HMul.hMul (α := TrivSqZeroExt R M) (inr x.snd) (inr y.snd))
rw₂ : HMul.hMul (α := TrivSqZeroExt R M) (inr x.snd) (inr y.snd) = 0
rw₃ rw₄ : Eq (α := TrivSqZeroExt R M) 0 0
⊢ Membership.mem (γ := Ideal (TrivSqZeroExt R M)) ⊥ (x * y)

Tactic:
rw [hx, hy, mem_bot, inr_mul_inr]

Premises used: Ideal.mem_bot, TrivSqZeroExt.inr_mul_inr
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := R) trop

Tactic:
fun _ _ => id

Premises used: id, Tropical, Function.Injective, Tropical.trop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := Tropical R) untrop

Tactic:
fun _ _ => id

Premises used: id, Tropical, Function.Injective, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x y : R
⊢ trop x = trop y ↔ x = y

Tactic:
Iff.rfl

Premises used: Iff.rfl, Tropical, Tropical.trop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x y : Tropical R
⊢ untrop x = untrop y ↔ x = y

Tactic:
Iff.rfl

Premises used: Iff.rfl, Tropical, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x : Tropical R
⊢ trop (untrop x) = x

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x : R
⊢ untrop (trop x) = x

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.LeftInverse.{u + 1, u + 1} (α := Tropical R) trop untrop

Tactic:
trop_untrop

Premises used: Function.LeftInverse, Tropical.trop_untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.RightInverse.{u + 1, u + 1} (α := Tropical R) trop untrop

Tactic:
untrop_trop

Premises used: Function.LeftInverse, Function.RightInverse, Tropical.untrop_trop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Eq.{u + 1} (α := (a : R) → Tropical R) (⇑tropEquiv : (a : R) → Tropical R) trop

Tactic:
rfl

Premises used: Tropical.trop, rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Eq.{u + 1} (α := (a : Tropical R) → R) (⇑(Equiv.symm tropEquiv) : (a : Tropical R) → R) untrop

Tactic:
rfl

Premises used: rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x : R
y : Tropical R
⊢ trop x = y ↔ x = untrop y

Tactic:
tropEquiv.apply_eq_iff_eq_symm_apply

Premises used: Tropical.tropEquiv, Tropical.trop, Tropical.untrop, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x : Tropical R
y : R
⊢ untrop x = y ↔ x = trop y

Tactic:
tropEquiv.symm.apply_eq_iff_eq_symm_apply

Premises used: Tropical.tropEquiv, Equiv.symm, Tropical.trop, Tropical.untrop, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := R) trop

Tactic:
tropEquiv.injective

Premises used: Tropical.tropEquiv, Equiv.injective, Tropical.trop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := Tropical R) untrop

Tactic:
tropEquiv.symm.injective

Premises used: Tropical.tropEquiv, Equiv.injective, Equiv.symm, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.Surjective.{u + 1, u + 1} (α := R) trop

Tactic:
tropEquiv.surjective

Premises used: Tropical.tropEquiv, Equiv.surjective, Tropical.trop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
⊢ Function.Surjective.{u + 1, u + 1} (α := Tropical R) untrop

Tactic:
tropEquiv.symm.surjective

Premises used: Tropical.tropEquiv, Equiv.surjective, Equiv.symm, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LE R
x y : Tropical R
⊢ untrop x ≤ untrop y ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LT R
x y : Tropical R
⊢ untrop x < untrop y ↔ x < y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Preorder R
⊢ Eq.{u + 1} (α := (a : R) → Tropical R) (⇑tropOrderIso : (a : R) → Tropical R) trop

Tactic:
rfl

Premises used: Tropical.trop, rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Preorder R
⊢ Eq.{u + 1} (α := (a : Tropical R) → R) (⇑(OrderIso.symm tropOrderIso) : (a : Tropical R) → R) untrop

Tactic:
rfl

Premises used: rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Preorder R
⊢ Monotone.{u, u} (α := R) trop

Tactic:
fun _ _ => id

Premises used: Monotone, id, Tropical.trop, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Preorder R
⊢ Monotone.{u, u} (α := Tropical R) untrop

Tactic:
fun _ _ => id

Premises used: Monotone, id
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Top R
⊢ Eq.{u + 1} (α := R) (untrop 0) ⊤

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : Top R
⊢ Eq.{u + 1} (α := Tropical R) (trop ⊤) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x : R
⊢ trop (↑x : WithTop R) ≠ 0

Tactic:
nofun

Premises used: False, _private.0.Tropical.trop_coe_ne_zero.match_1, Not
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
x : R
⊢ 0 ≠ trop (↑x : WithTop R)

Tactic:
nofun

Premises used: False, _private.0.Tropical.zero_ne_trop_coe.match_1, Not
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LE R
inst_1 : OrderTop R
x : Tropical R
⊢ x ≤ 0

Tactic:
le_top (α := R)

Premises used: le_top, Tropical.trop, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
⊢ untrop (x + y) = min (untrop x) (untrop y)

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : R
⊢ trop (min x y) = trop x + trop y

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
⊢ x + y = trop (min (untrop x) (untrop y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
simp : (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
⊢ untrop (a + b) = untrop (if a ≤ b then a else b)

Tactic:
simp only [untrop_add, min_def, untrop_le_iff]

Premises used: Tropical.untrop_add, min_def, Tropical.untrop_le_iff
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
pos : a ≤ b → untrop a = untrop a
neg : ¬a ≤ b → untrop b = untrop b
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
h : a ≤ b
⊢ untrop a = untrop a

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
h : ¬a ≤ b
⊢ untrop b = untrop b

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
simp : (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)
⊢ untrop (trop (max (untrop a) (untrop b))) = untrop (if a ≤ b then b else a)

Tactic:
simp only [max_def, untrop_le_iff, untrop_trop]

Premises used: Tropical.untrop_le_iff, Tropical.untrop_trop, max_def
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
pos : a ≤ b → untrop b = untrop b
neg : ¬a ≤ b → untrop a = untrop a
⊢ (if a ≤ b then untrop b else untrop a) = untrop (if a ≤ b then b else a)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
h : a ≤ b
⊢ untrop b = untrop b

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
a b : Tropical R
h : ¬a ≤ b
⊢ untrop a = untrop a

Tactic:
simp
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
⊢ untrop (max x y) = max (untrop x) (untrop y)

Tactic:
rfl

Premises used: Tropical.trop, rfl, Tropical.untrop
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
⊢ Eq.{u + 1} (α := Tropical R → Tropical R → Tropical R) min fun (x1 x2 : Tropical R) ↦ x1 + x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
⊢ Eq.{u + 1} (α := Tropical R → Tropical R → Tropical R) (fun (x1 x2 : Tropical R) ↦ min x1 x2)
    fun (x1 x2 : Tropical R) ↦ x1 + x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
⊢ max x y = trop (max (untrop x) (untrop y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ untrop (x + y) = untrop x

Tactic:
simpa using h
-- Module: Mathlib.Algebra.Tropical.Basic
Goal:
R : Type u
inst : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ untrop (x + y) = untrop y

Tactic:
simpa using h