mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : n = 0 → b = true
⊢ (if h : n = 0 → b = true then
      bit b n h
        (binaryRec zero
          (fun b n ih ↦
            if h : n = 0 → b = true then bit b n h ih
            else
              have this := ⋯;
              ⋯ ▸ zero)
          n)
    else
      have this := ⋯;
      ⋯ ▸ zero) =
    bit b n h (binaryRec' zero bit n)

Tactic:
dif_pos h,

Goal state after:
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
h : n = 0 → b = true
⊢ bit b n h
      (binaryRec zero
        (fun b n ih ↦
          if h : n = 0 → b = true then bit b n h ih
          else
            have this := ⋯;
            ⋯ ▸ zero)
        n) =
    bit b n h (binaryRec' zero bit n)
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ n) (y ^ n)

Tactic:
induction n with
  | zero =>
    rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _
  | succ n ih =>
    rw [pow_succ, pow_succ]
    exact ih.mul_right h

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

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

Tactic:
replace hk : k' ≠ 0 := by lia

Goal state after:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : 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
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
k' : ℕ
hk : 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

Tactic:
induction k' using Nat.binaryRecFromOne generalizing n m with
  | zero => simp at hk
  | one => simp [npowRec']
  | bit b k' k'0 ih =>
    rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
    cases b <;> simp only [Nat.bit, cond_false, cond_true, npowRec'_two_mul]
    rw [npowRec'_succ (by lia), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by lia), mul_assoc]

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowBinRec (n + 1) m = npowBinRec n m * m

Tactic:
iterate 2 rw [← npowBinRecAuto, ← npowRec_eq_npowBinRec]
  rfl

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

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

Tactic:
by
  cases h
  exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

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

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

Tactic:
by
  cases h
  exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
b✝ a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), motive a ⋯) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯) → motive a a✝
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ motive a ⋯

Tactic:
apply h_ih
  · exact fun h ↦ head h (.single hbc) (single hbc)
  · exact fun hab hbc ↦ head hab _

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧

Tactic:
Quotient.out_eq y

Goal state after:
α : Sort u_1
s : Setoid α
x : α
y : Quotient s
⊢ ⟦x⟧ = y ↔ ⟦x⟧ = y
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ min a b

Tactic:
rw [min_def]
  split_ifs <;> assumption

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j = i

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i ∧ i ≤ j
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
⊢ OrderTop α ⊕' NoTopOrder α

Tactic:
letI : Top α := ⟨Classical.choose H⟩

Goal state after:
case neg
α✝ : Type u
β : Type v
α : Type u_1
inst✝ : LE α
H : ∃ a, ∀ (b : α), b ≤ a
this : Top α := { top := Classical.choose H }
⊢ OrderTop α ⊕' NoTopOrder α
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ∧ y ≤ x ↔ x' = y'
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ∧ y ≤ x ↔ x' = y'

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ∧ y ≤ x ↔ x' ≤ y' ∧ y' ≤ x'
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∃ f, StrictMono f

Tactic:
refine ⟨fun n ↦ Int.casesOn n f fun n ↦ g (n + 1), strictMono_int_of_lt_succ ?_⟩

Goal state after:
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ ∀ (n : ℤ), (casesOn n f fun n ↦ g (n + 1)) < casesOn (n + 1) f fun n ↦ g (n + 1)
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p q : α → Prop
⊢ {x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)

Tactic:
Set.ext_iff,

Goal state after:
α : Type u
s : Set α
p q : α → Prop
⊢ (∀ (x : α), x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ {x | x ∈ s ∧ q x}) ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x

Tactic:
Set.ext_iff,

Goal state after:
α : Type u
s : Set α
p : α → Prop
⊢ (∀ (x : α), x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ s) ↔ ∀ (x : α), x ∈ s → p x
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
p : α → Prop
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x

Tactic:
Set.ext_iff,

Goal state after:
α : Type u
s : Set α
p : α → Prop
⊢ (∀ (x : α), x ∈ {x | x ∈ s ∧ p x} ↔ x ∈ ∅) ↔ ∀ (x : α), x ∈ s → ¬p x
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: case pos
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : p
⊢ x ∈ univ ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
simp_all

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

Goal state before:
pp: case neg
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
h✝ : ¬p
⊢ x ∈ t h✝ ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : 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)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : semilatt_sup_inst.toPartialOrder = semilatt_inf_inst.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ b

Tactic:
rw [partial_order_eq]
      apply inf_le_right

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ b = a ⊔ b ↔ a = b

Tactic:
rw [← inf_le_sup.ge_iff_eq, sup_le_inf]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ b < a ⊔ b ↔ a ≠ b

Tactic:
by rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]

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

Goal state before:
pp: case inl
α : Type u
s : Set α
h✝ : s = ∅
⊢ s.Subsingleton

Tactic:
simp_all

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

Goal state before:
pp: case inr
α : Type u
w✝ : α
⊢ {w✝}.Subsingleton

Tactic:
simp_all

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

Goal state before:
pp: case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

pp: case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

pp: case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

pp: case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
· rw [removeNoneAux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm

Goal state after:
case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

case some.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

case some.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x val✝¹ : α
h1 : e.symm (some (e.removeNoneAux x)) = some val✝¹
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_7
β : Type u_8
a : α
b : β
c : α
d : β
h : (a, b).toSigma = (c, d).toSigma
⊢ (a, b) = (c, d)

Tactic:
simp_all

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = ⊥ ∧ y = ⊥ ↔ x = ⊥ ∧ y = ⊥

Tactic:
simp_all

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

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

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (y \ z) ≤ x \ y ∧ x \ y ≤ (x \ z) \ (y \ z)
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
f : α → β
p : α → Prop
q : β → Prop
h : ∀ (x : α), p x ↔ q (f x)
y : Subtype q
x : α
⊢ (∃ h_1, ⟨f ↑⟨x, h_1⟩, ⋯⟩ = y) ↔ f x = ↑y

Tactic:
exact ⟨fun ⟨hp, h'⟩ => congr_arg Subtype.val h', fun h' => ⟨(h x).2 (h'.symm ▸ y.2),
            Subtype.ext h'⟩⟩

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b

Tactic:
exact h.of_disjoint_inf_of_le le_sup_left

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ (a ∆ b) = b

Tactic:
symmDiff_symmDiff_cancel_left

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ b = b
Module: Mathlib.Logic.Equiv.Basic

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

Tactic:
simp_all

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

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

Tactic:
simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ (range f ∩ s ⊆ range f ∩ s' ∧ ∃ x, x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔
    f ⁻¹' s ⊆ f ⁻¹' s' ∧ ∃ x, x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s

Tactic:
apply and_congr ?_ (by aesop)

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊆ range f ∩ s' ↔ f ⁻¹' s ⊆ f ⁻¹' s'
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
simp only [← and_and_left, mem_inter_iff, mem_prod]

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 α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)

Tactic:
by
  simp_rw [Set.symmDiff_def, image_union, image_sdiff hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, ← not_nonempty_iff_eq_empty, image_inter_nonempty_iff]

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

Goal state before:
pp: case mp
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s → t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
intro h
    by_cases hs : a ∈ t
    · right
      refine ⟨t \ {a}, by grind⟩
    · grind

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ range f = {y} ↔ ∀ (x : ι), f x = y

Tactic:
Set.ext_iff,

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ (∀ (x : α), x ∈ range f ↔ x ∈ {y}) ↔ ∀ (x : ι), f x = y
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.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ Prod.snd '' s ×ˢ t = t₁

Tactic:
← snd_image_prod h₁.1 t₁,

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ Prod.snd '' s ×ˢ t = Prod.snd '' s₁ ×ˢ t₁
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)

Tactic:
by
  simp only [EqOn, ← forall_and]
  refine forall_congr' fun a => ?_; by_cases a ∈ s <;> simp [*]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ ∅ = s₁ ×ˢ t₁

Tactic:
@eq_comm _ ∅,

Goal state after:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s₁ ×ˢ t₁ = ∅
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 : α
hx : x ∈ s
⊢ s.piecewise f g x = f x

Tactic:
simp_all

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 : α
hx : x ∈ sᶜ
⊢ s.piecewise f g x = g x

Tactic:
simp_all

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

Goal state before:
pp: case pos
ι : 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
h✝ : p i
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i

Tactic:
simp_all

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

Goal state before:
pp: case neg
ι : 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
h✝ : ¬p i
⊢ f i ∈ (fun i ↦ if p i then t₁ i else t₂ i) i

Tactic:
simp_all

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
⊢ (∃ f, s = graphOn f (Prod.fst '' s)) → InjOn Prod.fst s

Tactic:
rintro ⟨f, hf⟩
    rw [hf]
    exact InjOn.image_of_comp <| injOn_id _

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (1 + n) = a * a ^ n

Tactic:
rw [zpow_add, zpow_one]

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

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

Tactic:
rw [mul_assoc, ← mul_assoc u₂.val, val_inv, one_mul, val_inv]

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

Goal state before:
pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 0 = 0 * 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 * 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 0 = 1 * 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : x * y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 0 = 1 * 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 * 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 1 = 0 * 1

Tactic:
simp_all

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

Goal state before:
pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 1 = 1 * 0

Tactic:
simp_all

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

Goal state before:
pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀✝ : Type u_6
inst✝⁹ : MulZeroOneClass α
inst✝⁸ : MulZeroOneClass β
inst✝⁷ : MulZeroOneClass γ
inst✝⁶ : MulZeroOneClass δ
inst✝⁵ : FunLike F α β
M₀ : Type u_7
N₀ : Type u_8
inst✝⁴ : MulZeroOneClass M₀
inst✝³ : MulZeroOneClass N₀
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
x y : M₀
h✝² : ¬x * y = 0
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 1 = 1 * 1

Tactic:
simp_all

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

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

Tactic:
· rw [inv_mul_cancel₀ h, one_mul]

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

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
p : Prop
inst✝ : Decidable p
a : M₀
b : A
⊢ (if p then a else 0) • b = if p then a • b else 0

Tactic:
ite_smul,

Goal state after:
M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
p : Prop
inst✝ : Decidable p
a : M₀
b : A
⊢ (if p then a • b else 0 • b) = if p then a • b else 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ (if j = i then 1 else 0) • x = single i x j

Tactic:
ite_smul,

Goal state after:
M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
ι : Type u_12
inst✝ : DecidableEq ι
x : A
i j : ι
⊢ (if j = i then 1 • x else 0 • x) = single i x j