awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
hI : I.IsProper
inl : ∀ (hI : IsProper.{u_1} (P := P) ⊤), ∃ (J : Ideal P), ⊤ ≤ J ∧ J.IsMaximal
inr : ∀ (J : Ideal P) (hJ : IsCoatom J) (hJ' : I ≤ J), ∃ (J : Ideal P), I ≤ J ∧ J.IsMaximal
⊢ ∃ (J : Ideal P), I ≤ J ∧ J.IsMaximal

Tactic:
rcases IsCoatomic.eq_top_or_exists_le_coatom I with rfl | ⟨J, hJ, hJ'⟩

Premises used: IsCoatomic.eq_top_or_exists_le_coatom, rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
hI : IsProper.{u_1} (P := P) ⊤
⊢ ∃ (J : Ideal P), ⊤ ≤ J ∧ J.IsMaximal

Tactic:
simp [isProper_iff_ne_top] at hI

Premises used: Order.Ideal.isProper_iff_ne_top
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
hI : I.IsProper
J : Ideal P
hJ : IsCoatom J
hJ' : I ≤ J
⊢ ∃ (J : Ideal P), I ≤ J ∧ J.IsMaximal

Tactic:
⟨J, hJ', isMaximal_iff_isCoatom.2 hJ⟩

Premises used: Iff.mpr, Order.Ideal.isMaximal_iff_isCoatom, And.intro, Exists.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
hI : I.IsProper
J : Ideal P
hJ : IsCoatom J
hJ' : I ≤ J
⊢ ∃ (J : Ideal P), I ≤ J ∧ J.IsMaximal

Tactic:
exact ⟨J, hJ', isMaximal_iff_isCoatom.2 hJ⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
rcases : ∀ (a : P) (ha : a ≠ ⊤), ∃ (I : Ideal P), I.IsMaximal
⊢ ∃ (I : Ideal P), I.IsMaximal

Tactic:
rcases exists_ne (⊤ : P) with ⟨a, ha⟩

Premises used: exists_ne, Top.top
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
a : P
ha : a ≠ ⊤
⊢ IsProper (principal a)

Tactic:
rw [← isProper_principal_iff] at ha

Premises used: Order.Ideal.isProper_principal_iff
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
a : P
ha : IsProper (principal a)
rcases : ∀ (I : Ideal P) (hI : I.IsMaximal), ∃ (I : Ideal P), I.IsMaximal
⊢ ∃ (I : Ideal P), I.IsMaximal

Tactic:
rcases ha.exists_le_maximal with ⟨I, -, hI⟩

Premises used: Order.Ideal.IsProper.exists_le_maximal
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
a : P
ha : IsProper (principal a)
I : Ideal P
hI : I.IsMaximal
⊢ ∃ (I : Ideal P), I.IsMaximal

Tactic:
⟨I, hI⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
inst_2 : Nontrivial P
a : P
ha : IsProper (principal a)
I : Ideal P
hI : I.IsMaximal
⊢ ∃ (I : Ideal P), I.IsMaximal

Tactic:
exact ⟨I, hI⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf :
  ∀ (a : α) (b : β),
    s b ((f : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
g : r ↪r s
hg :
  ∀ (a : α) (b : β),
    s b ((g : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) b
h :
  Eq (α := (a : α) → β)
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) f hf))
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) g hg))
e_toRelEmbedding : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ mk (r := r) (s := s) f hf = mk (r := r) (s := s) g hg

Tactic:
congr with x
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf :
  ∀ (a : α) (b : β),
    s b ((f : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
g : r ↪r s
hg :
  ∀ (a : α) (b : β),
    s b ((g : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) b
h :
  Eq (α := (a : α) → β)
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) f hf))
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) g hg))
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf :
  ∀ (a : α) (b : β),
    s b ((f : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b
g : r ↪r s
hg :
  ∀ (a : α) (b : β),
    s b ((g : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑g : (a : α) → β)) b
h :
  Eq (α := (a : α) → β)
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) f hf))
    ((fun (f : r ≼i s) ↦ f.toRelEmbedding (r := r) (s := s).toEmbedding (r := r) (s := s).toFun)
      (mk (r := r) (s := s) g hg))
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
exact congr_fun h x

Premises used: congr_fun
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f.toOrderEmbedding : (a : α) → β) x : β) ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ Eq (α := (a : α) → β) (⇑f.toOrderEmbedding : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f g : r ≼i s
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
⊢ Eq (α := (a : α) → β) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
b : β
⊢ s b ((f : (a : α) → β) a) → Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) b

Tactic:
f.mem_range_of_rel' _ _

Premises used: InitialSeg.mem_range_of_rel', Set.Mem
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
a b : α
f : r ≼i s
⊢ s ((f : (a : α) → β) a) ((f : (a : α) → β) b) ↔ r a b

Tactic:
f.map_rel_iff'

Premises used: InitialSeg.toRelEmbedding, RelEmbedding.map_rel_iff'
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ↔ a = b

Tactic:
f.toRelEmbedding.inj

Premises used: RelEmbedding.inj, InitialSeg.toRelEmbedding
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a : α
b : β
h : s b ((f : (a : α) → β) a)
rcases :
  ∀ (a' : α) (h : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)),
    ∃ (a'_1 : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a'_1 : β) ((f : (a : α) → β) a' : β) ∧ r a'_1 a
⊢ ∃ (a' : α), (f : (a : α) → β) a' = b ∧ r a' a

Tactic:
rcases f.mem_range_of_rel h with ⟨a', rfl⟩

Premises used: InitialSeg.mem_range_of_rel, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a a' : α
h : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)
⊢ ∃ (a'_1 : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a'_1 : β) ((f : (a : α) → β) a' : β) ∧ r a'_1 a

Tactic:
⟨a', rfl, f.map_rel_iff.1 h⟩

Premises used: InitialSeg.map_rel_iff, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≼i s
a a' : α
h : s ((f : (a : α) → β) a') ((f : (a : α) → β) a)
⊢ ∃ (a'_1 : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a'_1 : β) ((f : (a : α) → β) a' : β) ∧ r a'_1 a

Tactic:
exact ⟨a', rfl, f.map_rel_iff.1 h⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≃r s
⊢ ∀ (a : α) (b : β),
    s b ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a) →
      Membership.mem (γ := Set β)
        (Set.range.{u_2, u_1 + 1} (ι := α) (⇑(f.toRelEmbedding (r := r) (s := s)) : (a : α) → β)) b

Tactic:
simp
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h :
  t c
    ((f.toRelEmbedding (r := r) (s := s).trans (r := r) (s := s) (t := t) (g.toRelEmbedding (r := s) (s := t)) :
        (a : α) → γ)
      a)
simp :
  Membership.mem (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    c
⊢ Membership.mem (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (⇑(f.toRelEmbedding (r := r) (s := s).trans (r := r) (s := s) (t := t) (g.toRelEmbedding (r := s) (s := t))) :
        (a : α) → γ))
    c

Tactic:
simp only [RelEmbedding.coe_trans, coe_coe_fn, comp_apply] at h ⊢

Premises used: RelEmbedding.coe_trans, Function.comp_apply, InitialSeg.coe_coe_fn
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
c : γ
h : t c ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
rcases :
  ∀ (b : β)
    (h : t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b) ((g : (a : β) → γ) ((f : (a : α) → β) a : β))),
    Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
      (Set.range.{u_3, u_1 + 1} (ι := α)
        (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
      ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b : γ)
⊢ Membership.mem (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    c

Tactic:
rcases g.2 _ _ h with ⟨b, rfl⟩

Premises used: InitialSeg.mem_range_of_rel', rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h : t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b) ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
⊢ s b ((f : (a : α) → β) a)

Tactic:
have h := g.map_rel_iff.1 h
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h_1 : t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b) ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
h : s b ((f : (a : α) → β) a)
rcases :
  ∀ (a' : α)
    (h :
      t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β))
        ((g : (a : β) → γ) ((f : (a : α) → β) a : β)))
    (h : s ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a') ((f : (a : α) → β) a)),
    Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
      (Set.range.{u_3, u_1 + 1} (ι := α)
        (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
      ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β) :
        γ)
⊢ Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) b : γ)

Tactic:
rcases f.2 _ _ h with ⟨a', rfl⟩

Premises used: InitialSeg.mem_range_of_rel', rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a a' : α
h_1 :
  t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β))
    ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
h : s ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a') ((f : (a : α) → β) a)
⊢ Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β) : γ)

