awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inhabited_h : Inhabited α
⊢ Nontrivial.{u_1} (Option α)

Tactic:
exact ⟨none, some default, nofun⟩
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
inst_1 : Nontrivial β
⊢ Nontrivial (α × β)

Tactic:
Prod.snd_surjective.nontrivial

Premises used: Function.Surjective.nontrivial, Prod.snd_surjective
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
inst_1 : Nonempty β
⊢ Nontrivial (α × β)

Tactic:
Prod.fst_surjective.nontrivial

Premises used: Prod.fst_surjective, Function.Surjective.nontrivial
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty.{u_4 + 1} (f i)
inst_1 : Nontrivial.{u_4} (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)

Tactic:
(Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

Premises used: Function.Injective.nontrivial, Classical.choice, Function.update_injective
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty.{u_4 + 1} (f i)
inst_1 : Nontrivial.{u_4} (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)

Tactic:
exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

Premises used: Function.Injective.nontrivial, Classical.choice, Function.update_injective
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
β : Type u_2
I : Type u_3
f : I → Type u_4
inst : Inhabited I
inst_1 : ∀ (i : I), Nonempty.{u_4 + 1} (f i)
inst_2 : Nontrivial.{u_4} (f default)
⊢ Nontrivial ((i : I) → f i)

Tactic:
nontrivial_at default

Premises used: Inhabited.default, Pi.nontrivial_at
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
β : Type u_2
h : Nonempty α
inst : Nontrivial β
⊢ Nontrivial (α → β)

Tactic:
h.elim fun a ↦ Pi.nontrivial_at a

Premises used: Nonempty.elim, Pi.nontrivial_at
-- Module: Mathlib.Logic.Nontrivial.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
x y : α
⊢ x ≤ y

Tactic:
le_of_eq (Subsingleton.elim x y)

Premises used: le_of_eq, Subsingleton.elim
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
⊢ Nontrivial α ↔ ∃ (x : α), ∃ (y : α), x ≠ y

Tactic:
⟨fun h ↦ h.exists_pair_ne, fun h ↦ ⟨h⟩⟩

Premises used: Nontrivial.mk, Iff.intro, Nontrivial.exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
inst : Nontrivial α
⊢ ∃ (x : α), ∃ (y : α), x ≠ y

Tactic:
Nontrivial.exists_pair_ne

Premises used: Nontrivial.exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
f : α → β
hf : Injective f
⊢ Nontrivial β

Tactic:
let ⟨x, y, h⟩ := exists_pair_ne α
  ⟨⟨f x, f y, hf.ne h⟩⟩

Premises used: Nontrivial, Function.Injective.ne, Nontrivial.mk, _private.0.Function.Injective.nontrivial.match_1, Exists.intro, exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
f : α → β
hf : Injective f
y : β
rcases : ∀ (x₁ x₂ : α) (hx : x₁ ≠ x₂), ∃ (x : α), f x ≠ y
⊢ ∃ (x : α), f x ≠ y

Tactic:
rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
pos : ∀ (h : f x₂ = y), ∃ (x : α), f x ≠ y
neg : ∀ (h : ¬f x₂ = y), ∃ (x : α), f x ≠ y
⊢ ∃ (x : α), f x ≠ y

Tactic:
by_cases h : f x₂ = y
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : 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:
⟨x₁, (hf.ne_iff' h).2 hx⟩

Premises used: Iff.mpr, Exists.intro, Function.Injective.ne_iff'
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : 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:
exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : 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:
⟨x₂, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : 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:
exact ⟨x₂, h⟩
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x : α
rcases : ∀ (y y' : α) (h : y ≠ y'), ∃ (y : α), y ≠ x
⊢ ∃ (y : α), y ≠ x

Tactic:
rcases exists_pair_ne α with ⟨y, y', h⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
pos : ∀ (hx : x = y), ∃ (y : α), y ≠ x
neg : ∀ (hx : ¬x = y), ∃ (y : α), y ≠ x
⊢ ∃ (y : α), y ≠ x

Tactic:
by_cases hx : x = y
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ x ≠ y'

Tactic:
rw [← hx] at h
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
h₁ : x ≠ y'
⊢ x = y

Tactic:
rw [← hx] at h
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ (y : α), y ≠ x

Tactic:
⟨y', h.symm⟩

Premises used: Ne.symm, Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ (y : α), y ≠ x

Tactic:
exact ⟨y', h.symm⟩
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ (y : α), y ≠ x

Tactic:
⟨y, Ne.symm hx⟩

Premises used: Ne.symm, Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
inst_1 : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ (y : α), y ≠ x

Tactic:
exact ⟨y, Ne.symm hx⟩
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
inst : Nontrivial α
x : α
⊢ ∃ (y : α), y ≠ x

Tactic:
Decidable.exists_ne x

Premises used: Decidable.exists_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
x y : α
h : x ≠ y
⊢ Nontrivial α

Tactic:
⟨⟨x, y, h⟩⟩

Premises used: Nontrivial.mk, Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
x : α
⊢ Nontrivial α ↔ ∃ (y : α), y ≠ x

Tactic:
⟨fun h ↦ @exists_ne α h x, fun ⟨_, hy⟩ ↦ nontrivial_of_ne _ _ hy⟩

Premises used: Nontrivial, exists_ne, nontrivial_of_ne, Iff.intro, _private.0.nontrivial_iff_exists_ne.match_1
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
obtain : ∀ (f g : α → β) (h : f ≠ g), Nontrivial β
⊢ Nontrivial β

Tactic:
obtain ⟨f, g, h⟩ := exists_pair_ne (α → β)

Premises used: exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
f g : α → β
h : f ≠ g
⊢ ∃ (x : α), ¬f x = g x

Tactic:
rw [ne_eq, funext_iff, Classical.not_forall] at h

Premises used: funext_iff, ne_eq, Classical.not_forall
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
f g : α → β
h : ∃ (x : α), ¬f x = g x
obtain : ∀ (a : α) (h : ¬f a = g a), Nontrivial β
⊢ Nontrivial β

Tactic:
obtain ⟨a, h⟩ := h
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
f g : α → β
a : α
h : ¬f a = g a
⊢ Nontrivial β

Tactic:
nontrivial_of_ne _ _ h

Premises used: nontrivial_of_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
β : Type u_4
inst : Nontrivial (α → β)
f g : α → β
a : α
h : ¬f a = g a
⊢ Nontrivial β

Tactic:
exact nontrivial_of_ne _ _ h

Premises used: nontrivial_of_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
⊢ Nontrivial Prop

Tactic:
⟨⟨True, False, true_ne_false⟩⟩

Premises used: False, Nontrivial.mk, True, Exists.intro, true_ne_false
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
⊢ Nonempty α

Tactic:
let ⟨x, _⟩ := _root_.exists_pair_ne α
  ⟨x⟩

Premises used: _private.0.Nontrivial.to_nonempty.match_1, Nonempty.intro, Nonempty, exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
h : Subsingleton α
⊢ ∀ (x y : α), x = y

Tactic:
Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
h : Subsingleton α
⊢ ∀ (x y : α), x = y

Tactic:
exact Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
⊢ ¬Nontrivial α ↔ Subsingleton α

Tactic:
simp only [nontrivial_iff, subsingleton_iff, not_exists, Classical.not_not]

Premises used: subsingleton_iff, Classical.not_not, not_exists, nontrivial_iff
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
inst : Subsingleton α
⊢ ¬Nontrivial α

Tactic:
fun ⟨⟨x, y, h⟩⟩ ↦ h <| Subsingleton.elim x y

Premises used: False, _private.0.not_nontrivial.match_1, Subsingleton.elim, Not
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
inst : Nontrivial α
⊢ ¬Subsingleton α

Tactic:
fun _ => not_nontrivial _ ‹_›

Premises used: not_nontrivial, Not
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
rw : ¬¬Nontrivial α ↔ Nontrivial α
rw₁ rw₂ : Nontrivial α ↔ Nontrivial α
⊢ ¬Subsingleton α ↔ Nontrivial α

Tactic:
rw [← not_nontrivial_iff_subsingleton, Classical.not_not]

Premises used: Classical.not_not, not_nontrivial_iff_subsingleton
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
rw : Nontrivial α ∨ ¬Nontrivial α
⊢ Subsingleton α ∨ Nontrivial α

Tactic:
rw [← not_nontrivial_iff_subsingleton, or_comm]

Premises used: not_nontrivial_iff_subsingleton, or_comm
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α

Tactic:
Classical.em _

Premises used: Classical.em
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α

Tactic:
exact Classical.em _

Premises used: Classical.em
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
inst : Nontrivial α
inst_1 : Subsingleton α
⊢ False

Tactic:
not_nontrivial _ ‹_›

Premises used: not_nontrivial
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
rcases : ∀ (x y : β) (h : x ≠ y), Nontrivial α
⊢ Nontrivial α

Tactic:
rcases exists_pair_ne β with ⟨x, y, h⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
rcases : ∀ (x' : α) (hx' : f x' = x), Nontrivial α
⊢ Nontrivial α

Tactic:
rcases hf x with ⟨x', hx'⟩
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
rcases : ∀ (y' : α) (hy' : f y' = y), Nontrivial α
⊢ Nontrivial α

Tactic:
rcases hf y with ⟨y', hy'⟩
-- Module: Mathlib.Logic.Nontrivial.Defs
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'

Tactic:
fun H ↦ h ?_

Premises used: Not
-- Module: Mathlib.Logic.Nontrivial.Defs
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
refine : ∀ (H : x' = y'), x = y
⊢ x' ≠ y'

Tactic:
refine fun H ↦ h ?_
-- Module: Mathlib.Logic.Nontrivial.Defs
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'
rw₂ rw₃ : f y' = f y'
⊢ x = y

Tactic:
rw [← hx', ← hy', H]
-- Module: Mathlib.Logic.Nontrivial.Defs
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'

Tactic:
have : x' ≠ y' := by
    refine fun H ↦ h ?_
    rw [← hx', ← hy', H]
-- Module: Mathlib.Logic.Nontrivial.Defs
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
this : x' ≠ y'
⊢ Nontrivial α

Tactic:
⟨⟨x', y', this⟩⟩

Premises used: Nontrivial.mk, Exists.intro
-- Module: Mathlib.Logic.Nontrivial.Defs
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
this : x' ≠ y'
⊢ Nontrivial α

Tactic:
exact ⟨⟨x', y', this⟩⟩
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_1
β : Type u_2
⊢ Nontrivial Bool

Tactic:
⟨⟨true, false, nofun⟩⟩

Premises used: False, _private.0.Bool.instNontrivial.match_1, Nontrivial.mk, Bool.true, Exists.intro, Bool.false
-- Module: Mathlib.Logic.Nontrivial.Defs
Goal:
α : Type u_3
inst : Zero α
a : α
inst_1 : NeZero a
⊢ Nontrivial α

Tactic:
⟨⟨a, 0, NeZero.ne a⟩⟩

Premises used: Nontrivial.mk, Exists.intro, OfNat.ofNat, NeZero.ne
-- Module: Mathlib.Logic.OpClass
Goal:
α : Sort u
β : Sort v
op : α → α → β
inst : IsSymmOp op
⊢ flip op = op

Tactic:
funext fun a ↦ funext fun b ↦ (IsSymmOp.symm_op a b).symm

Premises used: IsSymmOp.symm_op, funext, Eq.symm
-- Module: Mathlib.Logic.OpClass
Goal:
α : Sort u
β : Sort v
f : α → β → β
h : LeftCommutative f
⊢ RightCommutative fun (x : β) (y : α) ↦ f y x

Tactic:
⟨fun _ _ _ ↦ (h.left_comm _ _ _).symm⟩

Premises used: LeftCommutative.left_comm, RightCommutative.mk, Eq.symm
-- Module: Mathlib.Logic.OpClass
Goal:
α : Sort u
β : Sort v
f : β → α → β
h : RightCommutative f
⊢ LeftCommutative fun (x : α) (y : β) ↦ f y x

Tactic:
⟨fun _ _ _ ↦ (h.right_comm _ _ _).symm⟩

Premises used: LeftCommutative.mk, RightCommutative.right_comm, Eq.symm
-- Module: Mathlib.Logic.OpClass
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)
rw₂ rw₃ : f b (f a c) = f b (f a c)
⊢ f a (f b c) = f b (f a c)

Tactic:
rw [← ha.assoc, hc.comm a, ha.assoc]

Premises used: Std.Associative.assoc, Std.Commutative.comm
-- Module: Mathlib.Logic.OpClass
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
rw₂ rw₃ : f a (f c b) = f a (f c b)
⊢ f (f a b) c = f (f a c) b

Tactic:
rw [ha.assoc, hc.comm b, ha.assoc]

Premises used: Std.Associative.assoc, Std.Commutative.comm
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r p : α → α → Prop
hr : Pairwise r
h : ∀ ⦃i j : α⦄, r i j → p i j
⊢ Pairwise p

Tactic:
fun _i _j hij => h <| hr hij

Premises used: Pairwise
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r : α → α → Prop
a b : α
h : Pairwise r
⊢ ¬r a b → a = b

Tactic:
not_imp_comm.1 <| @h _ _

Premises used: not_imp_comm, Iff.mp
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r : α → α → Prop
inst : Subsingleton α
⊢ Pairwise r

Tactic:
fun _ _ h ↦ False.elim <| h.elim <| Subsingleton.elim _ _

Premises used: False.elim, Pairwise, Ne.elim, Subsingleton.elim
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
ι : Type u_3
f : ι → α
⊢ Injective f ↔ Pairwise ((fun (x1 x2 : α) ↦ x1 ≠ x2) on f)

Tactic:
forall₂_congr fun _i _j => not_imp_not.symm

Premises used: forall₂_congr, Pairwise, Function.Injective, Iff.symm, not_imp_not
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Pairwise r
f : β → α
hf : Injective f
⊢ Pairwise (r on f)

Tactic:
fun _ _ h ↦ hr <| hf.ne h

Premises used: Function.Injective.ne, Pairwise
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
hr : Pairwise (r on f)
hf : Surjective f
⊢ Pairwise r

Tactic:
hf.forall₂.2 fun _ _ h ↦ hr <| ne_of_apply_ne f h

Premises used: Iff.mpr, ne_of_apply_ne, Pairwise, Function.Surjective.forall₂
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
hf : Bijective f
⊢ Pairwise (r on f) ↔ Pairwise r

Tactic:
⟨fun hr ↦ hr.of_comp_of_surjective hf.surjective, fun hr ↦ hr.comp_of_injective hf.injective⟩

Premises used: Pairwise.comp_of_injective, Function.Bijective.injective, Function.Bijective.surjective, Pairwise.of_comp_of_surjective, Iff.intro
-- Module: Mathlib.Logic.Pairwise
Goal:
n : ℕ
R : Fin n.succ → Fin n.succ → Prop
inst : Std.Symm R
⊢ Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun (i j : Fin n) ↦ R i.succ j.succ

Tactic:
simp only [pairwise_fin_succ_iff, comm (b := 0) (r := R), and_self_left]

Premises used: comm, and_self_left, pairwise_fin_succ_iff
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : ∀ (a b : α), r a b
⊢ s.Pairwise r

Tactic:
fun a _ b _ _ => h a b

Premises used: Set.Pairwise
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r p : α → α → Prop
s : Set α
h : s.Pairwise r
hrp : s.Pairwise fun ⦃a b : α⦄ ↦ r a b → p a b
⊢ s.Pairwise p

Tactic:
fun _a ha _b hb hab => hrp ha hb hab <| h ha hb hab

Premises used: Set.Pairwise
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r p : α → α → Prop
s : Set α
h : s.Pairwise r
hpq : ∀ ⦃a b : α⦄, r a b → p a b
⊢ s.Pairwise p

Tactic:
h.imp_on <| pairwise_of_forall s _ hpq

Premises used: Set.pairwise_of_forall, Set.Pairwise.imp_on
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a b : α
hs : s.Pairwise r
ha : a ∈ s
hb : b ∈ s
h : ¬r a b
⊢ a = b

Tactic:
of_not_not fun hab => h <| hs ha hb hab

Premises used: of_not_not
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Refl r
⊢ s.Pairwise r ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r a b

Tactic:
forall₄_congr fun a _ _ _ => or_iff_not_imp_left.symm.trans <| or_iff_right_of_imp <| Eq.ndrec <|
    refl a

Premises used: Set.Pairwise, Classical.or_iff_not_imp_left, Iff.trans, Eq.ndrec, or_iff_right_of_imp, refl, Iff.symm, forall₄_congr
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
ι : Type u_3
r : α → α → Prop
f : ι → α
s : Set α
hs : s.Pairwise r
hf : Injective f
hfs : ∀ (x : ι), f x ∈ s
⊢ Pairwise (r on f)

Tactic:
fun i j hij => hs (hfs i) (hfs j) (hf.ne hij)

Premises used: Function.Injective.ne, Pairwise
-- Module: Mathlib.Logic.Pairwise
Goal:
α : Type u_1
r : α → α → Prop
h : Pairwise r
s : Set α
⊢ s.Pairwise r

Tactic:
fun _ _ _ _ w => h w

Premises used: Set.Pairwise
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Refl r
x y : α
hr : x ≠ y → r x y
⊢ r x y

Tactic:
grind [Std.Refl]

Premises used: Std.Refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Refl r
x y : α
⊢ x ≠ y → r x y ↔ r x y

Tactic:
⟨Std.Refl.rel_of_ne_imp, fun hr _ ↦ hr⟩

Premises used: Iff.intro, Std.Refl.rel_of_ne_imp
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Refl r ↔ Subrelation Eq r

Tactic:
grind [Std.Refl, Subrelation]

Premises used: Std.Refl, Subrelation
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Irrefl r ↔ Subrelation r Ne

Tactic:
grind [Std.Irrefl, Subrelation]

Premises used: Std.Irrefl, Subrelation
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
H : Symmetric r
x y : α
⊢ r x y ↔ r y x

Tactic:
⟨fun h ↦ H h, fun h ↦ H h⟩

Premises used: Iff.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h : Symmetric r
⊢ Eq.{max 1 u_1} (flip r) r

Tactic:
funext₂ fun _ _ ↦ propext <| h.iff _ _

Premises used: funext₂, propext, Symmetric.iff
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Symmetric r → Eq.{max 1 u_1} (swap (φ := fun (x y : α) ↦ Prop) r) r

Tactic:
Symmetric.flip_eq

Premises used: Symmetric.flip_eq
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Eq.{max 1 u_1} (flip r) r ↔ Symmetric r

Tactic:
⟨fun h _ _ ↦ (congr_fun₂ h _ _).mp, Symmetric.flip_eq⟩

Premises used: Eq.mp, congr_fun₂, Symmetric.flip_eq, Iff.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Eq.{max 1 u_1} (swap (φ := fun (x y : α) ↦ Prop) r) r ↔ Symmetric r

Tactic:
flip_eq_iff

Premises used: flip_eq_iff
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
h : Symmetric r
f : α → β
⊢ Symmetric (r on f)

Tactic:
fun _ _ hab ↦ h hab

Premises used: Symmetric
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : β → β → Prop
h : Equivalence r
f : α → β
⊢ Equivalence (r on f)

Tactic:
⟨fun a ↦ h.refl (f a), h.symm, h.trans⟩

Premises used: Equivalence.symm, Equivalence.refl, Equivalence.trans, Equivalence.mk
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
f : γ → β
h : ∀ (x : α) (y : γ), (r ∘r fun (x1 : β) (x2 : γ) ↦ x1 = f x2) x y ↔ r x (f y)
⊢ Eq (α := (a : α) → (c : γ) → Prop) (r ∘r fun (x1 : β) (x2 : γ) ↦ x1 = f x2) fun (x1 : α) (x2 : γ) ↦ r x1 (f x2)

Tactic:
ext x y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
f : γ → β
x : α
y : γ
⊢ (r ∘r fun (x1 : β) (x2 : γ) ↦ x1 = f x2) x y ↔ r x (f y)

Tactic:
simp [Comp]

Premises used: Relation.Comp
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (r ∘r fun (x1 x2 : β) ↦ x1 = x2) = r

Tactic:
comp_eq_fun ..

Premises used: Relation.comp_eq_fun
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
f : γ → α
h : ∀ (x : γ) (y : β), ((fun (x1 : γ) (x2 : α) ↦ f x1 = x2) ∘r r) x y ↔ r (f x) y
⊢ Eq (α := (a : γ) → (c : β) → Prop) ((fun (x1 : γ) (x2 : α) ↦ f x1 = x2) ∘r r) fun (x : γ) ↦ r (f x)

Tactic:
ext x y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
r : α → β → Prop
f : γ → α
x : γ
y : β
⊢ ((fun (x1 : γ) (x2 : α) ↦ f x1 = x2) ∘r r) x y ↔ r (f x) y

Tactic:
simp [Comp]

Premises used: Relation.Comp
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (fun (x1 x2 : α) ↦ x1 = x2) ∘r r = r

Tactic:
fun_eq_comp ..

Premises used: Relation.fun_eq_comp
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : Prop → α → Prop
⊢ Eq.{max 1 u_1} ((fun (x1 x2 : Prop) ↦ x1 ↔ x2) ∘r r) r

Tactic:
grind [eq_comp]

Premises used: Relation.eq_comp
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → Prop → Prop
⊢ Eq.{max 1 u_1} (r ∘r fun (x1 x2 : Prop) ↦ x1 ↔ x2) r

Tactic:
grind [comp_eq]

Premises used: Relation.comp_eq
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
h : ∀ (a : α) (d : δ), ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q

Tactic:
funext a d
-- 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 : δ
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

Tactic:
apply propext

Premises used: propext
-- 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 : δ
h : ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) 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

Tactic:
constructor
-- 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 ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩

Premises used: Relation.Comp, And.intro, Exists.intro, _private.0.Relation.comp_assoc.match_1
-- 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 ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