awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d

Tactic:
fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

Premises used: _private.0.Relation.comp_assoc.match_2, Relation.Comp, And.intro, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d

Tactic:
exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
h : ∀ (c : γ) (a : α), flip (r ∘r p) c a = (flip p ∘r flip r) c a
⊢ flip (r ∘r p) = flip p ∘r flip r

Tactic:
funext c a
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
h : flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a

Tactic:
apply propext

Premises used: propext
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
h : flip (r ∘r p) c a → (flip p ∘r flip r) c a
h₁ : (flip p ∘r flip r) c a → flip (r ∘r p) c a
⊢ flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a

Tactic:
constructor
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a

Tactic:
fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩

Premises used: _private.0.Relation.flip_comp.match_1, flip, Relation.Comp, And.intro, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a

Tactic:
exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Tactic:
fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩

Premises used: flip, Relation.Comp, And.intro, Exists.intro, _private.0.Relation.flip_comp.match_2
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Tactic:
exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)

Tactic:
?_
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
intro : ∀ (a : α), (∀ (y : α), rα y a → Acc rα y) → ∀ (ih : ∀ (y : α), rα y a → Acc rβ (f y)), Acc rβ (f a)
⊢ Acc rβ (f a)

Tactic:
induction ha with | intro a _ ih => ?_
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)

Tactic:
Acc.intro (f a) fun b hr ↦ ?_

Premises used: Acc.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
intro : ∀ (b : β) (hr : rβ b (f a)), Acc rβ b
⊢ Acc rβ (f a)

Tactic:
refine Acc.intro (f a) fun b hr ↦ ?_

Premises used: Acc.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
b : β
hr : rβ b (f a)
intro : ∀ (a' : α) (hr' : rα a' a) (hr : rβ (f a') (f a)), Acc rβ (f a')
⊢ Acc rβ b

Tactic:
obtain ⟨a', hr', rfl⟩ := fib hr

Premises used: rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
a' : α
hr' : rα a' a
hr : rβ (f a') (f a)
⊢ Acc rβ (f a')

Tactic:
ih a' hr'
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
a' : α
hr' : rα a' a
hr : rβ (f a') (f a)
⊢ Acc rβ (f a')

Tactic:
exact ih a' hr'
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
rβ : β → β → Prop
f : α → β
dc : ∀ {a : α} {b : β}, rβ b (f a) → ∃ (c : α), f c = b
a_1 : α
ha : Acc (InvImage rβ f) a_1
a : α
x : β
h : rβ x (f a)
a' : α
he : f a' = x
⊢ InvImage rβ f a' a

Tactic:
simp_all [InvImage]

Premises used: InvImage
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
r : α → β → Prop
f : α → γ
g : β → δ
c : γ
d : δ
⊢ Relation.Map r f g c d ↔ ∃ (a : α), ∃ (b : β), r a b ∧ f a = c ∧ g b = d

Tactic:
Iff.rfl

Premises used: Iff.rfl, Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → β → Prop
f₁ : α → γ
g₁ : β → δ
f₂ : γ → ε
g₂ : δ → ζ
⊢ Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

Tactic:
grind [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
f : α → γ
g : β → δ
hf : Injective f
hg : Injective g
r : α → β → Prop
a : α
b : β
⊢ Relation.Map r f g (f a) (g b) ↔ r a b

Tactic:
simp [Relation.Map, hf.eq_iff, hg.eq_iff]

Premises used: Function.Injective.eq_iff, Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (x : α) (x_1 : β), Relation.Map r id id x x_1 ↔ r x x_1
⊢ Relation.Map r id id = r

Tactic:
ext
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
x : α
x_1 : β
⊢ Relation.Map r id id x x_1 ↔ r x x_1

Tactic:
simp [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : Std.Refl r
f : α → β
hf : Surjective f
x : β
obtain : ∀ (y : α), Relation.Map r f f (f y) (f y)
⊢ Relation.Map r f f x x

Tactic:
obtain ⟨y, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : Std.Refl r
f : α → β
hf : Surjective f
y : α
⊢ Relation.Map r f f (f y) (f y)

Tactic:
⟨y, y, refl y, rfl, rfl⟩

Premises used: And.intro, Exists.intro, refl, rfl, Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : Std.Refl r
f : α → β
hf : Surjective f
y : α
⊢ Relation.Map r f f (f y) (f y)

Tactic:
exact ⟨y, y, refl y, rfl, rfl⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
x y : α
hxy : r x y
⊢ Relation.Map r f f (f y) (f x)

Tactic:
⟨_, _, hr hxy, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl, Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
hr : Symmetric r
f : α → β
x y : α
hxy : r x y
⊢ Relation.Map r f f (f y) (f x)

Tactic:
exact ⟨_, _, hr hxy, rfl, rfl⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
⊢ IsTrans β (Relation.Map r f f)

Tactic:
⟨fun _ _ _ ⟨x, y, hxy, hx, hy⟩ ⟨y', z, hyz, hy', hz⟩ ↦ ?_⟩

Premises used: IsTrans.mk, _private.0.IsTrans.map.match_1, Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
refine :
  ∀ (x x_1 x_2 : β),
    Relation.Map r f f x x_1 →
      Relation.Map r f f x_1 x_2 →
        ∀ (x_5 y : α) (hxy : r x_5 y) (hx : f x_5 = x) (hy : f y = x_1) (y' z : α) (hyz : r y' z) (hy' : f y' = x_1)
          (hz : f z = x_2), Relation.Map r f f x x_2
⊢ IsTrans β (Relation.Map r f f)

Tactic:
refine ⟨fun _ _ _ ⟨x, y, hxy, hx, hy⟩ ⟨y', z, hyz, hy', hz⟩ ↦ ?_⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
x_1 x_2 x_3 : β
h : Relation.Map r f f x_1 x_2
h_1 : Relation.Map r f f x_2 x_3
x y : α
hxy : r x y
hx : f x = x_1
hy : f y = x_2
y' z : α
hyz : r y' z
hy' : f y' = x_2
hz : f z = x_3
⊢ Relation.Map r f f x_1 x_3

Tactic:
⟨x, z, trans_of r hxy <| trans_of r (hf y y' <| hy' ▸ hy) hyz, hx, hz⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm, trans_of, Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : IsTrans α r
f : α → β
hf : ∀ (x y : α), f x = f y → r x y
x_1 x_2 x_3 : β
h : Relation.Map r f f x_1 x_2
h_1 : Relation.Map r f f x_2 x_3
x y : α
hxy : r x y
hx : f x = x_1
hy : f y = x_2
y' z : α
hyz : r y' z
hy' : f y' = x_2
hz : f z = x_3
⊢ Relation.Map r f f x_1 x_3

Tactic:
exact ⟨x, z, trans_of r hxy <| trans_of r (hf y y' <| hy' ▸ hy) hyz, hx, hz⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
r s : α → β → Prop
f : α → γ
g : β → δ
h : ∀ (x : α) (y : β), r x y → s x y
⊢ ∀ (x : γ) (y : δ), Relation.Map r f g x y → Relation.Map s f g x y

Tactic:
fun _ _ ⟨x, y, hxy, hx, hy⟩ => ⟨x, y, h _ _ hxy, hx, hy⟩

Premises used: _private.0.Relation.map_mono.match_1, And.intro, Exists.intro, Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
f : α → β
x : α
⊢ ∀ {y : α}, r x y → (Relation.Map r f f on f) x y

Tactic:
grind [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
f : α → β
hinj : Injective f
h : ∀ (x y : α), (Relation.Map r f f on f) x y ↔ r x y
⊢ Eq.{max 1 u_1} (Relation.Map r f f on f) r

Tactic:
ext x y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
f : α → β
hinj : Injective f
x y : α
⊢ (Relation.Map r f f on f) x y ↔ r x y

Tactic:
⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩

Premises used: _private.0.Relation.onFun_map_eq_of_injective.match_1, Eq.rec, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
f : α → β
hinj : Injective f
x y : α
⊢ (Relation.Map r f f on f) x y ↔ r x y

Tactic:
exact ⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
x : β
⊢ ∀ {y : β}, Relation.Map (r on f) f f x y → r x y

Tactic:
grind [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
h : ∀ (x y : β), Relation.Map (r on f) f f x y ↔ r x y
⊢ Eq.{max 1 u_2} (Relation.Map (r on f) f f) r

Tactic:
ext x y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
⊢ ∃ (a : α), f a = x

Tactic:
have _ := hsurj x
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
h : ∃ (a : α), f a = x
⊢ ∃ (a : α), f a = y

Tactic:
have _ := hsurj y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
h : ∃ (a : α), f a = x
h_1 : ∃ (a : α), f a = y
⊢ Relation.Map (r on f) f f x y ↔ r x y

Tactic:
grind [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
f : α → β
⊢ Eq.{max 1 u_2} (Relation.Map (Relation.Map r f f on f) f f) (Relation.Map r f f)

Tactic:
grind [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
⊢ Eq.{max 1 u_1} (Relation.Map (r on f) f f on f) (r on f)

Tactic:
grind [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
a₁ a₂ : α
⊢ Relation.Map (r on f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂)

Tactic:
grind [Relation.Map]

Premises used: Relation.Map
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

Tactic:
rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r p : α → α → Prop
hp : ∀ (a b : α), r a b → p a b
a : α
⊢ ReflGen p a a

Tactic:
rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a b c : α
⊢ Std.Refl (ReflGen r)

Tactic:
⟨@refl α r⟩

Premises used: Std.Refl.mk, Relation.ReflGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h' : Symmetric r
a b : α
⊢ ReflGen r a a

Tactic:
refl

Premises used: Relation.ReflGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h' : Symmetric r
a b : α
⊢ ReflGen r a a

Tactic:
exact refl

Premises used: Relation.ReflGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h' : Symmetric r
a b b_1 : α
h : r a b_1
⊢ ReflGen r b_1 a

Tactic:
single (h' h)

Premises used: Relation.ReflGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h' : Symmetric r
a b b_1 : α
h : r a b_1
⊢ ReflGen r b_1 a

Tactic:
exact single (h' h)

Premises used: Relation.ReflGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h' : Symmetric r
a b : α
h : ReflGen r a b
refl : ReflGen r a a
single : ∀ {b : α} (h : r a b), ReflGen r b a
⊢ ReflGen r b a

Tactic:
induction h with
  | refl => exact refl
  | single h => exact single (h' h)

Premises used: Relation.ReflGen.single, Relation.ReflGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b_1 c_1 : α
inst : IsTrans α r
a b c : α
h₁ : ReflGen r a b
h₂ : ReflGen r b c
refl : ReflGen r a b
single : ∀ (h₂ : r b c), ReflGen r a c
⊢ ReflGen r a c

Tactic:
obtain (rfl | h₂) := h₂

Premises used: rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b_1 c : α
inst : IsTrans α r
a b : α
h₁ : ReflGen r a b
⊢ ReflGen r a b

Tactic:
h₁
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b_1 c : α
inst : IsTrans α r
a b : α
h₁ : ReflGen r a b
⊢ ReflGen r a b

Tactic:
exact h₁
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b_1 c_1 : α
inst : IsTrans α r
a b c : α
h₁ : ReflGen r a b
h₂ : r b c
single : ∀ (h₂ : r a c), ReflGen r a c
single₁ : ∀ (h₁ : r a b), ReflGen r a c
⊢ ReflGen r a c

Tactic:
obtain (rfl | h₁) := h₁

Premises used: rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b c_1 : α
inst : IsTrans α r
a c : α
h₂ : r a c
⊢ ReflGen r a c

Tactic:
single h₂

Premises used: Relation.ReflGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b c_1 : α
inst : IsTrans α r
a c : α
h₂ : r a c
⊢ ReflGen r a c

Tactic:
exact single h₂

Premises used: Relation.ReflGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b_1 c_1 : α
inst : IsTrans α r
a b c : α
h₂ : r b c
h₁ : r a b
⊢ ReflGen r a c

Tactic:
single (trans_of r h₁ h₂)

Premises used: Relation.ReflGen.single, trans_of
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a_1 b_1 c_1 : α
inst : IsTrans α r
a b c : α
h₂ : r b c
h₁ : r a b
⊢ ReflGen r a c

Tactic:
exact single (trans_of r h₁ h₂)

Premises used: Relation.ReflGen.single, trans_of
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : r a b
⊢ SymmGen r a b

Tactic:
Or.inl h

Premises used: Or.inl, Relation.SymmGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : r b a
⊢ SymmGen r a b

Tactic:
Or.inr h

Premises used: Relation.SymmGen, Or.inr
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
hba : r b a
⊢ SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b

Tactic:
of_rel hba

Premises used: Relation.SymmGen.of_rel
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
hba : r b a
⊢ SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b

Tactic:
exact of_rel hba

Premises used: Relation.SymmGen.of_rel
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
hab : r a b
⊢ SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b

Tactic:
of_rel_symm hab

Premises used: Relation.SymmGen.of_rel_symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
hab : r a b
⊢ SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b

Tactic:
exact of_rel_symm hab

Premises used: Relation.SymmGen.of_rel_symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : SymmGen r b a
inl : ∀ (hba : r b a), SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
inr : ∀ (hab : r a b), SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
⊢ SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b

Tactic:
induction h with
  | inl hba => exact of_rel hba
  | inr hab => exact of_rel_symm hab
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ SymmGen r a a

Tactic:
.of_rel (_root_.refl _)

Premises used: Relation.SymmGen.of_rel, refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a : α
inst : Std.Refl r
⊢ SymmGen r a a

Tactic:
.refl ..

Premises used: Relation.SymmGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ SymmGen r a b → SymmGen r b a

Tactic:
Or.symm

Premises used: Or.symm, Relation.SymmGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Type u_7
inst : LE α
a b : α
h : a ≤ b
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
.of_rel h

Premises used: Relation.SymmGen.of_rel
-- Module: Mathlib.Logic.Relation
Goal:
α : Type u_7
inst : LE α
a b : α
h : b ≤ a
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b

Tactic:
.of_rel_symm h

Premises used: Relation.SymmGen.of_rel_symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
⊢ ReflTransGen r a b

Tactic:
assumption
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b_1 c_1 : α
h : ReflTransGen r b b_1
hcd : r b_1 c_1
hac : ReflTransGen r a b_1
⊢ ReflTransGen r a c_1

Tactic:
hac.tail hcd

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b_1 c_1 : α
h : ReflTransGen r b b_1
hcd : r b_1 c_1
hac : ReflTransGen r a b_1
⊢ ReflTransGen r a c_1

Tactic:
exact hac.tail hcd

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : ReflTransGen r b c
refl : ReflTransGen r a b
tail : ∀ {b_1 c : α}, ReflTransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : ReflTransGen r a b_1), ReflTransGen r a c
⊢ ReflTransGen r a c

Tactic:
induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
hab : r a b
⊢ ReflTransGen r a b

Tactic:
refl.tail hab

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
⊢ ReflTransGen r a b

Tactic:
refl.tail hab

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
⊢ ReflTransGen r a b

Tactic:
exact refl.tail hab

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
b_1 c_1 : α
h : ReflTransGen r b b_1
hcd : r b_1 c_1
hac : ReflTransGen r a b_1
⊢ ReflTransGen r a c_1

Tactic:
hac.tail hcd

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
b_1 c_1 : α
h : ReflTransGen r b b_1
hcd : r b_1 c_1
hac : ReflTransGen r a b_1
⊢ ReflTransGen r a c_1

Tactic:
exact hac.tail hcd

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : ReflTransGen r b c
refl : ReflTransGen r a b
tail : ∀ {b_1 c : α}, ReflTransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : ReflTransGen r a b_1), ReflTransGen r a c
⊢ ReflTransGen r a c

Tactic:
induction hbc with
  | refl => exact refl.tail hab
  | tail _ hcd hac => exact hac.tail hcd

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h : Symmetric r
x y : α
⊢ ReflTransGen r x x

Tactic:
rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h : Symmetric r
x y b_1 c_1 : α
h_1 : ReflTransGen r x b_1
b : r b_1 c_1
c : ReflTransGen r b_1 x
⊢ ReflTransGen r c_1 x

Tactic:
apply Relation.ReflTransGen.head (h b) c

Premises used: Relation.ReflTransGen.head
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h_1 : Symmetric r
x y : α
h : ReflTransGen r x y
refl : ReflTransGen r x x
tail : ∀ {b c : α}, ReflTransGen r x b → ∀ (b_1 : r b c) (c_1 : ReflTransGen r b x), ReflTransGen r c x
⊢ ReflTransGen r y x

Tactic:
induction h with
  | refl => rfl
  | tail _ b c => apply Relation.ReflTransGen.head (h b) c

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b → b = a ∨ ∃ (c : α), ReflTransGen r a c ∧ r c b

Tactic:
(cases_tail_iff r a b).1

Premises used: Relation.ReflTransGen.cases_tail_iff, Iff.mp
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b a : α
motive : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : motive a ⋯
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), motive c h → motive a_1 ⋯
⊢ motive a ⋯

Tactic:
refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b a : α
motive : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : motive a ⋯
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), motive c h → motive a_1 ⋯
⊢ motive a ⋯

Tactic:
exact refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop} (refl : motive b ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯
tail : motive b ⋯
tail₁ : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a ⋯
⊢ motive a ⋯

Tactic:
apply ih
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop} (refl : motive b ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ motive b ⋯

Tactic:
head hbc _ refl