awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
⊢ ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }

Tactic:
have hpk₂ : ¬(p : ℤ[i]) ∣ ⟨k, 1⟩ := fun ⟨x, hx⟩ =>
        lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
          calc
            (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, 1⟩).natAbs := by rw [hx]
            _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
            _ ≤ (norm (p * x : ℤ[i])).natAbs :=
              norm_le_norm_mul_left _ fun hx0 =>
                show (1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hpk : p ∣ HPow.hPow (β := ℕ) k 2 + 1
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
obtain : ∀ (y : ℕ) (hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y), False
⊢ False

Tactic:
obtain ⟨y, hy⟩ := hpk
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
y : ℕ
hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y
rw : HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 = (↑(HPow.hPow (β := ℕ) k 2 + 1) : ℤ[i])
⊢ HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 : ℤ√(-1) } { re := (↑k : ℤ), im := -1 : ℤ√(-1) } =
    HMul.hMul (α := ℤ[i]) (↑p : ℤ[i]) (↑y : ℤ[i])

Tactic:
rw [← hkmul, ← Nat.cast_mul p, ← hy]

Premises used: Nat.cast_mul
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
y : ℕ
hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y
⊢ HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 = (↑(HPow.hPow (β := ℕ) k 2 + 1) : ℤ[i])

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
y : ℕ
hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y
⊢ Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 } ∨
    Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }

Tactic:
have := hpi.2.2 ⟨k, 1⟩ ⟨k, -1⟩ ⟨y, by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp⟩
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime (M := ℤ[i]) (↑p : ℤ[i])
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = HMul.hMul (α := ZMod p) (↑k : ZMod p) (↑k : ZMod p)
hkmul :
  HPow.hPow (α := ℤ[i]) (β := ℕ) (↑k : ℤ[i]) 2 + 1 =
    HMul.hMul (α := ℤ[i]) { re := (↑k : ℤ), im := 1 } { re := (↑k : ℤ), im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
hpk₂ : ¬Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }
y : ℕ
hy : HPow.hPow (β := ℕ) k 2 + 1 = p * y
this :
  Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 } ∨
    Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }
inl : ∀ (this : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := 1 }), False
inr : ∀ (this : Dvd.dvd (α := ℤ[i]) (↑p : ℤ[i]) { re := (↑k : ℤ), im := -1 }), False
⊢ False

Tactic:
tauto
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
a b : ℕ
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = p
rw : ∀ (a b : ZMod 4), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≠ (↑3 : ZMod 4)
⊢ ∀ (a b : ZMod 4), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≠ (↑p : ZMod 4)

Tactic:
rw [← ZMod.natCast_mod p 4, hp3]

Premises used: ZMod.natCast_mod, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
a b : ℕ
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = p
⊢ ∀ (a b : ZMod 4), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≠ (↑3 : ZMod 4)

Tactic:
decide
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible (M := ℤ[i]) (↑p : ℤ[i])
a b : ℕ
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = p
this : ∀ (a b : ZMod 4), HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≠ (↑p : ZMod 4)
⊢ HPow.hPow (α := ZMod 4) (β := ℕ) (↑a : ZMod 4) 2 + HPow.hPow (α := ZMod 4) (β := ℕ) (↑b : ZMod 4) 2 =
    (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2) : ZMod 4)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Prime (M := ℤ[i]) (↑p : ℤ[i]) ↔ p % 4 = 3

Tactic:
⟨mod_four_eq_three_of_nat_prime_of_prime p, prime_of_nat_prime_of_mod_four_eq_three p⟩

Premises used: GaussianInt.mod_four_eq_three_of_nat_prime_of_prime, Iff.intro, GaussianInt.prime_of_nat_prime_of_mod_four_eq_three
-- Module: Mathlib.NumberTheory.Zsqrtd.ToReal
Goal:
d : ℤ
h0d : 0 ≤ d
hd : ∀ (n : ℤ), d ≠ n * n
⊢ Function.Injective (α := ℤ√d) (β := ℝ) (⇑(toReal h0d) : (a : ℤ√d) → ℝ)

Tactic:
lift_injective _ hd

Premises used: Zsqrtd.lift_injective
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
h : Symmetric r
⊢ Symmetric rᶜ

Tactic:
fun _ _ hr hr' =>
  hr <| h hr'

Premises used: Symmetric, Not
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsAntichain r ∅

Tactic:
pairwise_empty _

Premises used: Set.pairwise_empty, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
a : α
⊢ IsAntichain r {a}

Tactic:
pairwise_singleton _ _

Premises used: Set.pairwise_singleton, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsAntichain r s
h : t ⊆ s
⊢ IsAntichain r t

Tactic:
hs.mono h

Premises used: Set.Pairwise.mono, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r₁ r₂ : α → α → Prop
s : Set α
hs : IsAntichain r₁ s
h : r₂ ≤ r₁
⊢ IsAntichain r₂ s

Tactic:
hs.mono' <| compl_le_compl h

Premises used: compl_le_compl, IsAntichain, Set.Pairwise.mono'
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r₁ r₂ : α → α → Prop
s : Set α
hs : IsAntichain r₁ s
h : s.Pairwise fun ⦃a b : α⦄ ↦ r₂ a b → r₁ a b
⊢ IsAntichain r₂ s

Tactic:
hs.imp_on <| h.imp fun _ _ h h₁ h₂ => h₁ <| h h₂

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

Tactic:
Set.Pairwise.eq hs ha hb <| not_not_intro h

Premises used: not_not_intro, Set.Pairwise.eq
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
a b : α
ha : a ∈ s
hb : b ∈ s
h : r b a
⊢ a = b

Tactic:
(hs.eq hb ha h).symm

Premises used: IsAntichain.eq, Eq.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
h : IsAntichain r univ
⊢ Std.Antisymm r

Tactic:
⟨fun _ _ ha _ => h.eq trivial trivial ha⟩

Premises used: trivial, Std.Antisymm.mk, IsAntichain.eq
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
inl : ∀ (hab : r a b), a = b
inr : ∀ (hab : a = b), a = b
inr₁ : ∀ (hab : r b a), a = b
⊢ a = b

Tactic:
obtain hab | hab | hab := trichotomous_of r a b

Premises used: trichotomous_of
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

Tactic:
h.eq ha hb hab

Premises used: IsAntichain.eq
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

Tactic:
exact h.eq ha hb hab

Premises used: IsAntichain.eq
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

Tactic:
hab
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

Tactic:
exact hab
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b

Tactic:
h.eq' ha hb hab

Premises used: IsAntichain.eq'
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
inst : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b

Tactic:
exact h.eq' ha hb hab

Premises used: IsAntichain.eq'
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
⊢ IsAntichain (flip r) s

Tactic:
fun _ ha _ hb h =>
  hs hb ha h.symm

Premises used: Ne.symm, Set.Pairwise, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsAntichain r s
⊢ IsAntichain (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) s

Tactic:
hs.flip

Premises used: IsAntichain.flip
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False

Tactic:
hs hb hc (ne_of_apply_ne _ hbc) (h hr)

Premises used: ne_of_apply_ne
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False

Tactic:
exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)

Premises used: ne_of_apply_ne
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : β → α
hf : Injective f
h : ∀ ⦃a b : β⦄, r' a b → r (f a) (f b)
⊢ IsAntichain r' (f ⁻¹' s)

Tactic:
fun _ hb _ hc hbc hr =>
  hs hb hc (hf.ne hbc) <| h hr

Premises used: Function.Injective.ne, Set.Pairwise, IsAntichain, Not
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
⊢ IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b ∧ ¬r b a

Tactic:
Set.pairwise_insert

Premises used: Set.pairwise_insert, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hs : IsAntichain r s
hl : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r b a
hr : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b
⊢ IsAntichain r (insert a s)

Tactic:
isAntichain_insert.2 ⟨hs, fun _ hb hab => ⟨hr hb hab, hl hb hab⟩⟩

Premises used: Iff.mpr, isAntichain_insert, And.intro
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hr : Symmetric r
⊢ IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b

Tactic:
pairwise_insert_of_symmetric hr.compl

Premises used: Symmetric.compl, Set.pairwise_insert_of_symmetric, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hs : IsAntichain r s
hr : Symmetric r
h : ∀ ⦃b : α⦄, b ∈ s → a ≠ b → ¬r a b
⊢ IsAntichain r (insert a s)

Tactic:
(isAntichain_insert_of_symmetric hr).2 ⟨hs, h⟩

Premises used: Iff.mpr, And.intro, isAntichain_insert_of_symmetric
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : Membership.mem (γ := Set β) ((⇑φ : (a : α) → β) '' s) b
b' : β
hb' : Membership.mem (γ := Set β) ((⇑φ : (a : α) → β) '' s) b'
h₁ : b ≠ b'
h₂ : r' b b'
rw :
  ∀ (hb : ∃ x ∈ s, (φ : (a : α) → β) x = b) ⦃b' : β⦄ (hb' : ∃ x ∈ s, (φ : (a : α) → β) x = b') (h₁ : b ≠ b')
    (h₂ : r' b b'), False
⊢ False

Tactic:
rw [Set.mem_image] at hb hb'

Premises used: Set.mem_image
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, (φ : (a : α) → β) x = b
b' : β
hb' : ∃ x ∈ s, (φ : (a : α) → β) x = b'
h₁ : b ≠ b'
h₂ : r' b b'
obtain :
  ∀ (a : α) (has : a ∈ s) (a' : α) (has' : a' ∈ s)
    (h₁ : Ne.{u_2 + 1} (α := β) ((φ : (a : α) → β) a : β) ((φ : (a : α) → β) a' : β))
    (h₂ : r' ((φ : (a : α) → β) a) ((φ : (a : α) → β) a')), False
⊢ False

Tactic:
obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'

Premises used: rfl
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : Ne.{u_2 + 1} (α := β) ((φ : (a : α) → β) a : β) ((φ : (a : α) → β) a' : β)
h₂ : r' ((φ : (a : α) → β) a) ((φ : (a : α) → β) a')
haa' : a = a'
rw rw₁ : Eq.{u_2 + 1} (α := β) ((φ : (a : α) → β) a' : β) ((φ : (a : α) → β) a' : β)
⊢ Eq.{u_2 + 1} (α := β) ((φ : (a : α) → β) a : β) ((φ : (a : α) → β) a' : β)

Tactic:
rw [haa']
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : Ne.{u_2 + 1} (α := β) ((φ : (a : α) → β) a : β) ((φ : (a : α) → β) a' : β)
h₂ : r' ((φ : (a : α) → β) a) ((φ : (a : α) → β) a')
⊢ False

Tactic:
exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)

Premises used: RelEmbedding.map_rel_iff, Iff.mp
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
t : Set β
ht : IsAntichain r' t
φ : r ↪r r'
⊢ IsAntichain r ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
fun _ ha _s ha' hne hle =>
  ht ha ha' (fun h => hne (φ.injective h)) (φ.map_rel_iff.mpr hle)

Premises used: Iff.mpr, RelEmbedding.injective, Set.Pairwise, RelEmbedding.map_rel_iff, IsAntichain, Not
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ≃r r'
⊢ IsAntichain r' ((⇑φ : (a : α) → β) '' s)

Tactic:
hs.image_relEmbedding φ.toRelEmbedding

Premises used: IsAntichain.image_relEmbedding, RelIso.toRelEmbedding
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
t : Set β
hs : IsAntichain r' t
φ : r ≃r r'
⊢ IsAntichain r ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
hs.preimage_relEmbedding φ.toRelEmbedding

Premises used: RelIso.toRelEmbedding, IsAntichain.preimage_relEmbedding
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
φ : r ↪r r'
⊢ IsAntichain r' ((⇑φ : (a : α) → β) '' s) ↔ IsAntichain r s

Tactic:
⟨fun h => (φ.injective.preimage_image s).subst (h.preimage_relEmbedding φ), fun h =>
    h.image_relEmbedding φ⟩

Premises used: IsAntichain.image_relEmbedding, RelEmbedding.injective, Eq.subst, Function.Injective.preimage_image, Iff.intro, IsAntichain.preimage_relEmbedding
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
φ : r ≃r r'
⊢ IsAntichain r' ((⇑φ : (a : α) → β) '' s) ↔ IsAntichain r s

Tactic:
@image_relEmbedding_iff _ _ _ _ _ (φ : r ↪r r')

Premises used: IsAntichain.image_relEmbedding_iff
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
φ : α ↪o β
⊢ IsAntichain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s)

Tactic:
image_relEmbedding hs _

Premises used: IsAntichain.image_relEmbedding
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
t : Set β
ht : IsAntichain (fun (x1 x2 : β) ↦ x1 ≤ x2) t
φ : α ↪o β
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
preimage_relEmbedding ht _

Premises used: IsAntichain.preimage_relEmbedding
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
φ : α ↪o β
⊢ IsAntichain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s) ↔ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
image_relEmbedding_iff

Premises used: IsAntichain.image_relEmbedding_iff
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
φ : α ≃o β
⊢ IsAntichain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s)

Tactic:
image_relEmbedding hs _

Premises used: IsAntichain.image_relEmbedding
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : LE α
inst_1 : LE β
φ : α ≃o β
⊢ IsAntichain (fun (x1 x2 : β) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) '' s) ↔ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
image_relEmbedding_iff

