mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a x y

Tactic:
h,

Goal state after:
M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a y y
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x

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

Goal state after:
α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x
Module: Mathlib.Logic.Basic

Goal state before:
pp: β : Sort u
b a : β
h : a = cast ⋯ b
⊢ a ≍ b

Tactic:
h,

Goal state after:
β : Sort u
b a : β
h : a = cast ⋯ b
⊢ cast ⋯ b ≍ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
by_cases hp : P <;> by_cases hq : Q <;> simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
simp [h, forall_prop_of_false, forall_prop_of_true]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
simp [h, forall_prop_of_false, forall_prop_of_true]

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

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
h : f = g
⊢ g x = g y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
obtain ⟨c, rfl⟩ := h₂

Goal state after:
case pos
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
c : α₁
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ (f₁₂ c)) = extend f₁₂ g (e' ∘ f₂₃) (f₁₂ c)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ (if P then f x else f (f x)) = if ¬P then x else f x

Tactic:
h,

Goal state after:
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ (if P then f x else x) = if ¬P then x else f x
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
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q

Tactic:
funext a d

Goal state after:
α : 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: case single
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
a b b✝ : α
hc : r a b✝
⊢ r a b✝

Tactic:
| single hc =>

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

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

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ f (f' (gb x)) = gb (f (f' x))
Module: Mathlib.Logic.Function.Iterate

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

Tactic:
h,

Goal state after:
α : Type u
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ f^[n] x = x
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
h : mulSingle i x = 1
⊢ mulSingle i x i = 1

Tactic:
h,

Goal state after:
ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
h : mulSingle i x = 1
⊢ 1 i = 1
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ (a • b) • c • d = (a • c) • b • d

Tactic:
by rw [smul_assoc, smul_assoc, smul_comm b]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
have : SMulCommClass β α β := .symm ..

Goal state after:
α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
this : SMulCommClass β α β
⊢ a • b * c • d = (a * c) • (b * d)
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 : a = g • b
⊢ g⁻¹ • a = b

Tactic:
h,

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ g⁻¹ • g • b = b
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 : a = g⁻¹ • b
⊢ g • a = b

Tactic:
h,

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ g • g⁻¹ • b = b
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ x • 1 * (y * z) = x • y • z

Tactic:
h,

Goal state after:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ x • (y * z) = x • y • z
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G✝ : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst✝¹ : Group G
inst✝ : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ a⁻¹ • a • b = c

Tactic:
h,

Goal state after:
M : Type u_1
N : Type u_2
G✝ : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
G : Type u_9
P : Type u_10
inst✝¹ : Group G
inst✝ : MulAction G P
a : G
b c : P
h : a • b = a • c
⊢ a⁻¹ • a • c = c
Module: Mathlib.Data.Option.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map (g₁ ∘ f₁) (some a) = Option.map g₂ (Option.map f₂ (some a))

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ Option.map (g₂ ∘ f₂) (some a) = Option.map g₂ (Option.map f₂ (some a))
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ b < a

Tactic:
by
  rw [LinearOrder.compare_eq_compareOfLessAndEq,
    compareOfLessAndEq_eq_gt le_antisymm le_total not_le]

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α : Type u_1
inst✝ : LT α
⊢ DenselyOrdered αᵒᵈ → DenselyOrdered α

Tactic:
convert! @OrderDual.denselyOrdered αᵒᵈ _

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
⊢ ¬P x

Tactic:
intro hx'
      obtain ⟨M, hM, hM'⟩ := hind x hx hx'
      exact IH _ hM hM'

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ⊢ LinearOrder Prop

Tactic:
exact Lattice.toLinearOrder Prop

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
by
  simp only [Monotone, Antitone]
  grind [not_le]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ ⊥ ⊓ y' ⊔ x' ⊓ (y ⊓ y') = ⊥

Tactic:
bot_inf_eq,

Goal state after:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ ⊥ ⊔ x' ⊓ (y ⊓ y') = ⊥
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
have : NoMaxOrder {n // P n} :=
    ⟨fun n ↦ Exists.intro ⟨(h n.1).choose, (h n.1).choose_spec.2⟩ (h n.1).choose_spec.1⟩

Goal state after:
P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
this : NoMaxOrder { n // P n }
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
Module: Mathlib.Order.Disjoint

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

Tactic:
← coe_bot,

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 ⊔ (b ⊔ c) = b ⊔ c

Tactic:
← sup_assoc,

Goal state after:
α✝ : 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 ⊔ b ⊔ c = b ⊔ c
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 : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b

Tactic:
← sup_assoc,

Goal state after:
α✝ : 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 : α
⊢ a ⊔ a ⊔ b = a ⊔ b
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑(a ⊔ b) = ⊤ ↔ a ⊔ b = ⊤

Tactic:
← coe_top,

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
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

Tactic:
← sup_assoc,

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = b ⊔ (a ⊔ c)
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = b ⊔ (a ⊔ c)

Tactic:
← sup_assoc,

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = b ⊔ a ⊔ c
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: x : Prop
⊢ x ∈ {True, False}

Tactic:
rw [mem_insert_iff, mem_singleton_iff]

Goal state after:
x : Prop
⊢ x = True ∨ x = False
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hac : c ≤ a
hbc : c ≤ b
h : a \ c = b \ c
⊢ a \ c ⊔ c = b

Tactic:
h,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hac : c ≤ a
hbc : c ≤ b
h : a \ c = b \ c
⊢ b \ c ⊔ c = b
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s : Set α
⊢ sᶜ ∪ s = univ

Tactic:
rw [union_comm, union_compl_self]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊔ z = y

Tactic:
h,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ x ⊔ z = y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
h,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ x ⊓ z = ⊥
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
⊢ t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Tactic:
by
  ext x
  unfold Set.ite
  push _ ∈ _
  tauto

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

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

Tactic:
h,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y \ x = y \ z
⊢ ⊥ = y ⊓ z ⊓ y \ z
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 \ x

Tactic:
h,

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

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

Tactic:
h,

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
hx : y ≤ x
hy : y ≠ ⊥
⊢ x \ y < x

Tactic:
refine sdiff_le.lt_of_ne fun h => hy ?_

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

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

Tactic:
← sup_assoc,

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

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

Tactic:
bot_inf_eq,

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

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

Tactic:
h,

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (y \ z) ≤ x \ y ∧ x \ y ≤ (x \ z) \ (y \ z)

Tactic:
sdiff_le_comm

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : swap a c = swap a d
⊢ (swap a c) a = d

Tactic:
h,

Goal state after:
α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : swap a c = swap a d
⊢ (swap a d) a = d
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : BooleanAlgebra β
⊢ BooleanAlgebra α

Tactic:
by
  let top := e.top
  let compl := e.compl
  let himp := e.himp
  let generalizedBooleanAlgebra := e.generalizedBooleanAlgebra
  apply e.injective.booleanAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
← sup_assoc,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ (b ⊓ c) ⊔ a ⊓ (bᶜ ⊓ cᶜ) ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
⊢ g (f x) ∈ s ↔ x ∈ s

Tactic:
hfg x

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
⊢ x ∈ s ↔ x ∈ s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
simp only [← and_and_right, mem_inter_iff, mem_prod]

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ ∅.piecewise f g i = g i

Tactic:
simp [piecewise]

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ univ)
i : α
⊢ univ.piecewise f g i = f i

Tactic:
simp [piecewise]

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g j = f j

Tactic:
simp [piecewise]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x✝ : α
⊢ (∃ y, f y = x✝) ↔ x✝ = y

Tactic:
h,

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x✝ : α
⊢ (∃ y_1, y = x✝) ↔ x✝ = y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
h,

Goal state after:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ ∅ = s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
h,

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ False ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s

Tactic:
by
  rw [compl_eq_univ_sdiff, image_sdiff_preimage, image_univ]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ val ⁻¹' s = univ

Tactic:
by
  rw [← preimage_range, range_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
⊢ (fun o ↦ o.elim b f) '' range some = range f

Tactic:
by
  rw [← range_comp']
  simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
a : (i : ι) → α i
hab : ∀ (i : ι), f i (a i) = b i
hat : ∀ (i : ι), i ∈ s → a i ∈ t i
⊢ b ∈ Pi.map f '' s.pi t

Tactic:
exact ⟨a, hat, funext hab⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = ∅

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' ∅ = ∅
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f (a * b) = 1

Tactic:
h,

Goal state after:
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f 1 = 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₁) x = g (f₂ x)

Tactic:
h,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₂) x = g (f₂ x)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₁) x = g (f₂ x)

Tactic:
h,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₂) x = g (f₂ x)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
g : N →* P
f₁ f₂ : M →* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₁) x = g (f₂ x)

Tactic:
h,

Goal state after:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
g : N →* P
f₁ f₂ : M →* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ (g.comp f₂) x = g (f₂ x)
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : N
⊢ g (f (g x) * f (g y)) = g (f (g x * g y))

Tactic:
by rw [f.map_mul]

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁ ∩ f '' s

Tactic:
exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r

Tactic:
exact (subset_sdiff.1 hrss).2.symm.mono_left h.mapsTo

Goal state after: