awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Injective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Epi (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Z.toPresheafedSpace : TopCat) ⟶ (↑X.toPresheafedSpace : TopCat)
gc hc : X.presheaf ⟶ obj (pushforward C g) Z.presheaf
x : (↑(↑Z.toPresheafedSpace : TopCat) : Type v)
e :
  Eq (α := Z.toPresheafedSpace ⟶ Y.toPresheafedSpace) (InducedCategory.Hom.hom ({ hom := { base := g, c := gc } } ≫ f))
    (InducedCategory.Hom.hom ({ hom := { base := g, c := hc } } ≫ f))
⊢ Eq (α :=
    Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) g :
                (a : (↑(↑Z.toPresheafedSpace : TopCat) : Type v)) → (↑(↑X.toPresheafedSpace : TopCat) : Type v))
              x :
            (↑(↑X.toPresheafedSpace : TopCat) : Type v))) ⟶
      Z.presheaf.stalk x)
    (PresheafedSpace.Hom.stalkMap ({ base := g, c := gc : Z.Hom X.toPresheafedSpace } ≫ f.hom) x :
      Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier) (X :=
                (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base ({ base := g, c := gc : Z.Hom X.toPresheafedSpace } ≫ f.hom)) :
              (a : (↑(↑Z.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            x) ⟶
        Z.presheaf.stalk x)
    (PresheafedSpace.Hom.stalkMap ({ base := g, c := hc : Z.Hom X.toPresheafedSpace } ≫ f.hom) x)

Tactic:
congr 1
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
left_cancellation : ∀ {Z : SheafedSpace.{u, v, v} C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
⊢ Epi f

Tactic:
constructor
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
left_cancellation :
  ∀ (g : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat))
    (gc : Z.presheaf ⟶ obj (pushforward C g) Y.presheaf) (h : Y ⟶ Z),
    f ≫ { hom := { base := g, c := gc } } = f ≫ h → { hom := { base := g, c := gc } } = h
⊢ ∀ (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

Tactic:
⟨g, gc⟩
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)
gc : Z.presheaf ⟶ obj (pushforward C g) Y.presheaf
left_cancellation :
  ∀ (h : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat))
    (hc : Z.presheaf ⟶ obj (pushforward C h) Y.presheaf),
    Eq (α := X ⟶ Z) (f ≫ { hom := { base := g, c := gc } }) (f ≫ { hom := { base := h, c := hc } }) →
      Eq.{v + 1} (α := Y ⟶ Z) { hom := { base := g, c := gc } } { hom := { base := h, c := hc } }
⊢ ∀ (h : Y ⟶ Z), f ≫ { hom := { base := g, c := gc } } = f ≫ h → { hom := { base := g, c := gc } } = h

Tactic:
⟨h, hc⟩
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)
gc : Z.presheaf ⟶ obj (pushforward C g) Y.presheaf
h : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)
hc : Z.presheaf ⟶ obj (pushforward C h) Y.presheaf
e : Eq (α := X ⟶ Z) (f ≫ { hom := { base := g, c := gc } }) (f ≫ { hom := { base := h, c := hc } })
⊢ Eq (α := X.toPresheafedSpace ⟶ Z.toPresheafedSpace) (InducedCategory.Hom.hom (f ≫ { hom := { base := g, c := gc } }))
    (InducedCategory.Hom.hom (f ≫ { hom := { base := h, c := hc } }))

Tactic:
apply_fun InducedCategory.Hom.hom at e

