mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
a b c : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b c) = true → Decidable.decide (r a c) = true

Tactic:
by simpa using trans a b c

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

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

Tactic:
exact ⟨refl _, refl _⟩

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

Goal state before:
pp: case bit
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
b : Bool
k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 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)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit b k' ≠ 0
⊢ (bif b then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit b k') n

Tactic:
cases b <;> simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]

Goal state after:
case bit.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 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)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ m * n * npowRec' k' (n * n) = m * npowRec' (2 * k' + 1) n
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ 1 =
    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 1 m

Tactic:
Nat.binaryRec_zero

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ 1 = 1
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₂ : ∃! x, ∃! h, q x h
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
⊢ b

Tactic:
simp only [existsUnique_iff_exists] at h₂

Goal state after:
α : Sort u_1
p : α → Sort u_2
inst✝ : ∀ (x : α), Subsingleton (p x)
q : (x : α) → p x → Prop
b : Prop
h₁ : ∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b
h₂ : ∃! x, ∃ h, q x h
⊢ b
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * b * a = b

Tactic:
mul_comm,

Goal state after:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a * (a⁻¹ * b) = b
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a * b * a⁻¹ = b

Tactic:
mul_comm,

Goal state after:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (a * b) = b
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (b * a) = b

Tactic:
mul_comm,

Goal state after:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ b * a * a⁻¹ = b
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a * (b * a⁻¹) = b

Tactic:
mul_comm,

Goal state after:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ b * a⁻¹ * a = b
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ (a ∧ ¬a ∨ a ∧ ¬b) ∨ b ∧ (¬a ∨ ¬b)

Tactic:
and_not_self_iff,

Goal state after:
a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ (False ∨ a ∧ ¬b) ∨ b ∧ (¬a ∨ ¬b)
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ b ∧ ¬b

Tactic:
and_not_self_iff,

Goal state after:
a b : Prop
⊢ a ∧ ¬b ∨ b ∧ ¬a ↔ a ∧ ¬b ∨ b ∧ ¬a ∨ False
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂

Tactic:
← comp_assoc,

Goal state after:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ (g₁ ∘ f) ∘ g₂ = g₂
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ g x = f x

Tactic:
← h x,

Goal state after:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ g (f (f x)) = f (f (f x))
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ g ∘ f^[m] ∘ f = g

Tactic:
← comp_assoc,

Goal state after:
α : Type u
β : Type v
f : α → α
g : α → β
h : g ∘ f = g
n m : ℕ
⊢ (g ∘ f^[m]) ∘ f = g
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ (Equiv.refl α).trans e = e

Tactic:
cases e; rfl

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
M : Type u_9
α : Type u_10
inst✝¹ : CommMonoid M
inst✝ : MulAction M α
a a' : M
b : α
⊢ (a * a') • b = a' • a • b

Tactic:
mul_comm,

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
M : Type u_9
α : Type u_10
inst✝¹ : CommMonoid M
inst✝ : MulAction M α
a a' : M
b : α
⊢ (a' * a) • b = a' • a • b
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 N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • n • a = MulOpposite.unop n • m • a

Tactic:
← unop_smul_eq_smul n a,

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

Tactic:
← unop_smul_eq_smul n a,

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 N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ (m • n) • a = m • MulOpposite.unop n • a
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
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
⊢ ∀ (x y : M) (b : β), (x * y) • b = x • y • b

Tactic:
simp [hf.forall, ← smul, mul_smul]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update (f ∘ inr) i x j

Tactic:
by
  rw [← update_inr_comp_inr, Function.comp_apply]

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

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • y * z = x₁ • y • z

Tactic:
mul_comm,

Goal state after:
R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ z * x₁ • y = x₁ • y • z
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • (z * y) = x₁ • y • z

Tactic:
mul_comm,

Goal state after:
R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • (y * z) = x₁ • y • z
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty β
⊢ RightTotal R

Tactic:
simp only [RightTotal, IsEmpty.forall_iff]

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a b : αᵒᵈ
⊢ compare a b = compareOfLessAndEq a b

Tactic:
simp only [compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, eq_comm]

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a b : αᵒᵈ
⊢ (if b < a then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : eq.Compares a b
h : eq = lt
⊢ a < b

Tactic:
by injection h

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : gt.Compares a b
h : gt = lt
⊢ a < b

Tactic:
by injection h

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝² x✝¹ : α
h✝ : eq.Compares x✝² x✝¹
x✝ : x✝¹ ≤ x✝²
h : eq = lt
⊢ False

Tactic:
by injection h

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x✝² x✝¹ : α
h✝ : gt.Compares x✝² x✝¹
x✝ : x✝¹ ≤ x✝²
h : gt = lt
⊢ False

Tactic:
by injection h

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : lt.Compares a b
h : lt = eq
⊢ a = b

Tactic:
by injection h

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h✝ : gt.Compares a b
h : gt = eq
⊢ a = b

Tactic:
by injection h

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

Goal state before:
pp: case succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + (↑(n + 1) + 1)))

Tactic:
← Int.add_assoc

Goal state after:
case succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1) + 1))
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
c b a : α
hbc : b ⊓ c = c
hab : a ⊓ b = b
⊢ a ⊓ c = c

