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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| x ⊓ y ⊓ x \ y

Tactic:
inf_comm

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = ⊥
| x \ y ⊓ (x ⊓ y)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : x ⊓ y ⊓ z = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z

Tactic:
inf_comm

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : z ⊔ x ⊓ y = x \ y ⊔ x ⊓ y
i : z ⊓ (x ⊓ y) = x \ y ⊓ (x ⊓ y)
⊢ x \ y = z
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥

Tactic:
;

Goal state after:
α : Type u_2
inst✝¹ : HeytingAlgebra α
a : α
inst✝ : Nontrivial α
⊢ a ≤ aᶜ ∧ a ≠ aᶜ ↔ a = ⊥
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint (b ⊓ a) (a ⊓ b)ᶜ

Tactic:
inf_comm

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint (a ⊓ b) (a ⊓ b)ᶜ
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬(e (some x)).isSome = true
hn : e none = none
⊢ False

Tactic:
Option.not_isSome_iff_eq_none,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : e (some x) = none
hn : e none = none
⊢ False
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α✝
a✝ b✝ : α✝
α : Type u_2
inst✝ : CoheytingAlgebra α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ a ⊓ b ≤ c

Tactic:
inf_comm

Goal state after:
ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α✝
a✝ b✝ : α✝
α : Type u_2
inst✝ : CoheytingAlgebra α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α✝
a✝ b✝ : α✝
α : Type u_2
inst✝ : CoheytingAlgebra α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c

Tactic:
;

Goal state after:
ι : Type u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : HeytingAlgebra α✝
a✝ b✝ : α✝
α : Type u_2
inst✝ : CoheytingAlgebra α
a b c : αᵒᵈ
⊢ a ≤ toDual (ofDual c \ ofDual b) ↔ b ⊓ a ≤ c
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:
;

Goal state after:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
x : α
⊢ x ∈ insert a s \ {a} ↔ x ∈ s
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ y \ x ⊓ x = ⊥

Tactic:
inf_comm,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x = ⊥
Module: Mathlib.Order.BooleanAlgebra.Set

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

Tactic:
;

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z

Tactic:
;

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x ≤ y ∧ Disjoint x z
⊢ x \ z ≤ y \ z
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ y ⊓ (z ⊔ x) ⊔ z = y

Tactic:
inf_comm,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hd : Disjoint x z
hz : z ≤ y
hs : (x ⊔ z) ⊓ y = y
⊢ (z ⊔ x) ⊓ y ⊔ z = y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ (x ⊓ y) = y \ (z ⊓ y)

Tactic:
inf_comm,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ (y ⊓ x) = y \ (z ⊓ y)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ (y ⊓ z) = y \ (z ⊓ y)

Tactic:
inf_comm

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y ⊓ x = y ⊓ z
⊢ y \ (z ⊓ y) = y \ (z ⊓ y)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥

Tactic:
;

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = x ⊓ y ⊓ z ⊔ x \ y

Tactic:
inf_comm,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ (y \ z) = z ⊓ (x ⊓ y) ⊔ x \ y
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
⊢ (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)

Tactic:
by
  ext i
  cases i <;> rfl

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

Goal state before:
pp: α : Type u_9
β : Type u_10
⊢ (Equiv.refl α).sumCongr (Equiv.refl β) = Equiv.refl (α ⊕ β)

Tactic:
by
  ext i
  cases i <;> rfl

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ z ⊓ x = x \ y ⊔ x ⊓ z

Tactic:
inf_comm

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ x ⊓ z = x \ y ⊔ x ⊓ z
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
⊢ Option.elim' default Subtype.val (if h : a = default then none else some ⟨a, h⟩) = a

Tactic:
;

Goal state after:
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
⊢ Option.elim' default Subtype.val (if h : a = default then none else some ⟨a, h⟩) = a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z

Tactic:
inf_comm y,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) = x ⊓ y ⊔ x \ z ⊓ y \ z
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ x \ z ⊓ y = (y ⊓ x) \ z

Tactic:
inf_comm,

Goal state after:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y z : α
⊢ y ⊓ x \ z = (y ⊓ x) \ z
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ (a ⊓ b) \ c = (b ⊓ a) \ c

Tactic:
inf_comm

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

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

Tactic:
;

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h✝ : yᶜ ≤ xᶜ
h : xᶜᶜ ≤ yᶜᶜ
⊢ x ≤ y
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : p a
⊢ (ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)

Tactic:
simp [Perm.subtypeCongr.apply, h]

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

Goal state before:
pp: ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)

Tactic:
simp [Perm.subtypeCongr.apply, h]

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

Goal state before:
pp: case pos
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ (x ∘ Subtype.val) ⟨a, h✝⟩ = x a

Tactic:
;

Goal state after:
case pos
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst✝ : DecidablePred p
x₀ : { a // p a } → β
x✝ : { x // x ∘ Subtype.val = x₀ }
x : α → β
hx : x ∘ Subtype.val = x₀
a : α
h✝ : p a
⊢ (x ∘ Subtype.val) ⟨a, h✝⟩ = x a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊓ y = y ⊓ xᶜ

Tactic:
inf_comm

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ y ⊓ xᶜ = y ⊓ xᶜ
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤

Tactic:
;

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y = ⊤ ∧ x = ⊤ ↔ x = ⊤ ∧ y = ⊤
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst

Tactic:
;

Goal state after:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
ι : Type ?u.23
π : ι → Type u_9
f : { f // ∀ (i : ι), (f i).fst = i }
i : ι
⊢ π (↑f i).fst
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case refl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : α → Type u_10
a : Sigma β
x✝ : { s // s.fst = a.fst }
⊢ (fun b ↦ ⟨⟨a.fst, b⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
        ⟨a, ⋯⟩) =
    ⟨a, ⋯⟩

Tactic:
;

Goal state after:
case refl
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
β : α → Type u_10
a : Sigma β
x✝ : { s // s.fst = a.fst }
⊢ (fun b ↦ ⟨⟨a.fst, b⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
        ⟨a, ⋯⟩) =
    ⟨a, ⋯⟩
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ c = (sigmaSigmaSubtype p h) ⟨⟨a, ⟨b, c⟩⟩, h⟩

Tactic:
;

Goal state after:
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ c = (sigmaSigmaSubtype p h) ⟨⟨a, ⟨b, c⟩⟩, h⟩
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a' : α
b' : β
⊢ ⟨⟨a', b'⟩, ⋯⟩ = ⟨⟨a', b'⟩, ⋯⟩

Tactic:
;

Goal state after:
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a' : α
b' : β
⊢ ⟨⟨a', b'⟩, ⋯⟩ = ⟨⟨a', b'⟩, ⋯⟩
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a : α
b : β
s : { s // s.fst = a ∧ s.snd.fst = b }
⊢ (sigmaSigmaSubtypeEq a b) s = cast ⋯ (↑s).snd.snd

Tactic:
simp [sigmaSigmaSubtypeEq]

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

Goal state before:
pp: α : Type u_9
β : Type u_10
γ : α → β → Type u_11
a : α
b : β
c : γ a b
⊢ (sigmaSigmaSubtypeEq a b).symm c = ⟨⟨a, ⟨b, c⟩⟩, ⋯⟩

Tactic:
simp [sigmaSigmaSubtypeEq]

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

Goal state before:
pp: case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a✝ : Subtype p₁
⊢ (fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯)
      ((fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯) ⟦a✝⟧) =
    ⟦a✝⟧

Tactic:
;

Goal state after:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p₁ : α → Prop
s₁ : Setoid α
s₂ : Setoid (Subtype p₁)
p₂ : Quotient s₁ → Prop
hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧
h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y
a✝ : Subtype p₁
⊢ (fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯)
      ((fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯) ⟦a✝⟧) =
    ⟦a✝⟧
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b \ b ∆ a = a ⊓ b

Tactic:
inf_comm,

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b \ b ∆ a = b ⊓ a
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r

Tactic:
;

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if (if r = a then b else if r = b then a else r) = a then b
    else if (if r = a then b else if r = b then a else r) = b then a else if r = a then b else if r = b then a else r) =
    r
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r

Tactic:
;

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
r a b : α
⊢ (if r = a then b else if r = b then a else r) = if r = b then a else if r = a then b else r
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}

Tactic:
;

Goal state after:
case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ j ∈ insert j s \ {a}
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}

Tactic:
;

Goal state after:
case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ a ∈ insert j s \ {i}
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
⊢ (sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e) = (prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm

Tactic:
by
  ext ⟨a, b⟩ : 1
  simp only [trans_apply, sigmaCongrRight_apply, prodCongrRight_apply]
  rfl

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
x✝¹ : β → P
x✝ : α
⊢ (piCongrLeft' (fun x ↦ P) e).symm x✝¹ x✝ = (piCongrLeft' (fun a ↦ P) e.symm) x✝¹ x✝

Tactic:
;

Goal state after:
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
x✝¹ : β → P
x✝ : α
⊢ (piCongrLeft' (fun x ↦ P) e).symm x✝¹ x✝ = (piCongrLeft' (fun a ↦ P) e.symm) x✝¹ x✝
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ (b ⇨ a) = (b ⇨ a) ⊓ (a ⇨ b)

Tactic:
inf_comm

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ

Tactic:
inf_comm,

Goal state after:
case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ aᶜ ⊓ (b ⊓ cᶜ) = aᶜ ⊓ b ⊓ cᶜ
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case e_a
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c

Tactic:
· apply inf_left_right_swap

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {True} ↔ x✝ ∈ {a | p a}

Tactic:
;

Goal state after:
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {True} ↔ x✝ ∈ {a | p a}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {False} ↔ x✝ ∈ {a | ¬p a}

Tactic:
;

Goal state after:
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {False} ↔ x✝ ∈ {a | ¬p a}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
x✝¹ : Set α
x✝ : α
⊢ x✝ ∈ id '' x✝¹ ↔ x✝ ∈ id x✝¹

Tactic:
;

Goal state after:
α : Type u_1
x✝¹ : Set α
x✝ : α
⊢ x✝ ∈ id '' x✝¹ ↔ x✝ ∈ id x✝¹
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊆ range f ∩ s' → f ⁻¹' s ⊆ f ⁻¹' s'

Tactic:
intro r

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : range f ∩ s ⊆ range f ∩ s'
⊢ f ⁻¹' s ⊆ f ⁻¹' s'
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ f ⁻¹' s ⊆ f ⁻¹' s' → range f ∩ s ⊆ range f ∩ s'

Tactic:
intro r

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
⊢ range f ∩ s ⊆ range f ∩ s'
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
c : α
d : β
⊢ (c, d) ∈ {a} ×ˢ {b} ↔ (c, d) ∈ {(a, b)}

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
c : α
d : β
⊢ (c, d) ∈ {a} ×ˢ {b} ↔ (c, d) ∈ {(a, b)}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty

Tactic:
← image_inter_preimage,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' (s ∩ f ⁻¹' t)).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
x✝ : ↑s
⊢ x✝ ∈ range (codRestrict f s h) ↔ x✝ ∈ Subtype.val ⁻¹' range f

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
x✝ : ↑s
⊢ x✝ ∈ range (codRestrict f s h) ↔ x✝ ∈ Subtype.val ⁻¹' range f
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t

Tactic:
;

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s

Tactic:
;

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) ↔ y ∈ f '' s ∪ g '' sᶜ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ range (s.piecewise f g) ↔ y ∈ f '' s ∪ g '' sᶜ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : InjOn f s
⊢ (f '' s).Nontrivial

Tactic:
by
  obtain ⟨x, hx, y, hy, hxy⟩ := hs
  exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
x✝ : α default
⊢ x✝ ∈ uniqueElim ⁻¹' univ.pi t ↔ x✝ ∈ t default

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : Unique ι
t : (i : ι) → Set (α i)
x✝ : α default
⊢ x✝ ∈ uniqueElim ⁻¹' univ.pi t ↔ x✝ ∈ t default
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ ↑y ∈ s

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ ↑y ∈ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}

Tactic:
;

Goal state after:
case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ {y}
⊢ ∃ a, f a = y

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ {y}
⊢ ∃ a, f a = y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ a, f a = y

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ a, f a = y
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {x} = {x'}

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {x} = {x'}
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f

Tactic:
by
  refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩
  rw [← singleton_eq_singleton_iff]; apply h
  rw [image_singleton, image_singleton, hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' ⊤ = ⊤

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' ⊤ = ⊤
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