awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (hypothesis)
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ (y : α), y ≠ x
have h₁ : x ≠ y'
Tactic: rw [← hx] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
⊢ Nontrivial β
have obtain : ∀ (f g : α → β) (h : f ≠ g), Nontrivial β
Tactic: obtain ⟨f, g, h⟩ := exists_pair_ne (α → β)
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
f g : α → β
h : f ≠ g
⊢ Nontrivial β
have h₁ : ∃ (x : α), ¬f x = g x
Tactic: rw [ne_eq, funext_iff, Classical.not_forall] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
f g : α → β
h : ∃ (x : α), ¬f x = g x
⊢ Nontrivial β
have obtain : ∀ (a : α) (h : ¬f a = g a), Nontrivial β
Tactic: obtain ⟨a, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
⊢ ¬Subsingleton α ↔ Nontrivial α
have rw : ¬¬Nontrivial α ↔ Nontrivial α
Tactic: rw [← not_nontrivial_iff_subsingleton, Classical.not_not]
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
rw : ¬¬Nontrivial α ↔ Nontrivial α
⊢ ¬Subsingleton α ↔ Nontrivial α
have rw₁ : Nontrivial α ↔ Nontrivial α
Tactic: rw [← not_nontrivial_iff_subsingleton, Classical.not_not]
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_3
⊢ Subsingleton α ∨ Nontrivial α
have rw : Nontrivial α ∨ ¬Nontrivial α
Tactic: rw [← not_nontrivial_iff_subsingleton, or_comm]
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
⊢ Nontrivial α
have rcases : ∀ (x y : β) (h : x ≠ y), Nontrivial α
Tactic: rcases exists_pair_ne β with ⟨x, y, h⟩
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α
have rcases : ∀ (x' : α) (hx' : f x' = x), Nontrivial α
Tactic: rcases hf x with ⟨x', hx'⟩
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α
have rcases : ∀ (y' : α) (hy' : f y' = y), Nontrivial α
Tactic: rcases hf y with ⟨y', hy'⟩
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ x' ≠ y'
have refine : ∀ (H : x' = y'), x = y
Tactic: refine fun H ↦ h ?_
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y
have rw : f x' = y
Tactic: rw [← hx', ← hy', H]
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
rw : f x' = y
⊢ x = y
have rw₁ : f x' = f y'
Tactic: rw [← hx', ← hy', H]
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
rw : f x' = y
rw₁ : f x' = f y'
⊢ x = y
have rw₂ : f y' = f y'
Tactic: rw [← hx', ← hy', H]
-- Lean 4 proof step from Mathlib.Logic.Nontrivial.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α
have this : x' ≠ y'
Tactic: have : x' ≠ y' := by
    refine fun H ↦ h ?_
    rw [← hx', ← hy', H]
-- Lean 4 proof step from Mathlib.Logic.OpClass (goal)
Goal:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f a (f b c) = f b (f a c)
have rw : f (f a b) c = f b (f a c)
Tactic: rw [← ha.assoc, hc.comm a, ha.assoc]
-- Lean 4 proof step from Mathlib.Logic.OpClass (goal)
Goal:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
rw : f (f a b) c = f b (f a c)
⊢ f a (f b c) = f b (f a c)
have rw₁ : f (f b a) c = f b (f a c)
Tactic: rw [← ha.assoc, hc.comm a, ha.assoc]
-- Lean 4 proof step from Mathlib.Logic.OpClass (goal)
Goal:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
rw : f (f a b) c = f b (f a c)
rw₁ : f (f b a) c = f b (f a c)
⊢ f a (f b c) = f b (f a c)
have rw₂ : f b (f a c) = f b (f a c)
Tactic: rw [← ha.assoc, hc.comm a, ha.assoc]
-- Lean 4 proof step from Mathlib.Logic.OpClass (goal)
Goal:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
⊢ f (f a b) c = f (f a c) b
have rw : f a (f b c) = f (f a c) b
Tactic: rw [ha.assoc, hc.comm b, ha.assoc]
-- Lean 4 proof step from Mathlib.Logic.OpClass (goal)
Goal:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
rw : f a (f b c) = f (f a c) b
⊢ f (f a b) c = f (f a c) b
have rw₁ : f a (f c b) = f (f a c) b
Tactic: rw [ha.assoc, hc.comm b, ha.assoc]
-- Lean 4 proof step from Mathlib.Logic.OpClass (goal)
Goal:
α : Sort u
β : Sort v
f : α → α → α
hc : Std.Commutative f
ha : Std.Associative f
a b c : α
rw : f a (f b c) = f (f a c) b
rw₁ : f a (f c b) = f (f a c) b
⊢ f (f a b) c = f (f a c) b
have rw₂ : f a (f c b) = f a (f c b)
Tactic: rw [ha.assoc, hc.comm b, ha.assoc]
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
f : γ → β
⊢ Eq (α := (a : α) → (c : γ) → Prop) (r ∘r fun (x1 : β) (x2 : γ) ↦ x1 = f x2) fun (x1 : α) (x2 : γ) ↦ r x1 (f x2)
have h : ∀ (x : α) (y : γ), (r ∘r fun (x1 : β) (x2 : γ) ↦ x1 = f x2) x y ↔ r x (f y)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
f : γ → α
⊢ Eq (α := (a : γ) → (c : β) → Prop) ((fun (x1 : γ) (x2 : α) ↦ f x1 = x2) ∘r r) fun (x : γ) ↦ r (f x)
have h : ∀ (x : γ) (y : β), ((fun (x1 : γ) (x2 : α) ↦ f x1 = x2) ∘r r) x y ↔ r (f x) y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q
have h : ∀ (a : α) (d : δ), ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d
Tactic: funext a d
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
have h : ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d
Tactic: apply propext
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
have h : ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
h : ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d
⊢ ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d
have h₁ : (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
p : β → γ → Prop
⊢ flip (r ∘r p) = flip p ∘r flip r
have h : ∀ (c : γ) (a : α), flip (r ∘r p) c a = (flip p ∘r flip r) c a
Tactic: funext c a
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
have h : flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a
Tactic: apply propext
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
have h : flip (r ∘r p) c a → (flip p ∘r flip r) c a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
have h₁ : (flip p ∘r flip r) c a → flip (r ∘r p) c a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
⊢ Acc rβ (f a)
have intro : ∀ (a : α), (∀ (y : α), rα y a → Acc rα y) → ∀ (ih : ∀ (y : α), rα y a → Acc rβ (f y)), Acc rβ (f a)
Tactic: induction ha with | intro a _ ih => ?_
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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)
have intro : ∀ (b : β) (hr : rβ b (f a)), Acc rβ b
Tactic: refine Acc.intro (f a) fun b hr ↦ ?_
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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)
⊢ Acc rβ b
have intro : ∀ (a' : α) (hr' : rα a' a) (hr : rβ (f a') (f a)), Acc rβ (f a')
Tactic: obtain ⟨a', hr', rfl⟩ := fib hr
Cleared hypotheses: b, hr
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ Relation.Map r id id = r
have h : ∀ (x : α) (x_1 : β), Relation.Map r id id x x_1 ↔ r x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
inst : Std.Refl r
f : α → β
hf : Surjective f
x : β
⊢ Relation.Map r f f x x
have obtain : ∀ (y : α), Relation.Map r f f (f y) (f y)
Tactic: obtain ⟨y, rfl⟩ := hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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)
have 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
Tactic: refine ⟨fun _ _ _ ⟨x, y, hxy, hx, hy⟩ ⟨y', z, hyz, hy', hz⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
f : α → β
hinj : Injective f
⊢ Eq.{max 1 u_1} (Relation.Map r f f on f) r
have h : ∀ (x y : α), (Relation.Map r f f on f) x y ↔ r x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
⊢ Eq.{max 1 u_2} (Relation.Map (r on f) f f) r
have h : ∀ (x y : β), Relation.Map (r on f) f f x y ↔ r x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Logic.Relation (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
⊢ Relation.Map (r on f) f f x y ↔ r x y
have x₁ : ∃ (a : α), f a = x
Tactic: have _ := hsurj x
-- Lean 4 proof step from Mathlib.Logic.Relation (hypothesis)
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
f : α → β
hsurj : Surjective f
x y : β
h : ∃ (a : α), f a = x
⊢ Relation.Map (r on f) f f x y ↔ r x y
have x₁ : ∃ (a : α), f a = y
Tactic: have _ := hsurj y
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
h' : Symmetric r
a b : α
h : ReflGen r a b
⊢ ReflGen r b a
have refl : ReflGen r a a
Tactic: induction h with
  | refl => exact refl
  | single h => exact single (h' h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
h' : Symmetric r
a b : α
h : ReflGen r a b
refl : ReflGen r a a
⊢ ReflGen r b a
have single : ∀ {b : α} (h : r a b), ReflGen r b a
Tactic: induction h with
  | refl => exact refl
  | single h => exact single (h' h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
⊢ ReflGen r a c
have single : ∀ (h₂ : r b c), ReflGen r a c
Tactic: obtain (rfl | h₂) := h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
⊢ ReflGen r a c
have single : ∀ (h₂ : r a c), ReflGen r a c
Tactic: obtain (rfl | h₁) := h₁
Cleared hypotheses: b, h₁, h₂
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
⊢ ReflGen r a c
have single₁ : ∀ (h₁ : r a b), ReflGen r a c
Tactic: obtain (rfl | h₁) := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : SymmGen r b a
⊢ SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
have inl : ∀ (hba : r b a), 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
⊢ SymmGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
have inr : ∀ (hab : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : ReflTransGen r b c
refl : ReflTransGen r a b
⊢ ReflTransGen r a c
have tail : ∀ {b_1 c : α}, ReflTransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : ReflTransGen r a b_1), ReflTransGen r a c
Tactic: induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c
have refl : ReflTransGen r a b
Tactic: induction hbc with
  | refl => exact refl.tail hab
  | tail _ hcd hac => exact hac.tail hcd
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : ReflTransGen r b c
refl : ReflTransGen r a b
⊢ ReflTransGen r a c
have tail : ∀ {b_1 c : α}, ReflTransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : ReflTransGen r a b_1), ReflTransGen r a c
Tactic: induction hbc with
  | refl => exact refl.tail hab
  | tail _ hcd hac => exact hac.tail hcd
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
h_1 : Symmetric r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x
have refl : ReflTransGen r x x
Tactic: induction h with
  | refl => rfl
  | tail _ b c => apply Relation.ReflTransGen.head (h b) c
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
h_1 : Symmetric r
x y : α
h : ReflTransGen r x y
refl : ReflTransGen r x x
⊢ ReflTransGen r y x
have tail : ∀ {b c : α}, ReflTransGen r x b → ∀ (b_1 : r b c) (c_1 : ReflTransGen r b x), ReflTransGen r c x
Tactic: induction h with
  | refl => rfl
  | tail _ b c => apply Relation.ReflTransGen.head (h b) c
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 a ⋯
have tail : motive b sorry
Tactic: apply ih
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 ⋯
⊢ motive a ⋯
have tail₁ : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 sorry → motive a sorry
Tactic: apply ih
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
b : α
motive : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : motive b ⋯
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯
⊢ motive a h
have refl₁ : ∀ {motive : (a_1 : α) → ReflTransGen r a_1 a → Prop} (refl : motive a sorry)
  (head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), motive c h → motive a_1 sorry), motive a sorry
Tactic: induction h with
  | refl => exact refl
  | @tail b c _ hbc ih =>
  apply ih
  · exact head hbc _ refl
  · exact fun h1 h2 ↦ head h1 (h2.tail hbc)
Cleared hypotheses: motive, h, refl, head
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
b : α
motive : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : motive b ⋯
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯
refl₁ :
  ∀ {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 ⋯
⊢ motive a h
have tail : ∀ {b c : α} (a_1 : ReflTransGen r a b) (hbc : r b c)
  (ih :
    ∀ {motive : (a : α) → ReflTransGen r a b → Prop} (refl : motive b sorry)
      (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a sorry), motive a a_1)
  {motive : (a : α) → ReflTransGen r a c → Prop} (refl : motive c sorry)
  (head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a sorry), motive a sorry
Tactic: induction h with
  | refl => exact refl
  | @tail b c _ hbc ih =>
  apply ih
  · exact head hbc _ refl
  · exact fun h1 h2 ↦ head h1 (h2.tail hbc)
Cleared hypotheses: motive, h, refl, head
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
refl : ∀ (a : α), motive (a := a) ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive h
have refl₁ : motive (a := a) sorry
Tactic: induction h with
  | refl => exact refl a
  | tail hab hbc ih => exact trans hab (.single hbc) ih (single hbc)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
refl : ∀ (a : α), motive (a := a) ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
refl₁ : motive (a := a) ⋯
⊢ motive h
have tail : ∀ {b c : α} (hab : ReflTransGen r a b) (hbc : r b c) (ih : motive hab), motive sorry
Tactic: induction h with
  | refl => exact refl a
  | tail hab hbc ih => exact trans hab (.single hbc) ih (single hbc)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b
have refl : b = b ∨ ∃ (c : α), r b c ∧ ReflTransGen r c b
Tactic: induction h using Relation.ReflTransGen.head_induction_on
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
refl : b = b ∨ ∃ (c : α), r b c ∧ ReflTransGen r c b
⊢ a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b
have head : ∀ {a c : α},
  r a c →
    ReflTransGen r c b →
      (c = b ∨ ∃ (c_1 : α), r c c_1 ∧ ReflTransGen r c_1 b) → a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b
Tactic: induction h using Relation.ReflTransGen.head_induction_on
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b
have mpr : (a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
Tactic: use cases_head
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c ∨ ReflTransGen r c b_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
have tail : ∀ (IH : ReflTransGen r b_1 c), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
Tactic: rcases IH with (IH | IH)
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c ∨ ReflTransGen r c b_1
tail : ∀ (IH : ReflTransGen r b_1 c), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
have tail₁ : ∀ (IH : ReflTransGen r c b_1), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
Tactic: rcases IH with (IH | IH)
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
have tail : ∀ (ac : ReflTransGen r a b_1) (IH : ReflTransGen r b_1 b_1), ReflTransGen r c_1 b_1 ∨ ReflTransGen r b_1 c_1
Tactic: rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
Cleared hypotheses: c, ac, IH
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
tail : ∀ (ac : ReflTransGen r a b_1) (IH : ReflTransGen r b_1 b_1), ReflTransGen r c_1 b_1 ∨ ReflTransGen r b_1 c_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
have tail₁ : ∀ (e : α) (be : r b_1 e) (ec : ReflTransGen r e c), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
Tactic: rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
-- Lean 4 proof step from Mathlib.Logic.Relation (hypothesis)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
e : α
be : r b_1 e
ec : ReflTransGen r e c
be₁ : r b_1 c_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
have ec₁ : ReflTransGen r c_1 c
Tactic: cases U bd be
Cleared hypotheses: e, be, ec