Tactic:
rw [← hbc, ← inf_assoc, hab]

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

Goal state before:
pp: case ind
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {f : ℕ → ℕ},
        Antitone f →
          (∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)) → f 0 = m → ∃ n, n ≤ m ∧ ∀ (m : ℕ), n ≤ m → f m = f n
f : ℕ → ℕ
hfmono : Antitone f
hfstab : ∀ (m : ℕ), f m = f (m + 1) → f (m + 1) = f (m + 2)
h : f 0 = n
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
| ind n ih =>

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s = ∅ ∧ s ≠ {x} ∨ s = {x} ∧ s ≠ {x} ↔ s = ∅

Tactic:
and_not_self_iff,

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ s = ∅ ∧ s ≠ {x} ∨ False ↔ s = ∅
Module: Mathlib.Data.Set.Insert

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

Tactic:
by simp [Set.disjoint_iff, subset_def]

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

Goal state before:
pp: α : Type u
s : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False

Tactic:
exact hxy rfl

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
⊢ Preorder α

Tactic:
let lt := e.lt

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : Preorder β
le : LE α := e.le
lt : LT α := e.lt
⊢ Preorder α
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
⊢ LinearOrder α

Tactic:
let max := e.max

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝¹ : LinearOrder β
inst✝ : DecidableEq α
max : Max α := e.max
⊢ LinearOrder α
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
⊢ SemilatticeSup α

Tactic:
let max := e.max

Goal state after:
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemilatticeSup β
max : Max α := e.max
⊢ SemilatticeSup α
Module: Mathlib.Logic.Equiv.Option

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

Tactic:
| none =>

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

Goal state before:
pp: case some
α✝ : 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
p : Option α → Type v
h : ∀ (a : p none), False
val✝ : α
⊢ ∀ (a : p (some val✝)), (some val✝).isSome = true

Tactic:
intro _
      exact rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a

Tactic:
· rw [sup_assoc]
    exact le_sup_of_le_right le_sdiff_sup

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Tactic:
· have : ∀ x b, f x ≠ b := fun x b ↦
      eq_empty_iff_forall_notMem.1 ((hf b).resolve_right fun h ↦ hf' ⟨b, h⟩) x
    exact ⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩

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

Goal state before:
pp: case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u → ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ

Tactic:
intro x_in_u

Goal state after:
case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
⊢ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = (fun a ↦ f ↑a) ⁻¹' Subtype.val '' u

Tactic:
← preimage_preimage (g := f) (f := Subtype.val),

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = Subtype.val ⁻¹' f ⁻¹' Subtype.val '' u
Module: Mathlib.Data.Set.Restrict

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ f a ∈ f '' s

Tactic:
exact mem_image_of_mem f ha

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ {i | i ∈ s ∧ p i}.pi t₁
ht₂ : f ∈ {i | i ∈ s ∧ ¬p i}.pi t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i

Tactic:
by_cases p i <;> simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ Disjoint (f '' (s \ t)) (f '' (s ∩ t))

Tactic:
exact Disjoint.image disjoint_sdiff_inter h sdiff_subset inter_subset_left

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f (1 * 1) = 1 * f 1

Tactic:
one_mul,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Group G
inst✝ : MulOneClass M
f : M → G
map_mul : ∀ (a b : M), f (a * b) = f a * f b
⊢ f 1 = 1 * f 1
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N✝ : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : LeftCancelMonoid N
f : M →ₙ* N
⊢ f 1 * 1 = f 1 * f 1

Tactic:
simpa using f.map_mul' 1 1

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N✝ : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : RightCancelMonoid N
f : M →ₙ* N
⊢ 1 * f 1 = f 1 * f 1

Tactic:
simpa using f.map_mul' 1 1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ LeftInvOn (invFunOn f s) f (invFunOn f s '' t)

Tactic:
rintro _ ⟨y, hy, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
⊢ MapsTo f (invFunOn f s '' t) t

Tactic:
rintro _ ⟨y, hy, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst✝ : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ f (invFunOn f s y) ∈ t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_1
α : 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)
⊢ s ∪ r ⊆ s₁

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'

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

pp: case refine_4
α : 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)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)

Tactic:
· exact union_subset hss₁ <| hrss.trans <| sdiff_subset.trans inter_subset_left

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)
⊢ MapsTo f (s ∪ r) t'

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

case refine_4
α : 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)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
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✝¹ : Group G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ ∀ (a b : G), f a * f b = f b * f a

Tactic:
mul_comm,

Goal state after:
α : 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✝¹ : Group G
inst✝ : CommGroup H
f : G →* H
hf : Function.Injective ⇑f
⊢ ∀ (a b : G), True
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✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (x₁ x₂ : G), f (x₁ * x₂) = f (x₂ * x₁)

Tactic:
mul_comm,

Goal state after:
α : 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✝¹ : CommGroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
⊢ ∀ (x₁ x₂ : G), True
Module: Mathlib.Algebra.Group.TypeTags.Basic

Goal state before:
pp: case inr
ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → AddMonoid (M i)
i : ι
a : M i
j : ι
h : j ≠ i
⊢ mulSingle i (ofAdd a) j = ofAdd (single i a j)

Tactic:
simp only [mulSingle, ne_eq, h, not_false_eq_true, Function.update_of_ne, one_apply, single,
      zero_apply, ofAdd_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 ↦ x * x_1) ∘ fun x ↦ y * x) = fun x_1 ↦ x * y * x_1

Tactic:
ext z
  simp [mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 ↦ x_1 * x) ∘ fun x ↦ x * y) = fun x_1 ↦ x_1 * (y * x)

Tactic:
ext z
  simp [mul_assoc]

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

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * (1 * y⁻¹) = x / y

Tactic:
one_mul,

Goal state after:
G : Type u_3
inst✝ : DivInvMonoid G
x y : G
⊢ x * y⁻¹ = x / y
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : DivInvMonoid G
a b c : G
⊢ a * (b / c) = a * b / c

Tactic:
simp only [mul_assoc, div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a⁻¹ * b = 1
⊢ a = b

Tactic:
simpa using eq_inv_of_mul_eq_one_left h

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b⁻¹ = 1
⊢ a = b

Tactic:
simpa using eq_inv_of_mul_eq_one_left h

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

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

Tactic:
mul_comm,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
h : a = b * c
⊢ b⁻¹ * (b * c) = c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a * (b / c) = b / a

Tactic:
mul_comm,

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ b / c * (c / a) = b / a
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * (1 * u₁.inv) = 1

Tactic:
one_mul,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * u₁.inv = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * (1 * ↑u₂) = 1

Tactic:
one_mul,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ u₂.inv * ↑u₂ = 1