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

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ ∀ (e : motive (bit b n) = motive (bit b n)), e ▸ h b n = h b n

Tactic:
intros

Goal state after:
motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ h b n = h b n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
⊢ ∀ (e : motive (Nat.bit b n) = motive (Nat.bit b n)),
    e ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)

Tactic:
intros

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e✝ : motive (Nat.bit b n) = motive (Nat.bit b n)
⊢ e✝ ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : a * b = 1
⊢ a⁻¹⁻¹ = a

Tactic:
inv_inv

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : a * b = 1
⊢ a = a
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
⊢ β = β'

Tactic:
funext a

Goal state after:
α : Sort u
β : α → Sort v
f : (a : α) → β a
β' : α → Sort v
f' : (a : α) → β' a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
a : α
⊢ β a = β' a
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:
rw [h, Subsingleton.elim x y]

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
x : α
⊢ f^[n.succ] x = f (f^[n] x)

Tactic:
by
  rw [iterate_succ']
  rfl

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₁⁻¹⁻¹

pp: G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ ∀ (a : α), (a₂⁻¹ * a₁) • a = a

Tactic:
inv_inv

Goal state after:
case refine_2
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ a₁ = a₁

G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ ∀ (a : α), (a₂⁻¹ * a₁) • a = a
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = g • b

Tactic:
rw [← h, smul_inv_smul]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Semigroup (f i)
⊢ ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c)

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Semigroup (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), 1 * a = a

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ 1 * a✝ = a✝
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), 1 * a = a

Tactic:
intros; ext; exact one_mul _

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), a * 1 = a

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ a✝ * 1 = a✝
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Monoid (f i)
⊢ ∀ (x : (i : I) → f i), x ^ 0 = 1

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Monoid (f i)
x✝ : (i : I) → f i
⊢ x✝ ^ 0 = 1
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Monoid (f i)
⊢ ∀ (n : ℕ) (x : (i : I) → f i), x ^ (n + 1) = x ^ n * x

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Monoid (f i)
n✝ : ℕ
x✝ : (i : I) → f i
⊢ x✝ ^ (n✝ + 1) = x✝ ^ n✝ * x✝
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), a / b = a * b⁻¹

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
a✝ b✝ : (i : I) → f i
⊢ a✝ / b✝ = a✝ * b✝⁻¹
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
⊢ ∀ (a : (i : I) → f i), a ^ 0 = 1

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
a✝ : (i : I) → f i
⊢ a✝ ^ 0 = 1
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
⊢ ∀ (n : ℕ) (a : (i : I) → f i), a ^ ↑n.succ = a ^ ↑n * a

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
n✝ : ℕ
a✝ : (i : I) → f i
⊢ a✝ ^ ↑n✝.succ = a✝ ^ ↑n✝ * a✝
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
⊢ ∀ (n : ℕ) (a : (i : I) → f i), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
n✝ : ℕ
a✝ : (i : I) → f i
⊢ a✝ ^ Int.negSucc n✝ = (a✝ ^ ↑n✝.succ)⁻¹
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → InvolutiveInv (f i)
⊢ ∀ (x : (i : I) → f i), x⁻¹⁻¹ = x

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → InvolutiveInv (f i)
x✝ : (i : I) → f i
⊢ x✝⁻¹⁻¹ = x✝
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
a✝ b✝ : (i : I) → f i
⊢ (a✝ * b✝)⁻¹ = b✝⁻¹ * a✝⁻¹
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
a✝ b✝ : (i : I) → f i
x✝ : I
⊢ (a✝ * b✝)⁻¹ x✝ = (b✝⁻¹ * a✝⁻¹) x✝

Tactic:
exact mul_inv_rev _ _

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Group (f i)
⊢ ∀ (a : (i : I) → f i), a⁻¹ * a = 1

Tactic:
intros

Goal state after:
I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → Group (f i)
a✝ : (i : I) → f i
⊢ a✝⁻¹ * a✝ = 1
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
a : α
⊢ Function.Injective (mk a)

Tactic:
intro b₁ b₂ h

Goal state after:
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
b : β
⊢ Function.Injective fun a ↦ (a, b)

Tactic:
intro b₁ b₂ h

Goal state after:
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) b₂
⊢ b₁ = b₂
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_2.inr
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_ge h.2⟩

Goal state after:
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ ¬IsMax a ↔ a < ⊤

Tactic:
by
  rw [not_isMax_iff]
  exact ⟨fun ⟨b, hb⟩ ↦ hb.trans_le le_top, fun h ↦ ⟨⊤, h⟩⟩

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) (b + 1)