Premises used: IsAntichain.image_relEmbedding_iff
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
t : Set β
ht : IsAntichain (fun (x1 x2 : β) ↦ x1 ≤ x2) t
φ : α ≃o β
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) ⁻¹' t)

Tactic:
preimage_relEmbedding ht _

Premises used: IsAntichain.preimage_relEmbedding
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
t : Set β
φ : α ≃o β
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) ((⇑φ : (a : α) → β) ⁻¹' t) ↔ IsAntichain (fun (x1 x2 : β) ↦ x1 ≤ x2) t

Tactic:
⟨fun h => (φ.image_preimage t).subst (h.image_iso φ), fun h => h.preimage_iso _⟩

Premises used: IsAntichain.image_iso, Eq.subst, IsAntichain.preimage_iso, Iff.intro, OrderIso.image_preimage
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
inst : LE α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsAntichain (fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2) s

Tactic:
fun _ ha _ hb hab => hs hb ha hab.symm

Premises used: Ne.symm, Set.Pairwise, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
inst : LE α
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ IsAntichain (fun (x1 x2 : αᵒᵈ) ↦ x1 ≤ x2) s

Tactic:
⟨to_dual, to_dual⟩

Premises used: Iff.intro, IsAntichain.to_dual
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
inst : BooleanAlgebra α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (compl '' s)

Tactic:
(hs.image_embedding (OrderIso.compl α).toOrderEmbedding).flip

Premises used: OrderIso.toOrderEmbedding, IsAntichain.flip, OrderIso.compl, IsAntichain.image_embedding, OrderDual
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
inst : BooleanAlgebra α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (compl ⁻¹' s)

Tactic:
fun _ ha _ ha' hne hle =>
  hs ha' ha (fun h => hne (compl_inj_iff.mp h.symm)) (compl_le_compl hle)

Premises used: compl_le_compl, Set.Pairwise, IsAntichain, Iff.mp, compl_inj_iff, Eq.symm, Not
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
h : IsAntichain r s
⊢ IsAntichain r (s \ t)

Tactic:
h.subset Set.diff_subset

Premises used: Set.diff_subset, IsAntichain.subset
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsAntichain (fun (x1 x2 : (↑s : Type u_1)) ↦ r (↑x1 : α) (↑x2 : α)) (s ↓∩ t) ↔ IsAntichain r (s ∩ t)

Tactic:
simp [IsAntichain, Set.Pairwise]

Premises used: Set.Pairwise, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsAntichain (fun (x1 x2 : (↑s : Type u_1)) ↦ r (↑x1 : α) (↑x2 : α)) univ ↔ IsAntichain r s

Tactic:
simpa using isAntichain_preimage_subtypeVal s univ

Premises used: Set.univ, isAntichain_preimage_subtypeVal
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
rw : (s ∪ t).Pairwise rᶜ ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
rw₁ : (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
rw₂ : (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
rw₃ rw₄ :
  (s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a) ↔
    s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a

Tactic:
rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]

Premises used: Set.pairwise_union, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
s : Set α
hs : s.Subsingleton
r : α → α → Prop
⊢ IsAntichain r s

Tactic:
hs.pairwise _

Premises used: Set.Subsingleton.pairwise, IsAntichain
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
by_contra! : ∀ (hne : x ≠ y), False
⊢ x = y

Tactic:
by_contra! hne
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r x y
⊢ False

Tactic:
ht hx hy hne h
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r x y
⊢ False

Tactic:
exact ht hx hy hne h
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r y x
⊢ False

Tactic:
ht hy hx hne.symm h

Premises used: Ne.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
h : r y x
⊢ False

Tactic:
exact ht hy hx hne.symm h

Premises used: Ne.symm
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
⊢ r x y ∨ r y x

Tactic:
cases hs hx hy hne with
  | inl h => exact ht hx hy hne h
  | inr h => exact ht hy hx hne.symm h
-- Module: Mathlib.Order.Antichain
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsChain r s ∧ IsAntichain r s ↔ s.Subsingleton

Tactic:
⟨fun h ↦ subsingleton_of_isChain_of_isAntichain h.1 h.2, fun h ↦ ⟨h.isChain, h.isAntichain _⟩⟩

Premises used: Set.Subsingleton.isAntichain, Set.Subsingleton.isChain, And.right, And.left, And.intro, subsingleton_of_isChain_of_isAntichain, Iff.intro