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

Goal state before:
pp: n : Nat
n0 : ¬n = 0
⊢ (if n >>> 1 = 0 then 0 else (n >>> 1).log2.succ) < if n = 0 then 0 else n.log2.succ

Tactic:
obtain _ | n := n

Goal state after:
case zero
n0 : ¬0 = 0
⊢ (if 0 >>> 1 = 0 then 0 else (0 >>> 1).log2.succ) < if 0 = 0 then 0 else (log2 0).succ

case succ
n : Nat
n0 : ¬n + 1 = 0
⊢ (if (n + 1) >>> 1 = 0 then 0 else ((n + 1) >>> 1).log2.succ) < if n + 1 = 0 then 0 else (n + 1).log2.succ
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ
n : Nat
n0 : ¬n + 1 = 0
⊢ (if (n + 1) >>> 1 = 0 then 0 else ((n + 1) >>> 1).log2.succ) < if n + 1 = 0 then 0 else (n + 1).log2.succ

Tactic:
obtain _ | n := n

Goal state after:
case succ.zero
n0 : ¬0 + 1 = 0
⊢ (if (0 + 1) >>> 1 = 0 then 0 else ((0 + 1) >>> 1).log2.succ) < if 0 + 1 = 0 then 0 else (0 + 1).log2.succ

case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ
Module: Mathlib.Data.Nat.BinaryRec

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

Tactic:
rw [bit_eq_zero_iff]
        cases n <;> cases b <;> simp at h ⊢

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

Goal state before:
pp: M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (m + n) a = npowRec m a * npowRec n a

Tactic:
obtain _ | n := n

Goal state after:
case zero
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
hn : 0 ≠ 0
⊢ npowRec (m + 0) a = npowRec m a * npowRec 0 a

case succ
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
m : ℕ
a : M
ha : 1 * a = a
n : ℕ
hn : n + 1 ≠ 0
⊢ npowRec (m + (n + 1)) a = npowRec m a * npowRec (n + 1) a
Module: Mathlib.Logic.Basic

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

Tactic:
by rintro ⟨rfl, h⟩; rw [h, cast_eq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
let ⟨a⟩ := ha

Goal state after:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
⊢ B.SeparatesPoints

Tactic:
intro x y hne
  obtain ⟨f, hfA, hne'⟩ := hA hne
  exact ⟨f, hAB hfA, hne'⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
b : β
f : α → β
a : Option α
⊢ a.casesOn' b f = a.elim b f

Tactic:
by cases a <;> rfl

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₂ : β
⊢ (x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_5⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P

Tactic:
intros h P w

Goal state after:
α : 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
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (if a ≤ b then a else b)

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
h : a ≤ b
⊢ motive a

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
h : ¬a ≤ b
⊢ motive b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
⊢ motive (if a ≤ b then b else a)

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
h : a ≤ b
⊢ motive b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
h : ¬a ≤ b
⊢ motive a
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
split_ifs with h

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

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ a
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
split_ifs with h

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

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ b
Module: Mathlib.Order.Defs.LinearOrder

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

Tactic:
· exact compare_gt_iff_gt

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), NoMinOrder (π i)
a : (i : ι) → π i
⊢ ∃ b, b < a

Tactic:
obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
    exact ⟨_, update_lt_self_iff.2 hb⟩

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
simpa [hx, hy] using hf h

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
exact h.inf_left_eq_bot_iff

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

Goal state before:
pp: ⊢ Monotone fun n ↦ n ^ n

Tactic:
refine monotone_nat_of_le_succ fun n ↦ ?_
  rw [Nat.pow_succ]
  exact (Nat.pow_le_pow_left n.le_succ _).trans (Nat.le_mul_of_pos_right _ n.succ_pos)

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c

Tactic:
H,

Goal state after:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
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
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
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
⊢ a ⊔ b = b

Tactic:
by rw [← h, sup_comm, sup_inf_self]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ Subsingleton ↑s ↔ s.Subsingleton

Tactic:
constructor
  · intro h a ha b hb
    exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)
  · exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)

Goal state after:
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α : Type u₀
x✝ : f α
⊢ (mapEquiv f (Equiv.refl α)) x✝ = (Equiv.refl (f α)) x✝

Tactic:
simp [mapEquiv]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
⊢ (a ≤ if b ≤ c then ⊤ else c) ↔ min a b ≤ c

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : b ≤ c
⊢ a ≤ ⊤ ↔ min a b ≤ c

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ min a b ≤ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
⊢ (if a ≤ b then ⊥ else a) ≤ c ↔ a ≤ max b c

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : a ≤ b
⊢ ⊥ ≤ c ↔ a ≤ max b c

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ max b c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
⊢ f (a \ b) ≤ f c ↔ f a ≤ f (b ⊔ c)

Tactic:
map_sdiff,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b c : α
⊢ f a \ f b ≤ f c ↔ f a ≤ f (b ⊔ c)
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.12
β : Option α → Type u_9
f : (a : Option α) → β a
a : Option α
⊢ (fun x a ↦ Option.casesOn a x.fst x.snd) ((fun f ↦ (f none, fun a ↦ f (some a))) f) a = f a

Tactic:
by cases a <;> rfl

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

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

Tactic:
have h := compl_le_compl h; simpa using h

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f (a ⊓ b) ⊔ f (a \ b) = f a

Tactic:
map_sdiff,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f (a ⊓ b) ⊔ f a \ f b = f a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f (a ⊓ b) ⊓ f (a \ b) = f ⊥

Tactic:
map_sdiff,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedBooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a b : α
⊢ f (a ⊓ b) ⊓ f a \ f b = f ⊥
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (b : β) → P (e.symm b)
b : β
x : P (e.symm b)
⊢ (Equiv.piCongrLeft' P e).symm (update f b x) = update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x

Tactic:
by
  simp [(e.piCongrLeft' P).symm_apply_eq, piCongrLeft'_update]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ g ⁻¹' s ↔ g b ∈ s

Tactic:
mem_preimage

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ g b ∈ s ↔ g b ∈ s
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
⊢ (if h : ∃ a, f a = y then g (Classical.choose h) else g' y) ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ a, f a = y
⊢ g (Classical.choose h) ∈ range g ∪ g' '' (range f)ᶜ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ a, f a = y
⊢ g' y ∈ range g ∪ g' '' (range f)ᶜ
Module: Mathlib.Data.Set.Image

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

Tactic:
← preimage_image_eq s hf,

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ f ⁻¹' f '' s = t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ (m₁ '' s) ×ˢ (m₂ '' t) ↔ x ∈ (fun p ↦ (m₁ p.1, m₂ p.2)) '' s ×ˢ t

Tactic:
simp [-exists_and_right, exists_and_right.symm, and_left_comm, and_assoc, and_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : g x = extend f g j (f y)
⊢ f x = f y

Tactic:
hf.extend_apply

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
j : β → γ
hf : FactorsThrough g f
hg : Injective g
x y : α
heq : g x = g y
⊢ f x = f y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Tactic:
simp_rw [prod_eq_prod_iff, ht.ne_empty, and_true, or_iff_left_iff_imp, or_false]

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = ∅ ∧ s₁ = ∅ → s = s₁
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:
← preimage_image_eq s hf,

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

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

Tactic:
coe_injective.image_injective.eq_iff

Goal state after:
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t = val ⁻¹' u ↔ val ⁻¹' t = val ⁻¹' u
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : ∀ (x : β × γ), x ∈ range f ↔ x ∈ graphOn e₁ univ
e₂ : γ → β
he₂ : ∀ (x : γ × β), x ∈ range (⇑(Equiv.prodComm β γ) ∘ f) ↔ x ∈ graphOn e₂ univ
h : β
i : γ
⊢ e₁ h = i ↔ e₂ i = h

Tactic:
aesop (add simp [Prod.swap_eq_iff_eq_swap])

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s', s' ⊆ s ∧ BijOn f s' t

pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (∃ s', s' ⊆ s ∧ BijOn f s' t) → SurjOn f s t

Tactic:
· rcases eq_empty_or_nonempty t with (rfl | ht)
    · exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩
    · intro h
      have : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
      exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (∃ s', s' ⊆ s ∧ BijOn f s' t) → SurjOn f s t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : 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)
⊢ MapsTo f (s ∪ r) t'

Tactic:
mapsTo_iff_image_subset,

Goal state after:
case refine_2
α : 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)
⊢ f '' (s ∪ r) ⊆ t'
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsRightCancelMul M
a b : M
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
by rw [one_mul]

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

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

Tactic:
eq_mul_inv_iff_mul_eq

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a * c = b ↔ a * c = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c d : G
H : a / b = c / d
⊢ a / b = 1 ↔ c = d

Tactic:
H,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c d : G
H : a / b = c / d
⊢ c / d = 1 ↔ c = d
Module: Mathlib.Algebra.Group.Units.Basic

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

Tactic:
by rw [one_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
by rw [one_mul]

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

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

Tactic:
h.mul_inv_eq_iff_eq_mul

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit b
⊢ a = c * b ↔ a = c * b
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✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M × N
⊢ x✝ * 1 = x✝

Tactic:
ext <;> exact mul_one _

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✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (fst✝ * g₁, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
mul_comm h₁

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)
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✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (fst✝ * g₁, h₁ * snd✝) = (fst✝ * g₁, snd✝ * h₁)

Tactic:
mul_comm h₁

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (fst✝ * g₁, snd✝ * h₁) = (fst✝ * g₁, snd✝ * h₁)
Module: Mathlib.Algebra.GroupWithZero.NeZero

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = 1 * x

Tactic:
by rw [one_mul]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * y = y

Tactic:
by rw [one_mul]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ f (a * b) = 0

Tactic:
H,

Goal state after:
M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a b : M₀
H : a * b = 0
⊢ f 0 = 0
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: case neg
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
f : Perm α
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
x : α
hx : ¬p x
⊢ (ofSubtype (f.subtypePerm h₁)) x = f x

Tactic:
· rw [ofSubtype, MonoidHom.coe_mk, OneHom.coe_mk,
        Equiv.Perm.extendDomain_apply_not_subtype _ _ hx]
      exact not_not.mp fun h => hx (h₂ x (Ne.symm h))

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : n = 0
⊢ 0 ^ n = 1

case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
a b : M₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : IsRightCancelMulZero M₀
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
by rw [one_mul]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 0 else 1) = if p then 0 else 1

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 0 = 0

case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 1 = 1
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 1 else 0) = if p then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : p
⊢ f 1 = 1

case neg
α : Type u_2
β : Type u_3
inst✝⁴ : MulZeroOneClass α
inst✝³ : MulZeroOneClass β
F : Type u_7
inst✝² : FunLike F α β
inst✝¹ : MonoidWithZeroHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ f 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1

case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝ : NonAssocSemiring α
n : α
⊢ 1 * n + 1 * n = n + n

Tactic:
by rw [one_mul]

Goal state after: