mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
⊢ inst1 = inst2

Tactic:
ext

Goal state after:
α : Type u_1
inst1 inst2 : BEq α
inst✝¹ : LawfulBEq α
inst✝ : LawfulBEq α
x✝ y✝ : α
⊢ (x✝ == y✝) = (x✝ == y✝)
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α ∧ Nonempty α

Tactic:
constructor

Goal state after:
case left
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Subsingleton α

case right
α : Sort u
x✝ : Nonempty (Unique α)
u : Unique α
⊢ Nonempty α
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

Tactic:
rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h

Goal state after:
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

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

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

Goal state before:
pp: α : 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:
constructor

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

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: α : 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

Tactic:
constructor

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

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: α : Type u_1
β : Type u_2
r : α → β → Prop
⊢ Relation.Map r id id = r

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
x✝¹ : α
x✝ : β
⊢ Relation.Map r id id x✝¹ x✝ ↔ r x✝¹ x✝
Module: Mathlib.Logic.Function.Conjugate

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)

Tactic:
← hb (f (ga' x)),

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ gb' (gb (f (ga' x))) = gb' (f x)
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Tactic:
ext

Goal state after:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ((ab.equivCongr cd).symm x✝¹) x✝ = ((ab.symm.equivCongr cd.symm) x✝¹) x✝
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
⊢ f^[m + n] a = f^[n] a ↔ f^[n] (f^[m] a) = f^[n] a

Tactic:
by rw [← iterate_add_apply, Nat.add_comm]

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x✝ : α ≃ β
⊢ (fun f ↦ ofBijective ↑f ⋯) ((fun f ↦ ⟨⇑f, ⋯⟩) x✝) = x✝

Tactic:
ext

Goal state after:
α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x✝¹ : α ≃ β
x✝ : α
⊢ ((fun f ↦ ofBijective ↑f ⋯) ((fun f ↦ ⟨⇑f, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
⊢ (fun x ↦ a • x)^[n + 1] = fun x ↦ a ^ (n + 1) • x

Tactic:
ext

Goal state after:
M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
x✝ : α
⊢ (fun x ↦ a • x)^[n + 1] x✝ = a ^ (n + 1) • 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) → Mul (f i)
inst✝ : ∀ (i : I), IsMulCommutative (f i)
x✝¹ x✝ : (i : I) → f i
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext

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) → Mul (f i)
inst✝ : ∀ (i : I), IsMulCommutative (f i)
x✝² x✝¹ : (i : I) → f i
x✝ : I
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * 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) → Mul (f i)
inst✝ : ∀ (i : I), IsMulCommutative (f i)
x✝² x✝¹ : (i : I) → f i
x✝ : I
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * x✝²) x✝

Tactic:
apply mul_comm'

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) → CommMagma (f i)
x✝¹ x✝ : (i : I) → f i
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext

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) → CommMagma (f i)
x✝² x✝¹ : (i : I) → f i
x✝ : I
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * 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) → Semigroup (f i)
a✝ b✝ c✝ : (i : I) → f i
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)

Tactic:
ext

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
x✝ : I
⊢ (a✝ * b✝ * c✝) x✝ = (a✝ * (b✝ * c✝)) 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) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ 1 * a✝ = a✝

Tactic:
ext

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
x✝ : I
⊢ (1 * a✝) x✝ = a✝ 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) → MulOneClass (f i)
a✝ : (i : I) → f i
⊢ a✝ * 1 = a✝

Tactic:
ext

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
x✝ : I
⊢ (a✝ * 1) x✝ = a✝ 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) → InvOneClass (f i)
⊢ 1⁻¹ = 1

Tactic:
ext

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) → InvOneClass (f i)
x✝ : I
⊢ 1⁻¹ x✝ = 1 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) → Monoid (f i)
x✝ : (i : I) → f i
⊢ x✝ ^ 0 = 1

Tactic:
ext

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✝ : I
⊢ (x✝¹ ^ 0) x✝ = 1 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) → Monoid (f i)
n✝ : ℕ
x✝ : (i : I) → f i
⊢ x✝ ^ (n✝ + 1) = x✝ ^ n✝ * x✝

Tactic:
ext

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✝ : I
⊢ (x✝¹ ^ (n✝ + 1)) x✝ = (x✝¹ ^ n✝ * 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) → DivInvMonoid (f i)
a✝ b✝ : (i : I) → f i
⊢ a✝ / b✝ = a✝ * b✝⁻¹

Tactic:
ext

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
x✝ : I
⊢ (a✝ / b✝) x✝ = (a✝ * b✝⁻¹) 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✝ : (i : I) → f i
⊢ a✝ ^ 0 = 1

Tactic:
ext

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
x✝ : I
⊢ (a✝ ^ 0) x✝ = 1 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)
n✝ : ℕ
a✝ : (i : I) → f i
⊢ a✝ ^ ↑n✝.succ = a✝ ^ ↑n✝ * a✝

Tactic:
ext

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
x✝ : I
⊢ (a✝ ^ ↑n✝.succ) x✝ = (a✝ ^ ↑n✝ * a✝) 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)
n✝ : ℕ
a✝ : (i : I) → f i
⊢ a✝ ^ Int.negSucc n✝ = (a✝ ^ ↑n✝.succ)⁻¹

Tactic:
ext

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
x✝ : I
⊢ (a✝ ^ Int.negSucc n✝) x✝ = (a✝ ^ ↑n✝.succ)⁻¹ 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) → DivInvOneMonoid (f i)
⊢ 1⁻¹ = 1

Tactic:
ext

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) → DivInvOneMonoid (f i)
x✝ : I
⊢ 1⁻¹ x✝ = 1 x✝
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
d : α
⊢ (fun x ↦ x.getD d) ∘ some = id

Tactic:
ext

Goal state after:
α : Type u_1
d x✝ : α
⊢ ((fun x ↦ x.getD d) ∘ some) x✝ = id 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) → InvolutiveInv (f i)
x✝ : (i : I) → f i
⊢ x✝⁻¹⁻¹ = x✝

Tactic:
ext

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✝ : I
⊢ x✝¹⁻¹⁻¹ x✝ = 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:
ext

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
x✝ : I
⊢ (a✝ * b✝)⁻¹ x✝ = (b✝⁻¹ * a✝⁻¹) 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
h : a✝ * b✝ = 1
⊢ a✝⁻¹ = b✝

Tactic:
ext

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
h : a✝ * b✝ = 1
x✝ : I
⊢ a✝⁻¹ x✝ = b✝ 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) → Group (f i)
a✝ : (i : I) → f i
⊢ a✝⁻¹ * a✝ = 1

Tactic:
ext

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
x✝ : I
⊢ (a✝⁻¹ * a✝) x✝ = 1 x✝
Module: Mathlib.Order.Basic

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
c : β
ha : a.snd < c
hb : c < b.snd
⊢ ∃ a_1,
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)

Tactic:
exact ⟨(_, c), Or.inr ⟨h₁, ha⟩, Or.inr ⟨le_rfl, hb⟩⟩

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

Goal state before:
pp: ⊢ bne = xor

Tactic:
constructor

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ f ∘ rangeSplitting f = Subtype.val

Tactic:
ext

Goal state after:
α : Type u
β : Type v
f : α → β
x✝ : ↑(range f)
⊢ (f ∘ rangeSplitting f) x✝ = ↑x✝
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
⊢ (cmp a b).swap = cmp b a

Tactic:
unfold cmp cmpUsing
  by_cases h : a < b <;> by_cases h₂ : b < a <;> simp_all [lt_asymm]

Goal state after:
Module: Mathlib.Order.PropInstances

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

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g → ∀ (i : ι), Disjoint (f i) (g i)

case mpr
ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ (∀ (i : ι), Disjoint (f i) (g i)) → Disjoint f g
Module: Mathlib.Order.Monotone.Basic

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

Tactic:
monotone_toDual_comp_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Antitone (f ∘ ⇑ofDual) ↔ Monotone f
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

case mpr
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b ↔ ∃ c, b = a ⊔ c

Tactic:
constructor

Goal state after:
case mp
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ≤ b → ∃ c, b = a ⊔ c

case mpr
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ (∃ c, b = a ⊔ c) → a ≤ b
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s✝ t u : Set α
p : α → Prop
s : { s // ∀ (a : α), a ∈ s → p a }
⊢ (fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) ((fun s ↦ {a | ↑a ∈ ↑s}) s) = s

Tactic:
ext

Goal state after:
α : Type u_1
s✝ t u : Set α
p : α → Prop
s : { s // ∀ (a : α), a ∈ s → p a }
x✝ : α
⊢ x✝ ∈ ↑((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) ((fun s ↦ {a | ↑a ∈ ↑s}) s)) ↔ x✝ ∈ ↑s
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ {x | x ∈ l} = {a} ↔ l = [a]

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ {x | x ∈ l} = {a} → l = [a]

case mpr
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ l = [a] → {x | x ∈ l} = {a}
Module: Mathlib.Order.Lattice

Goal state before:
pp: case e_sup
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ sup✝¹ = sup✝

Tactic:
ext

Goal state after:
case e_sup
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x✝¹ x✝ : α
⊢ sup✝¹ x✝¹ x✝ = sup✝ x✝¹ x✝
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ Subsingleton ↑s ↔ s.Subsingleton

Tactic:
constructor

Goal state after:
case mp
α : Type u
s : Set α
⊢ Subsingleton ↑s → s.Subsingleton

case mpr
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton ↑s
Module: Mathlib.Order.GaloisConnection.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y

case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ b ⊔ (a \ c ⊔ c \ b)

Tactic:
simpa using @sdiff_sdiff_sdiff_le_sdiff

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)

Tactic:
ext

Goal state after:
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
x✝ : f α
⊢ (mapEquiv f (Equiv.refl α)) x✝ = (Equiv.refl (f α)) x✝
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
⊢ Functor.map ⇑(Equiv.refl α) = id

Tactic:
ext

Goal state after:
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
x✝ : f α
⊢ ⇑(Equiv.refl α) <$> x✝ = id x✝
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
⊢ Functor.map ⇑(k.trans h) = Functor.map ⇑h ∘ Functor.map ⇑k

Tactic:
by
    ext x
    apply LawfulFunctor.comp_map k h x

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ a ≤ bᶜ ↔ Disjoint a b

Tactic:
rw [← himp_bot, le_himp_iff, disjoint_iff_inf_le]

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
x : α
⊢ x ∈ insert a s \ {a} ↔ x ∈ s

Tactic:
simp [and_iff_left_of_imp (ne_of_mem_of_not_mem · h)]

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
ext

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ insert a (s \ {a}) ↔ x✝ ∈ s
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ (fun a ↦ ⟨↑e (some a), ⋯⟩) ((fun b ↦ ((↑e).symm ↑b).get ⋯) b) = b

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ ↑((fun a ↦ ⟨↑e (some a), ⋯⟩) ((fun b ↦ ((↑e).symm ↑b).get ⋯) b)) = ↑b
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ z ⊓ y \ x = ⊥ ↔ z ≤ x

Tactic:
← disjoint_iff

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
⊢ Disjoint z (y \ x) ↔ z ≤ x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = x ⊓ y

Tactic:
inf_eq_right.mpr hx

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
h : x ⊓ y = ⊥
⊢ y = y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : yᶜ ≤ xᶜ
⊢ x ≤ y

Tactic:
by have h := compl_le_compl h; simpa using h

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

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ x ⊓ xᶜ ≤ ⊥

Tactic:
constructor

Goal state after:
case left
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).fst ≤ ⊥.fst

case right
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ (x ⊓ xᶜ).snd ≤ ⊥.snd
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤ ≤ x ⊔ xᶜ

Tactic:
constructor

Goal state after:
case left
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤.fst ≤ (x ⊔ xᶜ).fst

case right
α : Type u
β : Type u_1
x✝ y z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x : α × β
⊢ ⊤.snd ≤ (x ⊔ xᶜ).snd
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ x \ y = x ⊓ yᶜ

Tactic:
ext

Goal state after:
case fst
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).fst = (x ⊓ yᶜ).fst

case snd
α : Type u
β : Type u_1
x✝ y✝ z : α
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
x y : α × β
⊢ (x \ y).snd = (x ⊓ yᶜ).snd