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

Goal state before:
pp: n : Nat
hn : n >>> 1 ≠ 0
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
hn : 0 >>> 1 ≠ 0
⊢ False
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : Std.Antisymm r
a b : α
⊢ a = b → r a b ∧ r b a

Tactic:
rintro rfl

Goal state after:
α : Sort u_1
r : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : Std.Antisymm r
a : α
⊢ r a a ∧ r a a
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m * (n + 1)) = (a ^ m) ^ (n + 1)

Tactic:
rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
a : α
b : β
e : β = α
⊢ a = cast e b → a ≍ b

Tactic:
rintro rfl

Goal state after:
α β : Sort u
b : β
e : β = α
⊢ cast e b ≍ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
a : α
b : β
⊢ a ≍ b ↔ ∃ h, cast h a = b

Tactic:
simp only [heq_comm (a := a), heq_iff_exists_eq_cast, eq_comm]

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

Goal state before:
pp: case neg
γ : 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
⊢ e' (f₂₃ b) = (e' ∘ f₂₃) b

pp: case neg.hb
γ : 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
⊢ ¬∃ a, (f₂₃ ∘ f₁₂) a = f₂₃ b

Tactic:
comp_apply

Goal state after:
case neg
γ : 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
⊢ e' (f₂₃ b) = e' (f₂₃ b)

case neg.hb
γ : 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
⊢ ¬∃ a, (f₂₃ ∘ f₁₂) a = f₂₃ b
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a✝² b✝¹ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝² c
d e : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
cases hfa with

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : { a // p a } ≃ { b // q b }
⊢ (∃! a, p a) ↔ ∃! b, q b

Tactic:
simp [← unique_subtype_iff_existsUnique, unique_iff_subsingleton_and_nonempty,
        nonempty_congr e, subsingleton_congr e]

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

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
by
  rw [← not_forall_not, forall_sum]
  simp

Goal state after:
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 : α
⊢ g • g⁻¹ • a = a

Tactic:
by rw [smul_smul, mul_inv_cancel, one_smul]

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
a : α
h : Sum.map f g (inl a) = inl c
⊢ ∃ a, f a = c

pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c

Tactic:
· exact ⟨a, inl_injective h⟩

Goal state after:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
c : γ
b : β
h : Sum.map f g (inr b) = inl c
⊢ ∃ a, f a = c
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), y * x • 1 = x • y
x : M
y z : N
⊢ x • y • z = y • x • z