Tactic:
⟨a', rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a a' : α
h_1 :
  t ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β))
    ((g : (a : β) → γ) ((f : (a : α) → β) a : β))
h : s ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a') ((f : (a : α) → β) a)
⊢ Membership.mem.{u_3, u_3} (α := γ) (γ := Set γ)
    (Set.range.{u_3, u_1 + 1} (ι := α)
      (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)))
    ((g.toRelEmbedding (r := s) (s := t) : (a : β) → γ) ((f.toRelEmbedding (r := r) (s := s) : (a : α) → β) a' : β) : γ)

Tactic:
exact ⟨a', rfl⟩
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
r : α → α → Prop
x : α
⊢ (InitialSeg.refl r : (a : α) → α) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
⊢ Eq.{u_3 + 1} (α := γ) ((f.trans (r := r) (s := s) (t := t) g : (a : α) → γ) a : γ)
    ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
h : ∀ (a : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
IsWellFounded.induction r a fun b IH =>
      extensional_of_trichotomous_of_irrefl s fun x => ?_

Premises used: extensional_of_trichotomous_of_irrefl, IsWellFounded.induction
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
a : α
h :
  ∀ (b : α) (IH : ∀ (y : α), r y b → Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) y : β) ((g : (a : α) → β) y : β)) (x : β),
    s x ((f : (a : α) → β) b) ↔ s x ((g : (a : α) → β) b)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
refine IsWellFounded.induction r a fun b IH =>
      extensional_of_trichotomous_of_irrefl s fun x => ?_

Premises used: extensional_of_trichotomous_of_irrefl, IsWellFounded.induction
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) y : β) ((g : (a : α) → β) y : β)
x : β
h : (∃ (a' : α), (f : (a : α) → β) a' = x ∧ r a' b) ↔ ∃ (a' : α), (g : (a : α) → β) a' = x ∧ r a' b
⊢ s x ((f : (a : α) → β) b) ↔ s x ((g : (a : α) → β) b)

Tactic:
rw [f.exists_eq_iff_rel, g.exists_eq_iff_rel]

Premises used: InitialSeg.exists_eq_iff_rel
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) y : β) ((g : (a : α) → β) y : β)
x : β
⊢ (∃ (a' : α), (f : (a : α) → β) a' = x ∧ r a' b) ↔ ∃ (a' : α), (g : (a : α) → β) a' = x ∧ r a' b

Tactic:
exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl

Premises used: Iff.rfl, Eq.rec, and_congr_left, exists_congr
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : Std.Trichotomous s
inst_1 : Std.Irrefl s
inst_2 : IsWellFounded α r
f g : r ≼i s
a b : α
IH : ∀ (y : α), r y b → Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) y : β) ((g : (a : α) → β) y : β)
x : β
⊢ (∃ (a' : α), (f : (a : α) → β) a' = x ∧ r a' b) ↔ ∃ (a' : α), (g : (a : α) → β) a' = x ∧ r a' b

Tactic:
exact exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl

Premises used: and_congr_left, exists_congr
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst : IsWellOrder β s
⊢ Subsingleton (r ≼i s)

Tactic:
⟨fun a => have := a.isWellFounded; Subsingleton.elim a⟩

Premises used: Subsingleton.intro, InitialSeg.toRelEmbedding, RelEmbedding.isWellFounded, Subsingleton.elim
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f g : r ≼i s
a : α
rw rw₁ : Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)

