mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero
n0 : ¬0 = 0
⊢ (if 0 >>> 1 = 0 then 0 else (0 >>> 1).log2.succ) < if 0 = 0 then 0 else (log2 0).succ

pp: case succ
n : Nat
n0 : ¬n + 1 = 0
⊢ (if (n + 1) >>> 1 = 0 then 0 else ((n + 1) >>> 1).log2.succ) < if n + 1 = 0 then 0 else (n + 1).log2.succ

Tactic:
·

Goal state after:
case zero
n0 : ¬0 = 0
⊢ (if 0 >>> 1 = 0 then 0 else (0 >>> 1).log2.succ) < if 0 = 0 then 0 else (log2 0).succ
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ.zero
n0 : ¬0 + 1 = 0
⊢ (if (0 + 1) >>> 1 = 0 then 0 else ((0 + 1) >>> 1).log2.succ) < if 0 + 1 = 0 then 0 else (0 + 1).log2.succ

pp: case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ

Tactic:
·

Goal state after:
case succ.zero
n0 : ¬0 + 1 = 0
⊢ (if (0 + 1) >>> 1 = 0 then 0 else ((0 + 1) >>> 1).log2.succ) < if 0 + 1 = 0 then 0 else (0 + 1).log2.succ
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
n : Nat
⊢ b.toNat < 2

pp: case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
·

Goal state after:
b : Bool
n : Nat
⊢ b.toNat < 2
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case H
b : Bool
n : Nat
⊢ 0 < 2

Tactic:
·

Goal state after:
case H
b : Bool
n : Nat
⊢ 0 < 2
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c

pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
·

Goal state after:
case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r a b
⊢ r a c
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c

pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
·

Goal state after:
case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a c : α
h₁ : ¬r a a
h₂ : r a c
⊢ r a c
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
·

Goal state after:
case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c

pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
·

Goal state after:
case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
·

Goal state after:
case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
·

Goal state after:
case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 ≠ 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

pp: case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a

Tactic:
·

Goal state after:
case zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 ≠ 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ 2 * k' ≠ 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y

pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x

pp: case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α

Tactic:
exact Classical.em _

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z

pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y

Tactic:
·

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f x = g y
z : α
⊢ f z = g z
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y

Tactic:
·

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ f x = g y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
this : (fun x ↦ c) = fun x ↦ if x = b₀ then c' else c
⊢ c = c'

pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ ((fun g ↦ g ∘ f) fun x ↦ c) = (fun g ↦ g ∘ f) fun x ↦ if x = b₀ then c' else c

Tactic:
·

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
this : (fun x ↦ c) = fun x ↦ if x = b₀ then c' else c
⊢ c = c'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd

Tactic:
·

Goal state after:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
h : update default i x = update default i y
⊢ x = y

pp: case refine_1
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
h : Injective (Pi.map f)
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
⊢ Pi.map f (update default i x) = Pi.map f (update default i y)

Tactic:
·

Goal state after:
case refine_2
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
h : update default i x = update default i y
⊢ x = y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
·

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
·

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
·

Goal state after:
case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
·

Goal state after:
case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

pp: case refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b, r a b

Tactic:
·

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b, r a b

Tactic:
·

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b, r a b
Module: Mathlib.Data.FunLike.Equiv

Goal state before:
pp: E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ inv e b = a ↔ b = e a

Tactic:
constructor <;> rintro ⟨_, rfl⟩

Goal state after:
case mp
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
⊢ b = e (inv e b)

case mpr
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
a : α
⊢ inv e (e a) = a
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type 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:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type 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:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c : α
inst✝ : IsTrans α r
a b : α
h₁ : ReflGen r a b
⊢ ReflGen r a b

pp: case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₁ : ReflGen r a b
h₂ : r b c
⊢ ReflGen r a c

Tactic:
·

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c : α
inst✝ : IsTrans α r
a b : α
h₁ : ReflGen r a b
⊢ ReflGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b c✝ : α
inst✝ : IsTrans α r
a c : α
h₂ : r a c
⊢ ReflGen r a c

pp: case single.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝ : IsTrans α r
a b c : α
h₂ : r b c
h₁ : r a b
⊢ ReflGen r a c

Tactic:
·

Goal state after:
case single.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a✝ b c✝ : α
inst✝ : IsTrans α r
a c : α
h₂ : r a c
⊢ ReflGen r a c
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.refl
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
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 ⋯

pp: case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
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 ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
·

Goal state after:
case tail.refl
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
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 ⋯
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
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 ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
·

Goal state after:
case tail.head
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop},
    motive b ⋯ → (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯) → motive a a✝
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 ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a ⋯
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr.inl
α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

pp: case mpr.inr
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Tactic:
·

Goal state after:
case mpr.inl
α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr.inr
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Tactic:
·

Goal state after:
case mpr.inr
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

pp: case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
·

Goal state after:
case tail.inl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl.inl
α : Type u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
ac : ReflTransGen r a b✝
IH : ReflTransGen r b✝ b✝
⊢ ReflTransGen r c✝ b✝ ∨ ReflTransGen r b✝ c✝

pp: case tail.inl.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
·

Goal state after:
case tail.inl.inl
α : Type u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
ac : ReflTransGen r a b✝
IH : ReflTransGen r b✝ b✝
⊢ ReflTransGen r c✝ b✝ ∨ ReflTransGen r b✝ c✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
·

Goal state after:
case tail.inl.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
e : α
be : r b✝ e
ec : ReflTransGen r e c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝

Tactic:
·

Goal state after:
case tail.inr
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r c b✝
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