Tactic:
by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty γ
inst✝ : Nonempty δ
f : α → γ
g : β → δ
h : Surjective (map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
inhabit δ
      obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
      exact ⟨a, congr_arg Prod.fst h⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b = if b ≤ a then b else a

Tactic:
obtain h | h | h := lt_trichotomy a b

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ min a b = if b ≤ a then b else a

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ min a b = if b ≤ a then b else a

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ min a b = if b ≤ a then b else a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ max a b = if b ≤ a then a else b

Tactic:
obtain h | h | h := lt_trichotomy a b

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ max a b = if b ≤ a then a else b

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ max a b = if b ≤ a then a else b

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ max a b = if b ≤ a then a else b
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

Tactic:
cases n <;> simp [leRec, Or.by_cases, dif_neg]

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| leRec refl le_succ_of_le h2

Tactic:
rw [leRec, Or.by_cases, dif_pos h1]

Goal state after:
m n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
| le_succ_of_le h1 (leRec refl le_succ_of_le h1)
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b

Tactic:
obtain h | h | h := lt_trichotomy a b

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (cmp a b).Compares a b

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ (cmp a b).Compares a b

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ (cmp a b).Compares a b
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
a' : α
ha : a' ≤ a
b : β
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
induction b using WellFoundedLT.induction generalizing a' with | ind b ihb
     =>  _ 

Goal state after:
case ind.ind
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
⊢ Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b → f a = f b

Tactic:
rintro rfl

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ a ≠ b

Tactic:
rintro rfl

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a c : α
h : f a < f a ∧ f c < f a ∨ f a < f a ∧ f a < f c
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ b ≠ c

Tactic:
rintro rfl

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
h : f a < f b ∧ f b < f b ∨ f b < f a ∧ f b < f b
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n : ℕ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℕ
⊢ f a ≠ x

Tactic:
rintro rfl

Goal state after:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n a : ℕ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n : ℕ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℕ
⊢ f a ≠ x

Tactic:
rintro rfl

Goal state after:
α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n a : ℕ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False

Tactic:
exact (hf.reflect_lt h2).not_ge (Nat.le_of_lt_succ <| hf.reflect_lt h1)

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n : ℤ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℤ
⊢ f a ≠ x

Tactic:
rintro rfl

Goal state after:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n a : ℤ
h1 : f n < f a
h2 : f a < f (n + 1)
⊢ False
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x

Tactic:
rintro rfl

Goal state after:
α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n a : ℤ
h1 : f (n + 1) < f a
h2 : f a < f n
⊢ False
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
⊢ a ⊓ a ⊓ b = a ⊓ b

Tactic:
inf_idem

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
⊢ a ⊓ b = a ⊓ b
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
⊢ a ⊓ (b ⊓ b) = a ⊓ b

Tactic:
inf_idem

Goal state after:
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : Min α
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
a b : α
⊢ a ⊓ b = a ⊓ b
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ s ∩ {a | p a} = s ∩ (t ∩ {a | p a})

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
s t : Set α
p : α → Prop
hst : s ⊆ t
⊢ s ∩ {a | p a} = s ∩ t ∩ {a | p a}
Module: Mathlib.Data.Set.Insert

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

Tactic:
rintro rfl

Goal state after:
case mpr
α : Type u_1
a : α
H : [a].Nodup
⊢ {x | x ∈ [a]} = {a}
Module: Mathlib.Order.BooleanAlgebra.Defs

Goal state before:
pp: ⊢ (fun x1 x2 ↦ max x1 x2) = or

Tactic:
by dsimp

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

Goal state before:
pp: ⊢ (fun x1 x2 ↦ min x1 x2) = and

Tactic:
by dsimp

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊓ a ≤ b ↔ a ≤ b

Tactic:
inf_idem

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
inf_idem

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ b ⇨ a = b ⇨ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hinf : a ⊓ c ≤ b
hsup : b ≤ a ⊔ c
⊢ b \ c ≤ a \ c

Tactic:
simpa [sup_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⊓ a ⇨ ⊥ = a ⇨ ⊥

Tactic:
inf_idem

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇨ ⊥ = a ⇨ ⊥
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ insert a (s \ insert a t) = insert a (s \ t)

Tactic:
← union_singleton (s := t),

Goal state after:
α : Type u_1
s t : Set α
a : α
⊢ insert a (s \ (t ∪ {a})) = insert a (s \ t)
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
rw [inf_sdiff_self_right]

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

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

Tactic:
inf_idem

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

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

Tactic:
inf_idem

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
himp_eq,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ c ⊔ bᶜ ↔ a ⊓ b ≤ c
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
himp_eq,

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z

Tactic:
himp_eq,

Goal state after:
α : Type u
x y z : α
inst✝ : BooleanAlgebra α
⊢ y ⊔ xᶜ ≤ z ↔ y ≤ z ∧ Codisjoint x z
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = b ∆ a

Tactic:
by simp only [symmDiff, sup_comm]

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

Goal state before:
pp: α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
⊢ a ∈ Set.image (⇑(swap i j)) s ↔ a ∈ insert j s \ {i}

Tactic:
by
    constructor
    · rintro ⟨a, ha, rfl⟩
      obtain rfl | ne := eq_or_ne a i
      · rw [swap_apply_left]; exact ⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩
      · rw [swap_apply_of_ne_of_ne ne (ne_of_mem_of_not_mem ha hj)]; exact ⟨.inr ha, ne⟩
    · rintro ⟨rfl | has, hai⟩
      · exact ⟨i, hi, swap_apply_left ..⟩
      · exact ⟨a, has, swap_apply_of_ne_of_ne hai (ne_of_mem_of_not_mem has hj)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
by
  simp_rw [disjoint_left, mem_prod, Prod.forall]
  grind

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Surjective (codRestrict f s h) ↔ range f = s

Tactic:
simp [← range_eq_univ, Subset.antisymm_iff (a := range f), range_subset_iff, h]

Goal state after:
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
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t

Tactic:
rintro rfl

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.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
⊢ x ∈ s

Tactic:
rw [← yvaleq]

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.Image

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s ∩ (s ∩ t) = s ∩ t

Tactic:
← inter_assoc,

Goal state after:
α : Type u_1
s t : Set α
⊢ s ∩ s ∩ t = s ∩ t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
hne : (s.pi t₁).Nonempty
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i

Tactic:
simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using
    image_mono (f := fun f : ∀ i, α i => f i) h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t → SurjOn f s t ∧ MapsTo f s t

Tactic:
rintro rfl

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ s = ∅ → BijOn f s ∅

Tactic:
rintro rfl

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ t = ∅ → BijOn f ∅ t

Tactic:
rintro rfl

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅
Module: Mathlib.Algebra.Group.Hom.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)

Tactic:
exact h.surjOn_image ha.surjOn

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

Goal state before:
pp: case mp
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1

Tactic:
rintro rfl

Goal state after:
case mp
M : Type u_4
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case mpr
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1

Tactic:
rintro rfl

Goal state after:
case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Subsingleton Mˣ
⊢ a = 1 → IsUnit a

Tactic:
rintro rfl

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
⊢ IsUnit 1
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
⊢ f 1 = ↑1

Tactic:
exact f.map_one

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u : αˣ
a : α
⊢ a * ↑u = 1 ↔ a = ↑u⁻¹

Tactic:
by rw [← mul_inv_eq_one, inv_inv]

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

Goal state before:
pp: α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
rw [← mul_left_cancel_iff (a := a), ← mul_assoc, h, one_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case left
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : α
⊢ fst✝¹ i = fst✝ i

pp: case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i

Tactic:
· simpa using Equiv.congr_fun h (Sum.inl i)

Goal state after:
case right
α : Type u_7
β : Type u_8
fst✝¹ : Perm α
snd✝¹ : Perm β
fst✝ : Perm α
snd✝ : Perm β
h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)
i : β
⊢ snd✝¹ i = snd✝ i
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n : ℕ
hn : n ≠ 0
ha : a ^ n ≠ 0
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
hn : n ≠ 0
ha : 0 ^ n ≠ 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
⊢ ∃ b, a * b = 1

Tactic:
obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)

Goal state after:
case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ ∃ b, a * b = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b : G₀
h : a * b = 1
⊢ a⁻¹ = b

Tactic:
by
  rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ (g.comp f₂) x = g (f₂ x)

Tactic:
comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g : β →*₀ γ
f₁ f₂ : α →*₀ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₂ x) = g (f₂ x)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : ¬a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
exact zpow_add₀ ha m n

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x

Tactic:
by rw [smul_sub, Convex.combo_self h]

Goal state after:
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
by rw [← hn, sqrt_eq, ← Int.natCast_mul, natAbs_mul_self]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case pred
i✝ : ℕ
a✝ : IsSquare (-↑i✝).sign ↔ 0 ≤ -↑i✝
⊢ IsSquare (-↑i✝ - 1).sign ↔ 0 ≤ -↑i✝ - 1

Tactic:
rw [sign_eq_neg_one_of_neg (by lia), ← neg_add', Int.neg_nonneg]
    norm_cast
    simp only [reduceNeg, le_zero_eq, Nat.add_eq_zero_iff, succ_ne_self, and_false, iff_false]
    rintro ⟨a | a, ⟨⟩⟩

Goal state after: