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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : n ≠ 0
⊢ n = 0 → b = true

Tactic:
simp [h]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
m n : ℕ
⊢ Commute (a ^ m) (b ^ n)

Tactic:
simp [h]

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

Goal state before:
pp: case zero
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
hk : 0 ≠ 0
⊢ Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y) (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) 0
      m n =
    m * npowRec' 0 n

Tactic:
simp at hk

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
a' : α
⊢ ∃! a, a' = a

Tactic:
simp only [ExistsUnique, and_self, forall_eq', exists_eq']

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ (f a == f b) = (a == b)

Tactic:
simp [h]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ f a = f b
Module: Mathlib.Logic.Function.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ (f a == f b) = (a == b)

Tactic:
simp [h]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ ¬f a = f b
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y

pp: case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y

Tactic:
· exact ⟨x₁, (hf.ne_iff' h).2 hx⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
A : Prop
B : A → Prop
h : A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
A : Prop
B : A → Prop
h : ¬A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : ¬P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : P
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : ¬P
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
h : ¬p
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
h : ¬p
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
simp [h]

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' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
extend_apply' _ _ _ h₃,

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' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = e' a
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ ⇑e = id

Tactic:
rw [Perm.subsingleton_eq_refl e, coe_refl]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∀ (b : β), p (e.symm b)) ↔ ∀ (b : β), q b

Tactic:
simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
simp [h]

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

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun b x ↦ f b) a l = f^[l.length] a

Tactic:
by
  induction l generalizing a with
  | nil => rfl
  | cons b l H => rw [length_cons, foldl, iterate_succ_apply, H]

Goal state after:
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
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = MulOpposite.unop m • n • a

Tactic:
← unop_smul_eq_smul m n,

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
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (MulOpposite.unop m • n) • a = MulOpposite.unop m • n • a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ b

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ b

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
· have : ¬ f a = f b := by rename_i h; exact inj.ne h
    contradiction

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: case inl
n m : ℕ
h : n ≤ m
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
simp [h]

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

Goal state before:
pp: case inl
n m : ℕ
h : m ≤ n
⊢ n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: o o' : Ordering
⊢ o.swap.swap = o'.swap ↔ o = o'.swap

Tactic:
swap_swap

Goal state after:
o o' : Ordering
⊢ o = o'.swap ↔ o = o'.swap
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
⊢ (if (fun x1 x2 ↦ x1 < x2) a b then lt else if (fun x1 x2 ↦ x1 < x2) b a then gt else eq).swap =
    if (fun x1 x2 ↦ x1 < x2) b a then lt else if (fun x1 x2 ↦ x1 < x2) a b then gt else eq

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

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case inr.inl
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
hab : r a b
hbc : r b a
⊢ r a a

pp: case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c

Tactic:
· exact asymm_of r hab hbc |>.elim

Goal state after:
case inr.inr
α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
hca : r c a
⊢ r a c
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case pos
p q : Prop
h : q
⊢ p ≤ q ∨ q ≤ p

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case neg
p q : Prop
h : ¬q
⊢ p ≤ q ∨ q ≤ p

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
h : r = ⊤
⊢ ∀ (a : α), r a a

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
h : r = ⊥
⊢ ∀ (a : α), ¬r a a

Tactic:
simp [h]

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

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

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

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint {a} s

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : b = x
⊢ (fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) ((fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) b) = b

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
x : β
e : α ≃ { y // y ≠ x }
b : β
h : ¬b = x
⊢ (fun a ↦ a.casesOn' x (Subtype.val ∘ ⇑e)) ((fun b ↦ if h : b = x then none else some (e.symm ⟨b, h⟩)) b) = b

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y < x ↔ ¬Disjoint y x

Tactic:
lt_iff_le_and_ne,

Goal state after:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ≤ x ∧ x \ y ≠ x ↔ ¬Disjoint y x
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
h : p x
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x

Tactic:
simp [h]

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

Goal state before:
pp: case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
x : ε
h : ¬p x
⊢ (subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a })) x = (Equiv.refl ε) x

Tactic:
simp [h]

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

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
x : α
⊢ f x = g x

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ (∀ ⦃a : α × β⦄, a.1 ∈ s₁ ∧ a.2 ∈ t₁ → ¬(a.1 ∈ s₂ ∧ a.2 ∈ t₂)) ↔
    (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂

Tactic:
Prod.forall

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ (∀ (a : α) (b : β), a ∈ s₁ ∧ b ∈ t₁ → ¬(a ∈ s₂ ∧ b ∈ t₂)) ↔
    (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁

Tactic:
intro heq
    have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
    rw [prod_nonempty_iff] at h h₁
    rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ x ∈ s ∧ f x = s.piecewise f g x

Tactic:
simp [h]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ x ∈ sᶜ ∧ g x = s.piecewise f g x

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t

Tactic:
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none

Tactic:
refine
    ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ (Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : insert (f a) (f '' s) \ {f a} = insert (f a) t \ {f a}
⊢ BijOn f s t

Tactic:
simp only [mem_singleton_iff, insert_sdiff_of_mem] at this

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t \ {f a}
⊢ BijOn f s t
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
simp [h]

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

Goal state before:
pp: case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then a * b else 1) = (if P then a else 1) * if P then b else 1

Tactic:
simp [h]

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

Goal state before:
pp: case pos
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
simp [h]

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

Goal state before:
pp: case neg
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
h : ¬P
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : b = a * c
⊢ a⁻¹ * b = c

Tactic:
simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c

Tactic:
simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b⁻¹
⊢ a * b = c

Tactic:
simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a / b = c

Tactic:
simp [h]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a = c / b
⊢ a * b = c

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ a * (1 / a) = 1

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a : α
h : IsUnit a
⊢ 1 / a * a = 1

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b

Tactic:
simp only [div_eq_mul_inv]
  exact Units.mul_left_inj h.inv.unit'

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
b a : α
h : IsUnit b
⊢ a * b * (1 / b) = a

Tactic:
simp [h]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : Group G
inst✝ : Group H
x✝ : G × H
⊢ x✝⁻¹ * x✝ = 1

Tactic:
by ext <;> exact inv_mul_cancel _

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ a⁻¹ * a * a⁻¹ * a⁻¹⁻¹ = a⁻¹ * a⁻¹⁻¹

Tactic:
simp [h]

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

Goal state before:
pp: G₀ : Type u
inst✝ : GroupWithZero G₀
b : G₀
h : b ≠ 0
a : G₀
⊢ a * (b * b⁻¹) = a

Tactic:
simp [h]

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

Goal state before:
pp: G₀ : Type u
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
b : G₀
⊢ a * a⁻¹ * b = b

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

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

Tactic:
simp [h]

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

Goal state before:
pp: case pos
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b x a : G₀
h : a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M₂ →+ M
hf : Injective ⇑f
smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x
x : M₂
⊢ f (0 • x) = f 0

Tactic:
simp only [smul, zero_smul, f.map_zero]

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

Goal state before:
pp: n : ℕ
⊢ n % 2 = 0 ↔ Even n

Tactic:
Nat.even_iff

Goal state after:
n : ℕ
⊢ n % 2 = 0 ↔ n % 2 = 0
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a + 1 = a
⊢ a + 1 = a + 0

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ -a⁻¹ = (-a)⁻¹

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
b a : G₀
h : b ≠ 0
⊢ a / b * b = a

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a x y : α
h : SemiconjBy a x y
m n : ℕ
⊢ SemiconjBy (↑m * a) (↑n * x) (↑n * y)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a b : α
h : Commute a b
m n : ℕ
⊢ Commute (↑m * a) (↑n * b)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ n * a = 0 ↔ a = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ n * a = 0 ↔ a = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = 1
⊢ a * (-1) ^ n = 0 ↔ a = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: case inr
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = -1
⊢ a * (-1) ^ n = 0 ↔ a = 0

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
a x y : α
h : SemiconjBy a x y
m n : ℤ
⊢ SemiconjBy (↑m * a) (↑n * x) (↑n * y)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
a b : α
h : Commute a b
m : ℤ
⊢ Commute a (↑m * b)

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝ : Ring α
a b : α
h : Commute a b
m : ℤ
⊢ Commute (↑m * a) b

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a - c + (b + c)

Tactic:
add_comm a,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a ≤ a - c + (b + c)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + (b - d) - c ≤ a - c + (b - d)

Tactic:
add_comm a,

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ b - d + a - c ≤ a - c + (b - d)