[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ Disjoint (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst)
    (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd)
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ ∀ ⦃a : γ⦄,
    a ∈ Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst →
      ¬a ∈ Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd
[PROOFSTEP]
rintro _ ⟨a, h⟩ ⟨b, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h :
  ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst a =
    ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd b
⊢ False
[PROOFSTEP]
simp only [trans_apply, inl_apply, inr_apply] at h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h : ↑(Function.Embedding.trans inl f) a = ↑(Function.Embedding.trans inr f) b
⊢ False
[PROOFSTEP]
have : Sum.inl a = Sum.inr b := f.injective h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
a : α
b : β
h : ↑(Function.Embedding.trans inl f) a = ↑(Function.Embedding.trans inr f) b
this : Sum.inl a = Sum.inr b
⊢ False
[PROOFSTEP]
simp only at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
⊢ Function.Injective fun x =>
    match x with
    | Sum.inl a => ↑f a
    | Sum.inr b => ↑g b
[PROOFSTEP]
rintro (a₁ | b₁) (a₂ | b₂) f_eq
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ a₂ : α
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ : β
a₂ : α
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ b₂ : β
f_eq :
  (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₁) =
    (fun x =>
        match x with
        | Sum.inl a => ↑f a
        | Sum.inr b => ↑g b)
      (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂
[PROOFSTEP]
simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ a₂ : α
f_eq : ↑f a₁ = ↑f a₂
⊢ Sum.inl a₁ = Sum.inl a₂
[PROOFSTEP]
rw [f.injective f_eq]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq : ↑f a₁ = ↑g b₂
⊢ Sum.inl a₁ = Sum.inr b₂
[PROOFSTEP]
exfalso
[GOAL]
case inl.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq : ↑f a₁ = ↑g b₂
⊢ False
[PROOFSTEP]
refine disj.le_bot ⟨⟨a₁, f_eq⟩, ⟨b₂, by simp [f_eq]⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
a₁ : α
b₂ : β
f_eq : ↑f a₁ = ↑g b₂
⊢ ↑(f, g).snd b₂ = ↑g b₂
[PROOFSTEP]
simp [f_eq]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ : β
a₂ : α
f_eq : ↑g b₁ = ↑f a₂
⊢ Sum.inr b₁ = Sum.inl a₂
[PROOFSTEP]
exfalso
[GOAL]
case inr.inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ : β
a₂ : α
f_eq : ↑g b₁ = ↑f a₂
⊢ False
[PROOFSTEP]
exact disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
b₁ b₂ : β
f_eq : ↑g b₁ = ↑g b₂
⊢ Sum.inr b₁ = Sum.inr b₂
[PROOFSTEP]
rw [g.injective f_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ (fun x =>
        match x with
        | { val := (f, g), property := disj } =>
          {
            toFun := fun x =>
              match x with
              | Sum.inl a => ↑f a
              | Sum.inr b => ↑g b,
            inj' :=
              (_ :
                ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                  (fun x =>
                          match x with
                          | Sum.inl a => ↑f a
                          | Sum.inr b => ↑g b)
                        a₁ =
                      (fun x =>
                          match x with
                          | Sum.inl a => ↑f a
                          | Sum.inr b => ↑g b)
                        a₂ →
                    a₁ = a₂) })
      ((fun f =>
          { val := (Function.Embedding.trans inl f, Function.Embedding.trans inr f),
            property :=
              (_ :
                Disjoint (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst)
                  (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd)) })
        f) =
    f
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
⊢ {
      toFun := fun x =>
        match x with
        | Sum.inl a => ↑(Function.Embedding.trans inl f) a
        | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
      inj' :=
        (_ :
          ∀ ⦃a₁ a₂ : α ⊕ β⦄,
            ((match a₁ with
                | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                match a₂ with
                | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
              a₁ = a₂) } =
    f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
x : α ⊕ β
⊢ ↑{
          toFun := fun x =>
            match x with
            | Sum.inl a => ↑(Function.Embedding.trans inl f) a
            | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                ((match a₁ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                    match a₂ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
                  a₁ = a₂) }
      x =
    ↑f x
[PROOFSTEP]
cases x
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : α
⊢ ↑{
          toFun := fun x =>
            match x with
            | Sum.inl a => ↑(Function.Embedding.trans inl f) a
            | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                ((match a₁ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                    match a₂ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
                  a₁ = a₂) }
      (Sum.inl val✝) =
    ↑f (Sum.inl val✝)
[PROOFSTEP]
simp!
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β ↪ γ
val✝ : β
⊢ ↑{
          toFun := fun x =>
            match x with
            | Sum.inl a => ↑(Function.Embedding.trans inl f) a
            | Sum.inr b => ↑(Function.Embedding.trans inr f) b,
          inj' :=
            (_ :
              ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                ((match a₁ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) =
                    match a₂ with
                    | Sum.inl a => ↑(Function.Embedding.trans inl f) a
                    | Sum.inr b => ↑(Function.Embedding.trans inr f) b) →
                  a₁ = a₂) }
      (Sum.inr val✝) =
    ↑f (Sum.inr val✝)
[PROOFSTEP]
simp!
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
property✝ : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
⊢ (fun f =>
        { val := (Function.Embedding.trans inl f, Function.Embedding.trans inr f),
          property :=
            (_ :
              Disjoint (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).fst)
                (Set.range ↑(Function.Embedding.trans inl f, Function.Embedding.trans inr f).snd)) })
      ((fun x =>
          match x with
          | { val := (f, g), property := disj } =>
            {
              toFun := fun x =>
                match x with
                | Sum.inl a => ↑f a
                | Sum.inr b => ↑g b,
              inj' :=
                (_ :
                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                    (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₁ =
                        (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₂ →
                      a₁ = a₂) })
        { val := (f, g), property := property✝ }) =
    { val := (f, g), property := property✝ }
[PROOFSTEP]
simp only [Prod.mk.inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ↑f.fst) (Set.range ↑f.snd) }
f : α ↪ γ
g : β ↪ γ
property✝ : Disjoint (Set.range ↑(f, g).fst) (Set.range ↑(f, g).snd)
⊢ {
      val :=
        (Function.Embedding.trans inl
            {
              toFun := fun x =>
                match x with
                | Sum.inl a => ↑f a
                | Sum.inr b => ↑g b,
              inj' :=
                (_ :
                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                    (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₁ =
                        (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₂ →
                      a₁ = a₂) },
          Function.Embedding.trans inr
            {
              toFun := fun x =>
                match x with
                | Sum.inl a => ↑f a
                | Sum.inr b => ↑g b,
              inj' :=
                (_ :
                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                    (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₁ =
                        (fun x =>
                            match x with
                            | Sum.inl a => ↑f a
                            | Sum.inr b => ↑g b)
                          a₂ →
                      a₁ = a₂) }),
      property :=
        (_ :
          Disjoint
            (Set.range
              ↑(Function.Embedding.trans inl
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ }),
                    Function.Embedding.trans inr
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ })).fst)
            (Set.range
              ↑(Function.Embedding.trans inl
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ }),
                    Function.Embedding.trans inr
                      ((fun x =>
                          match x with
                          | { val := (f, g), property := disj } =>
                            {
                              toFun := fun x =>
                                match x with
                                | Sum.inl a => ↑f a
                                | Sum.inr b => ↑g b,
                              inj' :=
                                (_ :
                                  ∀ ⦃a₁ a₂ : α ⊕ β⦄,
                                    (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₁ =
                                        (fun x =>
                                            match x with
                                            | Sum.inl a => ↑f a
                                            | Sum.inr b => ↑g b)
                                          a₂ →
                                      a₁ = a₂) })
                        { val := (f, g), property := property✝ })).snd)) } =
    { val := (f, g), property := property✝ }
[PROOFSTEP]
constructor
[GOAL]
α : Type u_1
β : Type u_2
bs : Set β
x : { f // ∀ (a : α), ↑f a ∈ bs }
⊢ (fun f => { val := Function.Embedding.trans f (subtype fun x => x ∈ bs), property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
      ((fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs)) x) =
    x
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
bs : Set β
x : { f // ∀ (a : α), ↑f a ∈ bs }
x✝ : α
⊢ ↑↑((fun f =>
              { val := Function.Embedding.trans f (subtype fun x => x ∈ bs),
                property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
            ((fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs)) x))
      x✝ =
    ↑↑x x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
bs : Set β
x : α ↪ ↑bs
⊢ (fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs))
      ((fun f =>
          { val := Function.Embedding.trans f (subtype fun x => x ∈ bs), property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
        x) =
    x
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u_1
β : Type u_2
bs : Set β
x : α ↪ ↑bs
x✝ : α
⊢ ↑(↑((fun f => Function.Embedding.codRestrict bs ↑f (_ : ∀ (a : α), ↑↑f a ∈ bs))
            ((fun f =>
                { val := Function.Embedding.trans f (subtype fun x => x ∈ bs),
                  property := (_ : ∀ (a : α), ↑(↑f a) ∈ bs) })
              x))
        x✝) =
    ↑(↑x x✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
⊢ (fun b => Disjoint (Set.range ↑a) (Set.range ↑b)) = fun f => ∀ (a_1 : β), ↑f a_1 ∈ (Set.range ↑a)ᶜ
[PROOFSTEP]
ext f
[GOAL]
case h.a
α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
f : β ↪ γ
⊢ Disjoint (Set.range ↑a) (Set.range ↑f) ↔ ∀ (a_1 : β), ↑f a_1 ∈ (Set.range ↑a)ᶜ
[PROOFSTEP]
rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
⊢ (fun x =>
        { toFun := fun x_1 => x, inj' := (_ : ∀ (x_1 x_2 : α), (fun x_3 => x) x_1 = (fun x_3 => x) x_2 → x_1 = x_2) })
      ((fun f => ↑f default) x✝) =
    x✝
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ ↑((fun x =>
            { toFun := fun x_1 => x,
              inj' := (_ : ∀ (x_1 x_2 : α), (fun x_3 => x) x_1 = (fun x_3 => x) x_2 → x_1 = x_2) })
          ((fun f => ↑f default) x✝))
      x =
    ↑x✝ x
[PROOFSTEP]
simp_rw [Function.Embedding.coeFn_mk]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ ↑x✝ default = ↑x✝ x
[PROOFSTEP]
congr 1
[GOAL]
case h.h.e_6.h
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : α ↪ β
x : α
⊢ default = x
[PROOFSTEP]
exact Subsingleton.elim _ x
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Unique α
x✝ : β
⊢ (fun f => ↑f default)
      ((fun x =>
          { toFun := fun x_1 => x, inj' := (_ : ∀ (x_1 x_2 : α), (fun x_3 => x) x_1 = (fun x_3 => x) x_2 → x_1 = x_2) })
        x✝) =
    x✝
[PROOFSTEP]
simp


[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e₁ e₂ : α ≃ β
h₁ : e₁.toFun = e₂.toFun
h₂ : e₁.invFun = e₂.invFun
⊢ e₁ = e₂
[PROOFSTEP]
cases e₁
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
e₂ : α ≃ β
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
h₁ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun = e₂.toFun
h₂ : { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFun
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂
[PROOFSTEP]
cases e₂
[GOAL]
case mk.mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝¹ : α → β
invFun✝¹ : β → α
left_inv✝¹ : LeftInverse invFun✝¹ toFun✝¹
right_inv✝¹ : Function.RightInverse invFun✝¹ toFun✝¹
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
h₁ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun
h₂ :
  { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun
⊢ { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
congr
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.16583
h : α = β
x✝ : α
⊢ cast (_ : β = α) (cast h x✝) = x✝
[PROOFSTEP]
cases h
[GOAL]
case refl
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort ?u.16583
x✝ : α
⊢ cast (_ : α = α) (cast (_ : α = α) x✝) = x✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.16583
h : α = β
x✝ : β
⊢ cast h (cast (_ : β = α) x✝) = x✝
[PROOFSTEP]
cases h
[GOAL]
case refl
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort ?u.16583
x✝ : α
⊢ cast (_ : α = α) (cast (_ : α = α) x✝) = x✝
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ ↑e = id
[PROOFSTEP]
rw [Perm.subsingleton_eq_refl e, coe_refl]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
⊢ ↑f x = y ↔ x = ↑f.symm y
[PROOFSTEP]
conv_lhs => rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
| ↑f x = y
[PROOFSTEP]
rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
| ↑f x = y
[PROOFSTEP]
rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
| ↑f x = y
[PROOFSTEP]
rw [← apply_symm_apply f y]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
x : α
y : (fun x => β) x
f : α ≃ β
⊢ ↑f x = ↑f (↑f.symm y) ↔ x = ↑f.symm y
[PROOFSTEP]
rw [apply_eq_iff_eq]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ✝ : Sort w
α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ ↑((Equiv.cast h).trans (Equiv.cast h2)) x = ↑(Equiv.cast (_ : α = γ)) x
[PROOFSTEP]
substs h h2
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
x : α
⊢ ↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x
[PROOFSTEP]
rfl
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort u_1
h : α = β
a : α
b : β
⊢ ↑(Equiv.cast h) a = b ↔ HEq a b
[PROOFSTEP]
subst h
[GOAL]
α✝ : Sort u
β : Sort v
γ : Sort w
α : Sort u_1
a b : α
⊢ ↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b
[PROOFSTEP]
simp [coe_refl]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : (fun x => α) x
H : ↑e.symm x = y
⊢ x = ↑e y
[PROOFSTEP]
simp [H.symm]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : (fun x => α) x
H : x = ↑e y
⊢ ↑e.symm x = y
[PROOFSTEP]
simp [H]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ e.symm.symm = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.symm.symm =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ (Equiv.refl α).trans e = e
[PROOFSTEP]
cases e
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : Function.RightInverse invFun✝ toFun✝
⊢ (Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ ∀ (x : β), ↑(e.symm.trans e) x = ↑(Equiv.refl β) x
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
⊢ ∀ (x : α), ↑(e.trans e.symm) x = ↑(Equiv.refl α) x
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
⊢ (fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac) = ac
[PROOFSTEP]
ext x
[GOAL]
case H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
x : α
⊢ ↑((fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac)) x = ↑ac x
[PROOFSTEP]
simp only [trans_apply, comp_apply, symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : β ≃ δ
⊢ (fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac) = ac
[PROOFSTEP]
ext x
[GOAL]
case H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort ?u.23940
ab : α ≃ β
cd : γ ≃ δ
ac : β ≃ δ
x : β
⊢ ↑((fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac)) x = ↑ac x
[PROOFSTEP]
simp only [trans_apply, comp_apply, apply_symm_apply]
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
⊢ equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)
[PROOFSTEP]
ext
[GOAL]
case H.H
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
x✝¹ : α ≃ β
x✝ : α
⊢ ↑(↑(equivCongr (Equiv.refl α) (Equiv.refl β)) x✝¹) x✝ = ↑(↑(Equiv.refl (α ≃ β)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (equivCongr ab cd).symm = equivCongr ab.symm cd.symm
[PROOFSTEP]
ext
[GOAL]
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ↑(↑(equivCongr ab cd).symm x✝¹) x✝ = ↑(↑(equivCongr ab.symm cd.symm) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)
[PROOFSTEP]
ext
[GOAL]
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
x✝¹ : α ≃ δ
x✝ : γ
⊢ ↑(↑((equivCongr ab de).trans (equivCongr bc ef)) x✝¹) x✝ = ↑(↑(equivCongr (ab.trans bc) (de.trans ef)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
⊢ ↑(permCongr e) (Equiv.refl α') = Equiv.refl β'
[PROOFSTEP]
simp [permCongr_def]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
⊢ (↑(permCongr e) p).trans (↑(permCongr e) p') = ↑(permCongr e) (p.trans p')
[PROOFSTEP]
ext
[GOAL]
case H
α : Sort u
β : Sort v
γ : Sort w
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
x✝ : β'
⊢ ↑((↑(permCongr e) p).trans (↑(permCongr e) p')) x✝ = ↑(↑(permCongr e) (p.trans p')) x✝
[PROOFSTEP]
simp only [trans_apply, comp_apply, permCongr_apply, symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₁ → β₁
x : α₁
⊢ (fun f => ↑e₂.symm ∘ f ∘ ↑e₁) ((fun f => ↑e₂ ∘ f ∘ ↑e₁.symm) f) x = f x
[PROOFSTEP]
simp only [comp_apply, symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₂ → β₂
x : α₂
⊢ (fun f => ↑e₂ ∘ f ∘ ↑e₁.symm) ((fun f => ↑e₂.symm ∘ f ∘ ↑e₁) f) x = f x
[PROOFSTEP]
simp only [comp_apply, apply_symm_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
⊢ ↑(arrowCongr ea ec) (g ∘ f) = ↑(arrowCongr eb ec) g ∘ ↑(arrowCongr ea eb) f
[PROOFSTEP]
ext
[GOAL]
case h
α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ → β₁
g : β₁ → γ₁
x✝ : α₂
⊢ ↑(arrowCongr ea ec) (g ∘ f) x✝ = (↑(arrowCongr eb ec) g ∘ ↑(arrowCongr ea eb) f) x✝
[PROOFSTEP]
simp only [comp, arrowCongr_apply, eb.symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f₁ f₂ : α → α
⊢ ↑(conj e) (f₁ ∘ f₂) = ↑(conj e) f₁ ∘ ↑(conj e) f₂
[PROOFSTEP]
apply arrowCongr_comp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : Prop
⊢ (fun b => b = true) ((fun p => decide p) p) = p
[PROOFSTEP]
simp [@Bool.decide_iff p (Classical.propDecidable _)]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun p => decide p) ((fun b => b = true) b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
α : Sort u
β : Sort v
γ : Sort w
⊢ (fun p => decide p) ((fun b => b = true) false) = false
[PROOFSTEP]
simp
[GOAL]
case true
α : Sort u
β : Sort v
γ : Sort w
⊢ (fun p => decide p) ((fun b => b = true) true) = true
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β✝ : Sort v
γ : Sort w
β : α → Sort u_1
inst✝ : Subsingleton α
a : α
x✝ : (a' : α) → β a'
b : α
⊢ (fun x b => cast (_ : β a = β b) x) (eval a x✝) b = x✝ b
[PROOFSTEP]
rw [Subsingleton.elim b a]
[GOAL]
α : Sort u
β✝ : Sort v
γ : Sort w
β : α → Sort u_1
inst✝ : Subsingleton α
a : α
x✝ : (a' : α) → β a'
b : α
⊢ (fun x b => cast (_ : β a = β b) x) (eval a x✝) a = x✝ a
[PROOFSTEP]
rfl
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∃! x, p x) ↔ ∃! y, q y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∃! x, p x) → ∃! y, q y
[PROOFSTEP]
rintro ⟨a, ha₁, ha₂⟩
[GOAL]
case mp.intro.intro
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
a : α
ha₁ : p a
ha₂ : ∀ (y : α), (fun x => p x) y → y = a
⊢ ∃! y, q y
[PROOFSTEP]
exact ⟨f a, h.1 ha₁, fun b hb => f.symm_apply_eq.1 (ha₂ (f.symm b) (h.2 (by simpa using hb)))⟩
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
a : α
ha₁ : p a
ha₂ : ∀ (y : α), (fun x => p x) y → y = a
b : β
hb : (fun y => q y) b
⊢ q (↑f (↑f.symm b))
[PROOFSTEP]
simpa using hb
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∃! y, q y) → ∃! x, p x
[PROOFSTEP]
rintro ⟨b, hb₁, hb₂⟩
[GOAL]
case mpr.intro.intro
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
b : β
hb₁ : q b
hb₂ : ∀ (y : β), (fun y => q y) y → y = b
⊢ ∃! x, p x
[PROOFSTEP]
exact ⟨f.symm b, h.2 (by simpa using hb₁), fun y hy => (eq_symm_apply f).2 (hb₂ _ (h.1 hy))⟩
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
b : β
hb₁ : q b
hb₂ : ∀ (y : β), (fun y => q y) y → y = b
⊢ q (↑f (↑f.symm b))
[PROOFSTEP]
simpa using hb₁
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
f : α ≃ β
x✝ : α
⊢ p x✝ ↔ p (↑f.symm (↑f x✝))
[PROOFSTEP]
simp
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∀ (x : α), p x) ↔ ∀ (y : β), q y
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∀ (x : α), p x) → ∀ (y : β), q y
[PROOFSTEP]
intro h₂ x
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
⊢ (∀ (y : β), q y) → ∀ (x : α), p x
[PROOFSTEP]
intro h₂ x
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q x
[PROOFSTEP]
rw [← f.right_inv x]
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ q (toFun f (invFun f x))
[PROOFSTEP]
apply h.mp
[GOAL]
case mp
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (x : α), p x
x : β
⊢ p (invFun f x)
[PROOFSTEP]
apply h₂
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ p x
[PROOFSTEP]
apply h.mpr
[GOAL]
case mpr
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
f : α ≃ β
h : ∀ {x : α}, p x ↔ q (↑f x)
h₂ : ∀ (y : β), q y
x : α
⊢ q (↑f x)
[PROOFSTEP]
apply h₂
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
f : α ≃ β
⊢ ∀ {x : α}, p x ↔ p (↑f.symm (↑f x))
[PROOFSTEP]
simp
[GOAL]
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Sort u_1
β : Sort u_2
f : α ≃ β
p : α → Prop
x✝ : ∃ a, p a
a : α
h : p a
⊢ p (↑f.symm (↑f a))
[PROOFSTEP]
simpa using h
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
⊢ LeftInverse (Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂)))
    (Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂)))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
x✝ : Quot ra
a : α
⊢ Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂))
      (Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂)) (mk ra a)) =
    mk ra a
[PROOFSTEP]
simp only [Quot.map, Equiv.symm_apply_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
⊢ Function.RightInverse (Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂)))
    (Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂)))
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (↑e a₁) (↑e a₂)
x✝ : Quot rb
a : β
⊢ Quot.map ↑e (_ : ∀ (a₁ a₂ : α), ra a₁ a₂ → rb (↑e a₁) (↑e a₂))
      (Quot.map ↑e.symm (_ : ∀ (b₁ b₂ : β), rb b₁ b₂ → ra (↑e.symm b₁) (↑e.symm b₂)) (mk rb a)) =
    mk rb a
[PROOFSTEP]
simp only [Quot.map, Equiv.apply_symm_apply]
[GOAL]
α : Sort u
β : Sort v
γ : Sort w
r : α → α → Prop
e : α ≃ β
x✝¹ x✝ : α
⊢ r x✝¹ x✝ ↔ r (↑e.symm (↑e x✝¹)) (↑e.symm (↑e x✝))
[PROOFSTEP]
simp only [e.symm_apply_apply]


[GOAL]
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
q : Quot r
f : (a : α) → motive (mk r a)
⊢ motive q
[PROOFSTEP]
induction q using Quot.rec
[GOAL]
case f
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
f : (a : α) → motive (mk r a)
a✝ : α
⊢ motive (mk r a✝)
case h
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
q : Quot r
f : (a : α) → motive (mk r a)
a✝ b✝ : α
p✝ : r a✝ b✝
⊢ (_ : mk r a✝ = mk r b✝) ▸ ?m.408 a✝ = ?m.408 b✝
[PROOFSTEP]
apply f
[GOAL]
case h
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
h : ∀ (a : α), Subsingleton (motive (mk r a))
q : Quot r
f : (a : α) → motive (mk r a)
a✝ b✝ : α
p✝ : r a✝ b✝
⊢ (_ : mk r a✝ = mk r b✝) ▸ f a✝ = f b✝
[PROOFSTEP]
apply Subsingleton.elim


[GOAL]
m n : ℕ
⊢ (fun b => bif b then 1 else 0) (Matrix.vecCons false ![true] 0) = 0 ∧
    (fun b => bif b then 1 else 0) (Matrix.vecCons false ![true] 1) = 1
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
⊢ Matrix.vecCons false ![true] ((fun b => bif b then 1 else 0) false) = false ∧
    Matrix.vecCons false ![true] ((fun b => bif b then 1 else 0) true) = true
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
⊢ (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ (cons s (cons t finZeroElim))
[PROOFSTEP]
ext f
[GOAL]
case h
m n : ℕ
α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
f : (i : Fin 2) → α i
⊢ f ∈ (fun f => (f 0, f 1)) ⁻¹' s ×ˢ t ↔ f ∈ Set.pi Set.univ (cons s (cons t finZeroElim))
[PROOFSTEP]
simp [Fin.forall_fin_two]
[GOAL]
m n : ℕ
i x : Fin (n + 1)
⊢ (fun x => Option.casesOn' x i (Fin.succAbove i)) (Fin.insertNth i none some i) = i
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
i x : Fin (n + 1)
j : Fin n
⊢ (fun x => Option.casesOn' x i (Fin.succAbove i)) (Fin.insertNth i none some (Fin.succAbove i j)) = Fin.succAbove i j
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
i : Fin (n + 1)
x : Option (Fin n)
⊢ Fin.insertNth i none some ((fun x => Option.casesOn' x i (Fin.succAbove i)) x) = x
[PROOFSTEP]
cases x
[GOAL]
case none
m n : ℕ
i : Fin (n + 1)
⊢ Fin.insertNth i none some ((fun x => Option.casesOn' x i (Fin.succAbove i)) none) = none
[PROOFSTEP]
dsimp
[GOAL]
case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ Fin.insertNth i none some ((fun x => Option.casesOn' x i (Fin.succAbove i)) (some val✝)) = some val✝
[PROOFSTEP]
dsimp
[GOAL]
case none
m n : ℕ
i : Fin (n + 1)
⊢ Fin.insertNth i none some i = none
[PROOFSTEP]
simp
[GOAL]
case some
m n : ℕ
i : Fin (n + 1)
val✝ : Fin n
⊢ Fin.insertNth i none some (Fin.succAbove i val✝) = some val✝
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
i : Fin (n + 1)
⊢ ↑(finSuccEquiv' i) i = none
[PROOFSTEP]
simp [finSuccEquiv']
[GOAL]
m✝ n : ℕ
i : Fin (n + 1)
m : Fin n
h : Fin.castSucc m < i
⊢ ↑(finSuccEquiv' i) (Fin.castSucc m) = some m
[PROOFSTEP]
rw [← Fin.succAbove_below _ _ h, finSuccEquiv'_succAbove]
[GOAL]
m✝ n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ Fin.castSucc m
⊢ ↑(finSuccEquiv' i) (Fin.succ m) = some m
[PROOFSTEP]
rw [← Fin.succAbove_above _ _ h, finSuccEquiv'_succAbove]
[GOAL]
m n : ℕ
i : Fin n
⊢ ↑(finSuccEquiv' (Fin.last n)) (Fin.castSucc i) = some i
[PROOFSTEP]
rw [← Fin.succAbove_last, finSuccEquiv'_succAbove]
[GOAL]
m n : ℕ
i : Fin (n + 1)
h : i ≠ Fin.last n
⊢ ↑(finSuccEquiv' (Fin.last n)) i = some (Fin.castLT i (_ : ↑i < n))
[PROOFSTEP]
rcases Fin.exists_castSucc_eq.2 h with ⟨i, rfl⟩
[GOAL]
case intro
m n : ℕ
i : Fin n
h : Fin.castSucc i ≠ Fin.last n
⊢ ↑(finSuccEquiv' (Fin.last n)) (Fin.castSucc i) = some (Fin.castLT (Fin.castSucc i) (_ : ↑(Fin.castSucc i) < n))
[PROOFSTEP]
rw [finSuccEquiv'_last_apply_castSucc]
[GOAL]
case intro
m n : ℕ
i : Fin n
h : Fin.castSucc i ≠ Fin.last n
⊢ some i = some (Fin.castLT (Fin.castSucc i) (_ : ↑(Fin.castSucc i) < n))
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ ↑(finSuccEquiv' i) j = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) j)
[PROOFSTEP]
rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩
[GOAL]
case intro
m n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : Fin.succAbove i j ≠ i
⊢ ↑(finSuccEquiv' i) (Fin.succAbove i j) = some (Fin.predAbove (Fin.castLT i (_ : ↑i < n)) (Fin.succAbove i j))
[PROOFSTEP]
rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩
[GOAL]
case intro.intro
m n : ℕ
j i : Fin n
hi : Fin.castSucc i ≠ Fin.last n
hj : Fin.succAbove (Fin.castSucc i) j ≠ Fin.castSucc i
⊢ ↑(finSuccEquiv' (Fin.castSucc i)) (Fin.succAbove (Fin.castSucc i) j) =
    some (Fin.predAbove (Fin.castLT (Fin.castSucc i) (_ : ↑(Fin.castSucc i) < n)) (Fin.succAbove (Fin.castSucc i) j))
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
x : { x // x ≠ Fin.last n }
⊢ ↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x = Fin.castLT ↑x (_ : ↑↑x < n)
[PROOFSTEP]
rw [← Option.some_inj]
[GOAL]
m n : ℕ
x : { x // x ≠ Fin.last n }
⊢ some (↑(OrderIso.symm (finSuccAboveEquiv (Fin.last n))) x) = some (Fin.castLT ↑x (_ : ↑↑x < n))
[PROOFSTEP]
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_last_apply x.property
[GOAL]
m n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ ↑(OrderIso.symm (finSuccAboveEquiv p)) x = Fin.predAbove (Fin.castLT p (_ : ↑p < n)) ↑x
[PROOFSTEP]
rw [← Option.some_inj]
[GOAL]
m n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ some (↑(OrderIso.symm (finSuccAboveEquiv p)) x) = some (Fin.predAbove (Fin.castLT p (_ : ↑p < n)) ↑x)
[PROOFSTEP]
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property
[GOAL]
m n : ℕ
⊢ ↑finSuccEquivLast (Fin.last n) = none
[PROOFSTEP]
simp [finSuccEquivLast]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
i : Fin (n + 1)
f : (j : Fin (n + 1)) → α j
⊢ (fun f => Fin.insertNth i f.fst f.snd) ((fun f => (f i, fun j => f (Fin.succAbove i j))) f) = f
[PROOFSTEP]
simp [Fin.insertNth_eq_iff]
[GOAL]
m n : ℕ
α : Fin (n + 1) → Type u
i : Fin (n + 1)
f : α i × ((j : Fin n) → α (Fin.succAbove i j))
⊢ (fun f => (f i, fun j => f (Fin.succAbove i j))) ((fun f => Fin.insertNth i f.fst f.snd) f) = f
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
x : Fin m ⊕ Fin n
⊢ (fun i => Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) x) = x
[PROOFSTEP]
cases' x with y y
[GOAL]
case inl
m n : ℕ
y : Fin m
⊢ (fun i => Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inl y)) = Sum.inl y
[PROOFSTEP]
dsimp
[GOAL]
case inr
m n : ℕ
y : Fin n
⊢ (fun i => Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) (Sum.inr y)) = Sum.inr y
[PROOFSTEP]
dsimp
[GOAL]
case inl
m n : ℕ
y : Fin m
⊢ Fin.addCases Sum.inl Sum.inr (Fin.castAdd n y) = Sum.inl y
[PROOFSTEP]
simp
[GOAL]
case inr
m n : ℕ
y : Fin n
⊢ Fin.addCases Sum.inl Sum.inr (Fin.natAdd m y) = Sum.inr y
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
x : Fin (m + n)
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i => Fin.addCases Sum.inl Sum.inr i) x) = x
[PROOFSTEP]
refine' Fin.addCases (fun i => _) (fun i => _) x
[GOAL]
case refine'_1
m n : ℕ
x : Fin (m + n)
i : Fin m
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i => Fin.addCases Sum.inl Sum.inr i) (Fin.castAdd n i)) =
    Fin.castAdd n i
[PROOFSTEP]
simp
[GOAL]
case refine'_2
m n : ℕ
x : Fin (m + n)
i : Fin n
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i => Fin.addCases Sum.inl Sum.inr i) (Fin.natAdd m i)) = Fin.natAdd m i
[PROOFSTEP]
simp
[GOAL]
m n✝ : ℕ
k : Fin m
n : ℕ
⊢ ↑finAddFlip (Fin.castAdd n k) = Fin.natAdd n k
[PROOFSTEP]
simp [finAddFlip]
[GOAL]
m✝ n : ℕ
k : Fin n
m : ℕ
⊢ ↑finAddFlip (Fin.natAdd m k) = Fin.castAdd m k
[PROOFSTEP]
simp [finAddFlip]
[GOAL]
m n k : ℕ
h : k < m
hk : optParam (k < m + n) (_ : k < m + n)
hnk : optParam (n + k < n + m) (_ : n + k < n + m)
⊢ ↑finAddFlip { val := k, isLt := hk } = { val := n + k, isLt := hnk }
[PROOFSTEP]
convert finAddFlip_apply_castAdd ⟨k, h⟩ n
[GOAL]
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ ↑finAddFlip { val := k, isLt := h₂ } = { val := k - m, isLt := (_ : k - m < n + m) }
[PROOFSTEP]
convert @finAddFlip_apply_natAdd n ⟨k - m, (tsub_lt_iff_right h₁).2 ?_⟩ m
[GOAL]
case h.e'_2.h.e'_6.h.e'_2
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k = ↑(Fin.natAdd m { val := k - m, isLt := (_ : k - m < n) })
[PROOFSTEP]
simp [add_tsub_cancel_of_le h₁]
[GOAL]
m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k < n + m
[PROOFSTEP]
rwa [add_comm]
[GOAL]
m n k : ℕ
h : k < n
⊢ ↑(finRotate (n + 1)) { val := k, isLt := (_ : k < n + 1) } = { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ n) }
[PROOFSTEP]
ext
[GOAL]
case h
m n k : ℕ
h : k < n
⊢ ↑(↑(finRotate (n + 1)) { val := k, isLt := (_ : k < n + 1) }) =
    ↑{ val := k + 1, isLt := (_ : Nat.succ k < Nat.succ n) }
[PROOFSTEP]
dsimp [finRotate_succ]
[GOAL]
case h
m n k : ℕ
h : k < n
⊢ ↑(↑finAddFlip { val := k, isLt := (_ : k < n + 1) }) = k + 1
[PROOFSTEP]
simp [finAddFlip_apply_mk_left h, add_comm]
[GOAL]
m n : ℕ
⊢ ↑(finRotate (n + 1)) { val := n, isLt := (_ : n < n + 1) } = { val := 0, isLt := (_ : 0 < Nat.succ n) }
[PROOFSTEP]
dsimp [finRotate_succ]
[GOAL]
m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) (↑finAddFlip { val := n, isLt := (_ : n < n + 1) }) = 0
[PROOFSTEP]
rw [finAddFlip_apply_mk_right le_rfl]
[GOAL]
m n : ℕ
⊢ ↑(finCongr (_ : 1 + n = n + 1)) { val := n - n, isLt := (_ : n - n < 1 + n) } = 0
[PROOFSTEP]
simp
[GOAL]
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i => cons a v (↑(finRotate (n + 1)) i)
[PROOFSTEP]
ext ⟨i, h⟩
[GOAL]
case h.mk
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
by_cases h' : i < n
[GOAL]
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
[GOAL]
case pos
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ _root_.cast (_ : α = α) (v (castLT { val := i, isLt := h } h')) =
    cases a v { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }
[PROOFSTEP]
rfl
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
have h'' : n = i := by
  simp only [not_lt] at h'
  exact (Nat.eq_of_le_of_lt_succ h' h).symm
[GOAL]
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ n = i
[PROOFSTEP]
simp only [not_lt] at h'
[GOAL]
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : n ≤ i
⊢ n = i
[PROOFSTEP]
exact (Nat.eq_of_le_of_lt_succ h' h).symm
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
h'' : n = i
⊢ snoc v a { val := i, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := i, isLt := h })
[PROOFSTEP]
subst h''
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ snoc v a { val := n, isLt := h } = cons a v (↑(finRotate (n + 1)) { val := n, isLt := h })
[PROOFSTEP]
rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
[GOAL]
case neg
m n : ℕ
α : Type u_1
v : Fin n → α
a : α
h : n < n + 1
h' : ¬n < n
⊢ _root_.cast (_ : α = α) a = cases a v { val := 0, isLt := (_ : 0 < Nat.succ n) }
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
i : Fin (n + 1)
⊢ ↑(finRotate (n + 1)) i = i + 1
[PROOFSTEP]
cases n
[GOAL]
case zero
m : ℕ
i : Fin (Nat.zero + 1)
⊢ ↑(finRotate (Nat.zero + 1)) i = i + 1
[PROOFSTEP]
exact @Subsingleton.elim (Fin 1) _ _ _
[GOAL]
case succ
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
[PROOFSTEP]
rcases i.le_last.eq_or_lt with (rfl | h)
[GOAL]
case succ.inl
m n✝ : ℕ
⊢ ↑(finRotate (Nat.succ n✝ + 1)) (Fin.last (n✝ + 1)) = Fin.last (n✝ + 1) + 1
[PROOFSTEP]
simp [finRotate_last]
[GOAL]
case succ.inr
m n✝ : ℕ
i : Fin (Nat.succ n✝ + 1)
h : i < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) i = i + 1
[PROOFSTEP]
cases i
[GOAL]
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : { val := val✝, isLt := isLt✝ } < Fin.last (n✝ + 1)
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val, Fin.val_last, Fin.val_mk] at h
[GOAL]
case succ.inr.mk
m n✝ val✝ : ℕ
isLt✝ : val✝ < Nat.succ n✝ + 1
h : val✝ < n✝ + 1
⊢ ↑(finRotate (Nat.succ n✝ + 1)) { val := val✝, isLt := isLt✝ } = { val := val✝, isLt := isLt✝ } + 1
[PROOFSTEP]
simp [finRotate_of_lt h, Fin.eq_iff_veq, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]
[GOAL]
m n : ℕ
⊢ ↑(finRotate (Nat.succ n)) 0 = 1
[PROOFSTEP]
rw [finRotate_succ_apply, zero_add]
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
⊢ ↑(↑(finRotate (n + 1)) i) = ↑i + 1
[PROOFSTEP]
rw [finRotate_succ_apply]
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
⊢ ↑(i + 1) = ↑i + 1
[PROOFSTEP]
have : (i : ℕ) < n := Fin.val_lt_last h
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
h : i ≠ Fin.last n
this : ↑i < n
⊢ ↑(i + 1) = ↑i + 1
[PROOFSTEP]
exact Fin.val_add_one_of_lt this
[GOAL]
m n : ℕ
i : Fin (Nat.succ n)
⊢ ↑(↑(finRotate (Nat.succ n)) i) = if i = Fin.last n then 0 else ↑i + 1
[PROOFSTEP]
rw [finRotate_succ_apply, Fin.val_add_one i]
[GOAL]
m n : ℕ
x : Fin m × Fin n
⊢ ↑x.snd + n * ↑x.fst + 1 = ↑x.fst * n + ↑x.snd + 1
[PROOFSTEP]
ac_rfl
[GOAL]
m n : ℕ
x✝ : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
⊢ ↑y / n + ↑x = 0 + ↑x
[PROOFSTEP]
rw [Nat.div_eq_of_lt y.2]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (fun a => (a / n, ↑a)) ((fun p => p.fst * n + ↑p.snd) p) = p
[PROOFSTEP]
refine' Prod.ext _ (Fin.ext <| Nat.mul_add_mod_of_lt p.2.is_lt)
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ ((fun a => (a / n, ↑a)) ((fun p => p.fst * n + ↑p.snd) p)).fst = p.fst
[PROOFSTEP]
dsimp only
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (p.fst * n + ↑p.snd) / n = p.fst
[PROOFSTEP]
rw [add_comm, Nat.add_mul_div_right _ _ (NeZero.pos n), Nat.div_eq_of_lt p.2.is_lt, zero_add]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ (fun p => p.fst * ↑n + ↑↑p.snd) ((fun a => (a / ↑n, ↑(natMod a ↑n))) a) = a
[PROOFSTEP]
simp_rw [Fin.coe_ofNat_eq_mod, Int.coe_nat_mod, Int.natMod, Int.toNat_of_nonneg (Int.emod_nonneg _ <| NeZero.ne ↑n),
  Int.emod_emod, Int.ediv_add_emod']
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (fun a => (a / ↑n, ↑(natMod a ↑n))) ((fun p => p.fst * ↑n + ↑↑p.snd) (q, { val := r, isLt := hrn })) =
    (q, { val := r, isLt := hrn })
[PROOFSTEP]
simp only [Fin.val_mk, Prod.mk.inj_iff, Fin.ext_iff]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (q * ↑n + ↑r) / ↑n = q ∧ ↑↑(natMod (q * ↑n + ↑r) ↑n) = r
[PROOFSTEP]
obtain ⟨h1, h2⟩ := Int.coe_nat_nonneg r, Int.ofNat_lt.2 hrn
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ (q * ↑n + ↑r) / ↑n = q ∧ ↑↑(natMod (q * ↑n + ↑r) ↑n) = r
[PROOFSTEP]
rw [add_comm, Int.add_mul_ediv_right _ _ (NeZero.ne ↑n), Int.ediv_eq_zero_of_lt h1 h2, Int.natMod,
  Int.add_mul_emod_self, Int.emod_eq_of_lt h1 h2, Int.toNat_coe_nat]
[GOAL]
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ 0 + q = q ∧ ↑↑r = r
[PROOFSTEP]
exact ⟨zero_add q, Fin.val_cast_of_lt hrn⟩
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
i : Fin n
⊢ ↑(castLE h i) < n
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : Fin n
⊢ (fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) ((fun i => { val := castLE h i, property := (_ : ↑i < n) }) x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : { i // ↑i < n }
⊢ (fun i => { val := castLE h i, property := (_ : ↑i < n) }) ((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ n m : ℕ
h : n ≤ m
⊢ ∀ {a b : Fin n},
    ↑{ toFun := fun i => { val := castLE h i, property := (_ : ↑i < n) },
              invFun := fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) },
              left_inv := (_ : ∀ (x : Fin n), { val := ↑x, isLt := (_ : ↑x < n) } = x),
              right_inv :=
                (_ :
                  ∀ (x : { i // ↑i < n }),
                    { val := castLE h ((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x),
                        property := (_ : ↑((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x) < n) } =
                      x) }
          a ≤
        ↑{ toFun := fun i => { val := castLE h i, property := (_ : ↑i < n) },
              invFun := fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) },
              left_inv := (_ : ∀ (x : Fin n), { val := ↑x, isLt := (_ : ↑x < n) } = x),
              right_inv :=
                (_ :
                  ∀ (x : { i // ↑i < n }),
                    { val := castLE h ((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x),
                        property := (_ : ↑((fun i => { val := ↑↑i, isLt := (_ : ↑↑i < n) }) x) < n) } =
                      x) }
          b ↔
      a ≤ b
[PROOFSTEP]
simp [(strictMono_castLE h).le_iff_le]