Tactic:
apply hd _ _ (Nat.add_lt_add_iff_right.1 h)
    · have : a + 1 = b ∨ a + 1 < b := by lia
      rcases this with (rfl | h)
      · exact ha _
      apply diag_induction P ha hb hd (a + 1) b h
    apply diag_induction P ha hb hd a (b + 1)
    apply Nat.lt_of_le_of_lt (Nat.le_succ _) h

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f

Tactic:
by
  grind [Injective]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ∧ Codisjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)

Tactic:
disjoint_iff,

Goal state after:
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) ∧ Codisjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i) ∧ Codisjoint (f i) (g i)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ AntitoneOn f s

Tactic:
by
  rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ m + f n ≤ f (m + n)

Tactic:
by
  rw [Nat.add_comm m, Nat.add_comm m]
  induction m with
  | zero => rw [Nat.add_zero, Nat.add_zero]
  | succ m ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]
    exact ih.trans_lt (hf (n + m).lt_succ_self)

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ Disjoint a b ↔ Disjoint ↑a ↑b

Tactic:
disjoint_iff,

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ Disjoint ↑a ↑b
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ Disjoint ↑a ↑b

Tactic:
disjoint_iff,

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this✝ : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot hbot
⊢ a ⊓ b = ⊥ ↔ ↑a ⊓ ↑b = ⊥
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ ⊤ ≤ ⊥ ⊔ c

Tactic:
← hab.eq_bot,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ ⊤ ≤ a ⊓ b ⊔ c
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Disjoint ↑a ↑b ↔ Disjoint a b

Tactic:
disjoint_iff,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ⊓ ↑b = ⊥ ↔ Disjoint a b
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ⊓ ↑b = ⊥ ↔ Disjoint a b

Tactic:
disjoint_iff,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ⊓ ↑b = ⊥ ↔ a ⊓ b = ⊥
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Max α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
a b c : α
hab : a ⊔ b = b
hbc : b ⊔ c = c
⊢ a ⊔ c = c

Tactic:
by rw [← hbc, ← sup_assoc, hab]

Goal state after:
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p q : α → Prop
⊢ (∀ (x : α), x ∈ s ∧ p x ↔ x ∈ s ∧ q x) ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)

Tactic:
and_congr_right_iff

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case pos
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
h' : x ≤ y
⊢ x ⊔ y = y

pp: case neg
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : α
h' : ¬x ≤ y
⊢ x ⊔ y = x

Tactic:
exacts [sup_of_le_right h', sup_of_le_left <| (total_of (· ≤ ·) x y).resolve_left h']

Goal state after:
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
hs : s.Nontrivial
z : α
⊢ ∃ x, x ∈ s ∧ x ≠ z

Tactic:
by_contra! H
  rcases hs with ⟨x, hx, y, hy, hxy⟩
  rw [H x hx, H y hy] at hxy
  exact hxy rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := ⋯
lt : LT α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : PartialOrder β
preorder : Preorder α := e.preorder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊓ y) = Min.min (e x) (e y)

Tactic:
intros

Goal state after:
case min
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊓ y✝) = Min.min (e x✝) (e y✝)
Module: Mathlib.Order.Lattice

Goal state before:
pp: case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), e (x ⊔ y) = Max.max (e x) (e y)

Tactic:
intros

Goal state after:
case max
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ e (x✝ ⊔ y✝) = Max.max (e x✝) (e y✝)
Module: Mathlib.Order.Lattice

Goal state before:
pp: case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := ⋯
min : Min α := ⋯
preorder : Preorder α := ⋯
compare : Ord α := ⋯
⊢ ∀ (x y : α), Ord.compare (e x) (e y) = Ord.compare x y

Tactic:
intros

Goal state after:
case compare
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
min : Min α := e.min
preorder : Preorder α := e.preorder
compare : Ord α := e.ord
x✝ y✝ : α
⊢ Ord.compare (e x✝) (e y✝) = Ord.compare x✝ y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

Tactic:
intros

Goal state after:
case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y ≤ e x ↔ y ≤ x

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ ≤ e x✝ ↔ y✝ ≤ x✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ {x y : α}, e y < e x ↔ y < x

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
x✝ y✝ : α
⊢ e y✝ < e x✝ ↔ y✝ < x✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := ⋯
partialOrder : PartialOrder α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

Tactic:
intros

Goal state after:
case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeInf β
min : Min α := e.min
partialOrder : PartialOrder α := e.partialOrder
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

Tactic:
intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝
Module: Mathlib.Order.Lattice

Goal state before:
pp: case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := ⋯
semilatticeInf : SemilatticeInf α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

Tactic:
intros

Goal state after:
case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