Tactic:
rw [Subsingleton.elim f g]

Premises used: Subsingleton.elim
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
g : r ≃r s
a : α
⊢ Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
InitialSeg.eq g.toInitialSeg f a

Premises used: InitialSeg.eq, RelIso.toInitialSeg
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
g : s ≼i r
⊢ Eq (α := (a : α) → β) (⇑(f.antisymm (r := r) (s := s) g) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder α r
inst_1 : IsWellOrder β s
f : r ≼i s
g : s ≼i r
⊢ (f.antisymm (r := r) (s := s) g).symm (r := r) (s := s) = g.antisymm (r := s) (s := r) f

Tactic:
RelIso.coe_fn_injective rfl

Premises used: RelIso.coe_fn_injective, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
apply :
  (¬∃ (b : β),
        ∀ (x : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b) →
    Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β) ∨
    ∃ (b : β), ∀ (x : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b

Tactic:
apply or_iff_not_imp_right.2

Premises used: Iff.mpr, Classical.or_iff_not_imp_right
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
h : ¬∃ (b : β), ∀ (x : β), Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ↔ s x b
b : β
⊢ ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
apply : ∀ (x : β), (∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y) → ∃ (a : α), (f : (a : α) → β) a = x
⊢ ∃ (a : α), (f : (a : α) → β) a = b

Tactic:
apply IsWellFounded.induction s b

Premises used: IsWellFounded.induction
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y
inl :
  ∀ (y : β) (hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y) (hs : ¬s y x),
    ∃ (a : α), (f : (a : α) → β) a = x
inr :
  ∀ (y : β) (hy : y ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) (hs : s y x),
    ∃ (a : α), (f : (a : α) → β) a = x
⊢ ∃ (a : α), (f : (a : α) → β) a = x

Tactic:
obtain ⟨y, ⟨hy, hs⟩ | ⟨hy, hs⟩⟩ := h x
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y
y : β
hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y
hs : ¬s y x
inl :
  ∀ (IH : ∀ (y_1 : β), s y_1 y → ∃ (a : α), (f : (a : α) → β) a = y_1) (hs : ¬s y y), ∃ (a : α), (f : (a : α) → β) a = y
inl₁ : ∀ (h : s x y), ∃ (a : α), (f : (a : α) → β) a = x
⊢ ∃ (a : α), (f : (a : α) → β) a = x

Tactic:
obtain (rfl | h) := (trichotomous y x).resolve_left hs

Premises used: Or.resolve_left, trichotomous, rfl
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
y : β
hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y
IH : ∀ (y_1 : β), s y_1 y → ∃ (a : α), (f : (a : α) → β) a = y_1
hs : ¬s y y
⊢ ∃ (a : α), (f : (a : α) → β) a = y

Tactic:
hy

Premises used: Set.Mem, setOf, Set.range
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
y : β
hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y
IH : ∀ (y_1 : β), s y_1 y → ∃ (a : α), (f : (a : α) → β) a = y_1
hs : ¬s y y
⊢ ∃ (a : α), (f : (a : α) → β) a = y

Tactic:
exact hy
-- Module: Mathlib.Order.InitialSeg
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : IsWellOrder β s
f : r ≼i s
b : β
h_1 :
  ∀ (b : β),
    ∃ (x : β),
      Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) x ∧ ¬s x b ∨
        x ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ (a : α), (f : (a : α) → β) a = y
y : β
hy : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) y
hs : ¬s y x
h : s x y
inl : ∀ (z : α) (hs : ¬s ((f : (a : α) → β) z) x) (h : s x ((f : (a : α) → β) z)), ∃ (a : α), (f : (a : α) → β) a = x
⊢ ∃ (a : α), (f : (a : α) → β) a = x

Tactic:
obtain ⟨z, rfl⟩ := hy

Premises used: rfl