Premises used: CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
h₁ :
  Function.Surjective (α := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (β :=
    (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
h₂ :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Mono (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace.{u, v, v} C
g : (↑Y.toPresheafedSpace : TopCat) ⟶ (↑Z.toPresheafedSpace : TopCat)
gc hc : Z.presheaf ⟶ obj (pushforward C g) Y.presheaf
e :
  Eq (α := X.toPresheafedSpace ⟶ Z.toPresheafedSpace) (InducedCategory.Hom.hom (f ≫ { hom := { base := g, c := gc } }))
    (InducedCategory.Hom.hom (f ≫ { hom := { base := g, c := hc } }))
⊢ Eq.{v + 1} (α := Y ⟶ Z) { hom := { base := g, c := gc } } { hom := { base := g, c := hc } }

Tactic:
SheafedSpace.hom_stalk_ext ⟨g, gc⟩ ⟨g, hc⟩ rfl fun y ↦ ?_

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.mk, AlgebraicGeometry.SheafedSpace.hom_stalk_ext, CategoryTheory.InducedCategory.Hom.mk, rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
m : G
x : ι ↪ α
h :
  ∀ (x_1 : ι),
    Eq.{u_4 + 1} (α := β) (({ toFun := f.toFun ∘ (m • x).toFun, inj' := ⋯ : ι ↪ β } : (a : ι) → β) x_1 : β)
      ((σ m • { toFun := f.toFun ∘ x.toFun, inj' := ⋯ : ι ↪ β } : (a : ι) → β) x_1 : β)
⊢ { toFun := f.toFun ∘ (m • x).toFun, inj' := ⋯ : ι ↪ β } = σ m • { toFun := f.toFun ∘ x.toFun, inj' := ⋯ : ι ↪ β }

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
m : G
x : ι ↪ α
x_1 : ι
⊢ Eq.{u_4 + 1} (α := β) (({ toFun := f.toFun ∘ (m • x).toFun, inj' := ⋯ : ι ↪ β } : (a : ι) → β) x_1 : β)
    ((σ m • { toFun := f.toFun ∘ x.toFun, inj' := ⋯ : ι ↪ β } : (a : ι) → β) x_1 : β)

Tactic:
simp [f.map_smul']

Premises used: MulActionHom.map_smul'
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
x : ι ↪ α
i : ι
⊢ Eq.{u_4 + 1} (α := β) ((((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) x : ι ↪ β) : (a : ι) → β) i : β)
    ((f : (a : α) → β) ((x : (a : ι) → α) i : α) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a₁ : ι ↪ α
_ :
  ∀ ⦃a₂ : ι ↪ α⦄,
    Eq (α := ι ↪ β) ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₁ : ι ↪ β)
        ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₂ : ι ↪ β) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : ι ↪ α⦄,
    Eq (α := ι ↪ β) ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₁ : ι ↪ β)
        ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₂ : ι ↪ β) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a₁ a₂ : ι ↪ α
hxy :
  Eq (α := ι ↪ β) ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₁ : ι ↪ β)
    ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₂ : ι ↪ β)
h : ∀ (x : ι), Eq.{u_2 + 1} (α := α) ((a₁ : (a : ι) → α) x : α) ((a₂ : (a : ι) → α) x : α)
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a₁ a₂ : ι ↪ α
hxy :
  Eq (α := ι ↪ β) ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₁ : ι ↪ β)
    ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₂ : ι ↪ β)
x : ι
h :
  Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) ((a₁ : (a : ι) → α) x : α) : β)
    ((f : (a : α) → β) ((a₂ : (a : ι) → α) x : α) : β)
⊢ Eq.{u_2 + 1} (α := α) ((a₁ : (a : ι) → α) x : α) ((a₂ : (a : ι) → α) x : α)

Tactic:
apply hf
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Injective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
a₁ a₂ : ι ↪ α
hxy :
  Eq (α := ι ↪ β) ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₁ : ι ↪ β)
    ((mulActionHom_embedding ι hf : (a : ι ↪ α) → ι ↪ β) a₂ : ι ↪ β)
x : ι
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) ((a₁ : (a : ι) → α) x : α) : β)
    ((f : (a : α) → β) ((a₂ : (a : ι) → α) x : α) : β)

Tactic:
simp only [← hf.mulActionHom_embedding_apply, hxy]

Premises used: Function.Injective.mulActionHom_embedding_apply
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Bijective (α := ι ↪ α) (β := ι ↪ β) (⇑(Injective.mulActionHom_embedding ι ⋯) : (a : ι ↪ α) → ι ↪ β)

Tactic:
⟨hf.injective.mulActionHom_embedding_isInjective, ?_⟩

Premises used: Function.Injective.mulActionHom_embedding_isInjective, Function.Bijective.injective, And.intro, Function.Bijective
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
refine : Surjective (α := ι ↪ α) (β := ι ↪ β) (⇑(Injective.mulActionHom_embedding ι ⋯) : (a : ι ↪ α) → ι ↪ β)
⊢ Bijective (α := ι ↪ α) (β := ι ↪ β) (⇑(Injective.mulActionHom_embedding ι ⋯) : (a : ι ↪ α) → ι ↪ β)

Tactic:
refine ⟨hf.injective.mulActionHom_embedding_isInjective, ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
obtain :
  ∀ (g : β → α),
    LeftInverse g (⇑f : (a : α) → β) →
      ∀ (hfg : RightInverse g (⇑f : (a : α) → β)),
        ∃ (a : ι ↪ α), (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) a = y
⊢ ∃ (a : ι ↪ α), (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) a = y

Tactic:
obtain ⟨g, _, hfg⟩ := Function.bijective_iff_has_inverse.mp hf

Premises used: Function.bijective_iff_has_inverse, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
h : (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := ⋯ } = y
⊢ ∃ (a : ι ↪ α), (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) a = y

Tactic:
use ⟨g ∘ y, hfg.injective.comp (EmbeddingLike.injective y)⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
h :
  ∀ (x : ι),
    Eq.{u_4 + 1} (α := β)
      ((((Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := ⋯ } :
              ι ↪ β) :
            (a : ι) → β)
          x :
        β)
      ((y : (a : ι) → β) x : β)
⊢ (Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := ⋯ } = y

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
x : ι
h : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (g ((y : (a : ι) → β) x)) : β) ((y : (a : ι) → β) x : β)
⊢ Eq.{u_4 + 1} (α := β)
    ((((Injective.mulActionHom_embedding ι ⋯ : (a : ι ↪ α) → ι ↪ β) { toFun := g ∘ (⇑y : (a : ι) → β), inj' := ⋯ } :
            ι ↪ β) :
          (a : ι) → β)
        x :
      β)
    ((y : (a : ι) → β) x : β)

Tactic:
simp only [hf.injective.mulActionHom_embedding_apply, coeFn_mk, comp_apply]

Premises used: Function.Injective.mulActionHom_embedding_apply, Function.Bijective.injective, Function.Embedding.coeFn_mk, Function.comp_apply
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
x : ι
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (g ((y : (a : ι) → β) x)) : β) ((y : (a : ι) → β) x : β)

Tactic:
hfg (y _)

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
ι : Type u_5
hf : Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
y : ι ↪ β
g : β → α
left : LeftInverse g (⇑f : (a : α) → β)
hfg : RightInverse g (⇑f : (a : α) → β)
x : ι
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (g ((y : (a : ι) → β) x)) : β) ((y : (a : ι) → β) x : β)

Tactic:
exact hfg (y _)

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
n : ℕ
⊢ IsMultiplyPretransitive G α n ↔ ∀ (x y : Fin n ↪ α), ∃ (g : G), g • x = y

Tactic:
isPretransitive_iff _ _

Premises used: MulAction.isPretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x_1 y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
x : n ↪ β
i : n
simp :
  f.toFun ((Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf : (a : β) → α) ((x : (a : n) → β) i : β)) =
    (x : (a : n) → β) i
⊢ f.toFun ((aux x : (a : n) → α) i) = (x : (a : n) → β) i

Tactic:
simp only [trans_apply, aux]

Premises used: Function.Embedding.trans_apply
-- Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H : Type u_3
β : Type u_4
inst_2 : Group H
inst_3 : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
inst_4 : IsPretransitive G (n ↪ α)
x_1 y : n ↪ β
aux : (x : n ↪ β) → n ↪ α := fun (x : n ↪ β) ↦ x.trans (Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf)
x : n ↪ β
i : n
⊢ f.toFun ((Function.Embedding.ofSurjective (⇑f : (a : α) → β) hf : (a : β) → α) ((x : (a : n) → β) i : β)) =
    (x : (a : n) → β) i

Tactic:
apply Function.surjInv_eq

Premises used: Function.surjInv_eq