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

Goal state before:
pp: G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)

Tactic:
rw [← natCast_zsmul]
  exact SubNegMonoid.zsmul_neg' n a

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

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

Tactic:
by_cases h : f x₂ = y

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

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: α β : Sort u
e : β = α
a : α
b : β
h : a ≍ b
⊢ a = cast e b

Tactic:
cases h

Goal state after:
case refl
α : Sort u
a : α
e : α = α
⊢ a = cast e a
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
h : ∀ (x y : α), (x == y) = (x == y)
⊢ inst1 = inst2

Tactic:
have ⟨beq1⟩ := inst1
  congr
  funext x y
  exact h x y

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a ↦ p a) a
he : ∀ (y : α), (fun a ↦ p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ b = a

Tactic:
exact he b hb

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

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective h.mp

Tactic:
cases h

Goal state after:
case refl
α : Sort u_3
⊢ Bijective ⋯.mp
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective h.mpr

Tactic:
cases h

Goal state after:
case refl
α : Sort u_3
⊢ Bijective ⋯.mpr
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α β : Sort u_3
h : α = β
⊢ Bijective (cast h)

Tactic:
cases h

Goal state after:
case refl
α : Sort u_3
⊢ Bijective (cast ⋯)
Module: Mathlib.Data.FunLike.Basic

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f = g
⊢ ⇑f = ⇑g

Tactic:
cases h

Goal state after:
case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f : F
⊢ ⇑f = ⇑f
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.succ] x = x

Tactic:
iterate_succ_apply,

Goal state after:
α : Type u
f : α → α
x : α
h : f x = x
n✝ n : ℕ
ihn : f^[n] x = x
⊢ f^[n] (f x) = x
Module: Mathlib.Logic.Function.Iterate

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

Tactic:
iterate_succ_apply,

Goal state after:
case cons
α : Type u
β : Type v
f : α → α
b : β
l : List β
H : ∀ (a : α), foldl (fun b x ↦ f b) a l = f^[l.length] a
a : α
⊢ foldl (fun b x ↦ f b) (f a) l = f^[l.length] (f a)
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x y : α ⊕ β
h : x = y
⊢ rec f g x = cast ⋯ (rec f g y)

Tactic:
cases h

Goal state after:
case refl
α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x : α ⊕ β
⊢ rec f g x = cast ⋯ (rec f g x)
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isLeft = true ↔ y.isLeft = true

Tactic:
cases h

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isLeft = true ↔ (inl c✝).isLeft = true

case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isLeft = true ↔ (inr d✝).isLeft = true
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✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ s • r • 1 • x = s • r • x

Tactic:
one_smul

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✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ s • r • x = s • r • x
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isRight = true ↔ y.isRight = true

Tactic:
cases h

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isRight = true ↔ (inl c✝).isRight = true

case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isRight = true ↔ (inr d✝).isRight = true
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
c : γ
h : LiftRel r s x (inl c)
⊢ x.isLeft = true

Tactic:
cases h

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
c : γ
a✝¹ : α
a✝ : r a✝¹ c
⊢ (inl a✝¹).isLeft = true
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
a : α
h : LiftRel r s (inl a) y
⊢ y.isLeft = true

Tactic:
cases h

Goal state after:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a : α
c✝ : γ
a✝ : r a c✝
⊢ (inl c✝).isLeft = true
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
d : δ
h : LiftRel r s x (inr d)
⊢ x.isRight = true

Tactic:
cases h

Goal state after:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
d : δ
b✝ : β
a✝ : s b✝ d
⊢ (inr b✝).isRight = true
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 : α
⊢ 1 • a = a

Tactic:
one_smul

Goal state after:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ a = a
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
b : β
h : LiftRel r s (inr b) y
⊢ y.isRight = true

Tactic:
cases h

Goal state after:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b : β
d✝ : δ
a✝ : s b d✝
⊢ (inr d✝).isRight = true
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ 1 • 1 = 1

Tactic:
one_smul

Goal state after:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ 1 = 1
Module: Mathlib.Data.Sum.Basic

Goal state before:
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:
cases h

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)
d : δ
a : α
h : Sum.map f g (inl a) = inr d
⊢ ∃ a, g a = d

Tactic:
cases h

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

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • r • 1 • x = s • r • 1 • x

Tactic:
one_smul

Goal state after:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ s • r • x = s • r • x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
M : Type u_9
N : Type u_10
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ x • 1 • y = x • y

Tactic:
one_smul

Goal state after:
α : Type u_5
M : Type u_9
N : Type u_10
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ x • y = x • y
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Type u_5
E : α → Type u_4
⊢ IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)

Tactic:
simp only [← not_nonempty_iff, nonempty_sigma, not_exists]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : One γ
i : α
c : γ
⊢ Sum.elim (Pi.mulSingle i c) 1 = Pi.mulSingle (inl i) c

Tactic:
simp only [Pi.mulSingle, Sum.elim_update_left, elim_one_one]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
x₂ : α
y₂ : β
h : (x₁, y₁) = (x₂, y₂)
P : Sort u_5
w : x₁ = x₂ → y₁ = y₂ → P
⊢ P

Tactic:
cases h

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
P : Sort u_5
w : x₁ = x₁ → y₁ = y₁ → P
⊢ P
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: α α' : Sort u
β β' : Sort v
h : α = α'
h' : ∀ (a : α'), β = β'
⊢ (α → β) = (α' → β')

Tactic:
cases h

Goal state after:
case refl
α : Sort u
β β' : Sort v
h' : ∀ (a : α), β = β'
⊢ (α → β) = (α → β')
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a * b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
Int.mul_ne_zero_iff

Goal state after:
a b : ℤ
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∧ a ≠ 0 ∧ b ≠ 0 ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Module: Mathlib.Data.Int.Order.Basic

Goal state before:
pp: a b : ℤ
⊢ a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [← not_iff_not, not_le, Int.mul_pos_iff]
  lia

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : a < b
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.lt a b := hab

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : a < b
hab : lt.Compares a b
⊢ o.Compares a b
Module: Mathlib.Order.RelClasses

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

Tactic:
induction a using WellFoundedLT.induction generalizing a' b with | ind a iha

Goal state after:
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)
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
a✝ b x a : α
⊢ a ∈ insert x ∅ ↔ a ∈ {x}

Tactic:
simp only [mem_empty_iff_false, mem_insert_iff, or_false]

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
a✝ b x a : α
⊢ a = x ↔ a ∈ {x}
Module: Mathlib.Order.Lattice

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Lattice α
a b c : α
h : a ⊓ b = c ∧ a ⊔ b = c
⊢ a = c ∧ b = c

Tactic:
obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
    simpa using h

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

Goal state before:
pp: α : Type u
a : α
s✝ t : Set α
inst✝ : Subsingleton α
s : Set α
⊢ Subsingleton ↑s

Tactic:
by
  rw [s.subsingleton_coe]
  exact subsingleton_of_subsingleton

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

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

Tactic:
← @sup_sdiff_left_self _ _ _ b

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)

Tactic:
tauto

Goal state after:
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
a✝ : α
x✝ : { s // s.fst = a✝ }
a : Sigma β
h : a.fst = a✝
⊢ (fun b ↦ ⟨⟨a✝, b⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
        ⟨a, h⟩) =
    ⟨a, h⟩

Tactic:
cases h

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: α : 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 : Quotient s₂
⊢ (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:
induction a using Quotient.inductionOn; rfl

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:
rw [inf_comm, inf_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ sᶜ → s.piecewise f g x ≠ s.piecewise f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ (x : α), x ∈ s → ∀ (y : α), ¬y ∈ s → f x ≠ g y

Tactic:
refine and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ s.piecewise f g x ≠ s.piecewise f g y ↔ f x ≠ g y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
s t : Set α
x : α × α
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2

Tactic:
tauto

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

Goal state before:
pp: α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set ↑t), p (val '' s)) ↔ ∀ (s : Set α), s ⊆ t → p s

Tactic:
← forall_subset_range_iff,

Goal state after:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set α), s ⊆ range val → p s) ↔ ∀ (s : Set α), s ⊆ t → p s
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: F : 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
inst✝¹ : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst✝ : (i : ι) → Mul (M i)
i j : ι
h : i = j
x✝¹ x✝ : M i
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝

Tactic:
cases h

Goal state after:
case refl
F : 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
inst✝¹ : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst✝ : (i : ι) → Mul (M i)
i : ι
x✝¹ x✝ : M i
__Equiv✝ : M i ≃ M i := Equiv.cast ⋯
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ SurjOn (g ∘ f) s (g '' t)

Tactic:
rw [SurjOn, image_comp g f]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Tactic:
rw [invFunOn, dif_pos h]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst✝ : Nonempty α
h : ∃ a, a ∈ s ∧ f a = b
⊢ Classical.choose h ∈ s ∧ f (Classical.choose h) = b
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a' h

Tactic:
cases h

Goal state after:
case refl
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a ⋯
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ ≍ f a' h

Tactic:
cases h

Goal state after:
case refl
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ ≍ f a ⋯
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
h : a ≍ a'
⊢ a = a'

Tactic:
cases h

Goal state after:
case refl
α : Sort u
a : α
⊢ a = a
Module: Mathlib.Tactic.DepRewrite

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

Tactic:
cases h

Goal state after:
case refl
α : Sort u
a : α
⊢ a = cast ⋯ a
Module: Mathlib.Tactic.DepRewrite

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

Tactic:
cases h

Goal state after:
case refl
α : Sort u
a : α
⊢ cast ⋯ a = a
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a + b ≤ c ↔ b < c

Tactic:
rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ u, r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
    (image_mono hrs) Subset.rfl
  exact ⟨u, hru, hus, h.image_eq, h.injOn⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b c d : α
⊢ (a / b)⁻¹ = (c / d)⁻¹ ↔ b / a = d / c

Tactic:
simp only [inv_div]

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

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

Tactic:
by
  rw [mul_assoc, inv_mul, mul_one]

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

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

Tactic:
rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]

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

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

Tactic:
rw [mul_comm, h.mul_div_cancel_right]

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n✝ m✝ : ℕ
hmn : n✝.le m✝
ha : a ^ n✝ = 0
⊢ a ^ m✝ * a = 0

Tactic:
pow_eq_zero_of_le hmn ha,

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n✝ m✝ : ℕ
hmn : n✝.le m✝
ha : a ^ n✝ = 0
⊢ 0 * a = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case inr.inr
G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ 1 • 1 = 1

Tactic:
one_smul

Goal state after:
case inr.inr
G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ 1 = 1
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1

Tactic:
cases h

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

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

Tactic:
one_smul

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
h : a + b = 1
x : M
⊢ x = x
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ 1 • x + 1 • x = x + x

Tactic:
one_smul

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ x + x = x + x
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ 1 • m = m

Tactic:
one_smul

Goal state after:
M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ m = m