awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
            (const 1 1 (op ⦋0⦌)) :
          (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1 :
          TopCat.toSSet.obj TopCat.I _⦋0⦌) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
have trans : (Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
        (const 1 1 (op ⦋0⦌)) :
      (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) =
  stdSimplex.δ 0 ≫ toSSetObjI
Tactic: trans stdSimplex.δ 0 ≫ toSSetObjI
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
trans :
  (Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
            (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
          (const 1 1 (op ⦋0⦌)) :
        (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) =
    stdSimplex.δ 0 ≫ toSSetObjI
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (toSSetObjI.app (op ⦋0⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (Δ[1] _⦋0⦌)) → (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌))
            (const 1 1 (op ⦋0⦌)) :
          (fun (X : Type u_1) ↦ X) (TopCat.toSSet.obj TopCat.I _⦋0⦌)) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1 :
          TopCat.toSSet.obj TopCat.I _⦋0⦌) :
      Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
have trans₁ : stdSimplex.δ 0 ≫ toSSetObjI =
  (Equiv.symm yonedaEquiv : (a : TopCat.toSSet.obj TopCat.I _⦋0⦌) → Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u_1)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 1 :
      TopCat.toSSet.obj TopCat.I _⦋0⦌)
Tactic: trans stdSimplex.δ 0 ≫ toSSetObjI
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₀
have rw : ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
Tactic: rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
have h_fst : (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
    SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
  (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
    SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
h_fst :
  (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
⊢ ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
have h_snd : (ι₀ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
    SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
  (TopCat.toSSet.map TopCat.ι₀ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
    SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI ≫ Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I = TopCat.toSSet.map TopCat.ι₁
have rw : ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
Tactic: rw [← cancel_mono (μIso _ _ _).inv, Category.assoc, Category.assoc, μIso_inv,
    μ_δ, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
have h_fst : (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
    SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
  (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
    SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
h_fst :
  (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I
have h_snd : (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
    SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
  (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
    SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SingularHomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
inst_3 : HasPullbacks.{v, u} C
X : C
X_1 Y : TopCat
f : X_1 ⟶ Y
h : Mono f
⊢ Mono (C := ChainComplex.{v, u, 0} C ℕ) (X := Functor.obj (Functor.obj (singularChainComplexFunctor C) X) X_1)
    (CategoryTheory.Functor.map (Functor.obj (singularChainComplexFunctor C) X) f)
have dsimp : Mono (C := ChainComplex.{v, u, 0} C ℕ) (X :=
  Functor.obj (alternatingFaceMapComplex C)
    (Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.obj X_1)))
  (CategoryTheory.Functor.map (alternatingFaceMapComplex C)
    (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.map f)))
Tactic: dsimp [singularChainComplexFunctor, SSet.chainComplexFunctor]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SingularHomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
inst_3 : HasPullbacks.{v, u} C
X : C
X_1 Y : TopCat
f : X_1 ⟶ Y
h : Mono f
⊢ Mono (C := ChainComplex.{v, u, 0} C ℕ) (X :=
    Functor.obj (alternatingFaceMapComplex C)
      (Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
        (TopCat.toSSet.obj X_1)))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C)
      (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
        (TopCat.toSSet.map f)))
have inst : Mono (C := SimplicialObject.{v, u} C) (X :=
  Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X)) (TopCat.toSSet.obj X_1))
  (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
    (TopCat.toSSet.map f))
Tactic: apply +allowSynthFailures Functor.map_mono
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SingularHomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
inst_3 : HasPullbacks.{v, u} C
X : C
X_1 Y : TopCat
f : X_1 ⟶ Y
h : Mono f
⊢ Mono (C := SimplicialObject.{v, u} C) (X :=
    Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.obj X_1))
    (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.map f))
have inst : Functor.PreservesMonomorphisms (D := SimplicialObject.{v, u} C)
  (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
Tactic: apply +allowSynthFailures Functor.map_mono
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SingularHomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ CategoryStruct.comp (Y :=
      sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
        Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
      (Sigma.ι.{w, v, u} (C := C)
          (fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
            Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
          i :
        Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F ⟶
          sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
            Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
      (NatTrans.app (NatTrans.app (Adjunction.counit (singularChainComplexFunctorAdjunction C n)) F) X :
        (Functor.obj
                (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌) ⋙
                  Functor.obj (C := C ⥤ TopCat ⥤ HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                    (Functor.obj Functor.postcompose₂ (eval C (ComplexShape.down ℕ) n)) (singularChainComplexFunctor C))
                F).obj
            X ⟶
          (Functor.obj (𝟭 (CategoryTheory.Functor.{w, v, w + 1, u} TopCat C)) F).obj X) =
    F.map i.down
have trans : CategoryStruct.comp (Y :=
    sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
      Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
    (Sigma.ι.{w, v, u} (C := C)
        (fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
          Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
        i :
      Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F ⟶
        sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
          Functor.obj (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌)) F)
    (NatTrans.app (NatTrans.app (Adjunction.counit (singularChainComplexFunctorAdjunction C n)) F) X :
      (Functor.obj
              (Functor.obj (evaluation TopCat C) (SimplexCategory.toTop.{w} ^⦋n⦌) ⋙
                Functor.obj (C := C ⥤ TopCat ⥤ HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
                  (Functor.obj Functor.postcompose₂ (eval C (ComplexShape.down ℕ) n)) (singularChainComplexFunctor C))
              F).obj
          X ⟶
        (Functor.obj (𝟭 (CategoryTheory.Functor.{w, v, w + 1, u} TopCat C)) F).obj X) =
  F.map
    (toTopSimplex.inv.app ⦋n⦌ ≫
      toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
        sSetTopAdj.counit.app X)
Tactic: trans F.map (SSet.toTopSimplex.inv.app ⦋n⦌ ≫ SSet.toTop.map (SSet.yonedaEquiv.symm i) ≫
      sSetTopAdj.counit.app X)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SingularHomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ F.map
      (toTopSimplex.inv.app ⦋n⦌ ≫
        toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
          sSetTopAdj.counit.app X) =
    F.map i.down
have e_a : toTopSimplex.inv.app ⦋n⦌ ≫
    toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
      sSetTopAdj.counit.app X =
  i.down
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SingularHomology.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ toTopSimplex.inv.app ⦋n⦌ ≫
      toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
        sSetTopAdj.counit.app X =
    i.down
have e_a : ULift.down
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (sSetTopAdj.unit.app (TopCat.toSSet.obj X)) (Opposite.op ⦋n⦌)) :
          (a : TopCat.toSSet.obj X _⦋n⦌) → TopCat.toSSet.obj (toTop.obj (TopCat.toSSet.obj X)) _⦋n⦌)
        i) ≫
    sSetTopAdj.counit.app X =
  i.down
Tactic: rw [← reassoc_of% sSetTopAdj_unit_app_app_down]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
⊢ v.IsEquiv w ↔
    ∀ (x : R),
      LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
have refine : ∀
  (h :
    ∀ (x : R),
      LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S))
  (x y : R),
  LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)
Tactic: refine ⟨fun h _ ↦ h.lt_one_iff, fun h x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)
have inl : Eq.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S) →
  (LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S))
Tactic: rcases eq_or_ne (v x) 0 with (_ | hy₀)
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
inl :
  Eq.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S) →
    (LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
      LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S))
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)
have inr : ∀ (hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)),
  LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)
Tactic: rcases eq_or_ne (v x) 0 with (_ | hy₀)
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
x y : R
hy₀ : Ne.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) (0 : S)
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)
have inr : LT.lt.{u_2} (α := S) ((v : (a : R) → S) (y * x⁻¹) : S) (1 : S) ↔
  LT.lt.{u_2} (α := S) ((w : (a : R) → S) (y * x⁻¹) : S) (1 : S)
Tactic: rw [le_iff_le_iff_lt_iff_lt, ← one_mul (v x), ← mul_inv_lt_iff₀ (by simp_all), ← one_mul (w x),
    ← mul_inv_lt_iff₀ (by simp_all), ← map_inv₀, ← map_mul, ← map_inv₀, ← map_mul]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
⊢ v.IsEquiv w
have refine : ∀ (a : R),
  LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
Tactic: refine isEquiv_iff_lt_one_iff.2 fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
have inl : LT.lt.{u_2} (α := S) ((v : (a : R) → S) 0 : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) 0 : S) (1 : S)
Tactic: rcases eq_or_ne a 0 with (rfl | ha₀)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
inl : LT.lt.{u_2} (α := S) ((v : (a : R) → S) 0 : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) 0 : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
have inr : ∀ (ha₀ : a ≠ 0),
  LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
Tactic: rcases eq_or_ne a 0 with (rfl | ha₀)
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
have inr : ∀ (hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)), LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)
Tactic: refine ⟨h a, fun hw ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)
have inr : ∀ (x₀ : R) (hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)),
  LT.lt.{u_2} (α := S) ((v : (a : R) → S) a : S) (1 : S)
Tactic: let ⟨x₀, hx₀⟩ := hv.exists_abv_lt_one
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ (w : (a : R) → S) x₀ < HPow.hPow (α := S) ((w : (a : R) → S) a : S) n
have rw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)
Tactic: rw [← one_mul (_ ^ _), ← mul_inv_lt_iff₀ (pow_pos (by simp_all) _),
      ← map_pow, ← map_inv₀, ← map_mul]
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ LT.lt.{u_2} (α := S) ((w : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)
have a₁ : LT.lt.{u_2} (α := S) ((v : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Analysis.AbsoluteValue.Equivalence (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Field R
inst_1 : Semifield S
inst_2 : LinearOrder S
v w : AbsoluteValue R S
inst_3 : IsStrictOrderedRing S
inst_4 : Archimedean S
inst_5 : ExistsAddOfLE S
hv_1 : v.IsNontrivial
h :
  ∀ (x : R),
    LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) → LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)
a : R
ha₀ : a ≠ 0
hw : LT.lt.{u_2} (α := S) ((w : (a : R) → S) a : S) (1 : S)
x₀ : R
hx₀ : x₀ ≠ 0 ∧ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x₀ : S) (1 : S)
n : ℕ
hv : LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) a : S)
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) (x₀ * (a ^ n)⁻¹) : S) (1 : S)
have a₁ : (v : (a : R) → S) x₀ < HPow.hPow (α := S) ((v : (a : R) → S) a : S) n
Tactic: rw [map_mul, map_inv₀, map_pow, mul_inv_lt_iff₀ (pow_pos (by simp [ha₀]) _), one_mul]