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

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
⊢ (if h' : 0 = 0 then
      have this := ⋯;
      ⋯ ▸ one
    else bit true 0 h' zero) =
    one

Tactic:
dif_pos rfl

Goal state after:
motive : Nat → Sort u
zero : motive 0
one : motive 1
bit : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (Nat.bit b n)
⊢ (have this := ⋯;
    ⋯ ▸ one) =
    one
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ one₁ = one₂

Tactic:
exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

Goal state after:
Module: Mathlib.Logic.Basic

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

Tactic:
rintro ⟨rfl, h⟩

Goal state after:
β : Sort u
b a : β
h : a = cast ⋯ b
⊢ a ≍ b
Module: Mathlib.Logic.Basic

Goal state before:
pp: P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h

Tactic:
by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]

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

Goal state before:
pp: case inl
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
b : β
a : α
⊢ update f a b a = if a = a then b else f a

Tactic:
simp [*]

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

Goal state before:
pp: case inr
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
hne : a ≠ a'
⊢ update f a' b a = if a = a' then b else f a

Tactic:
simp [*]

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

Goal state before:
pp: case inl
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
j : ι
a : α j
⊢ Pi.map f (update g j a) j = update (Pi.map f g) j (f j a) j

Tactic:
simp [*]

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

Goal state before:
pp: case inr
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
a : α i
j : ι
hij : j ≠ i
⊢ Pi.map f (update g i a) j = update (Pi.map f g) i (f i a) j

Tactic:
simp [*]

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

Goal state before:
pp: case inl.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
⊢ curry (update f (a, a') b) a a' = update (curry f) (a, a').fst (update (curry f (a, a').fst) (a, a').snd b) a a'

Tactic:
simp [*]

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

Goal state before:
pp: case inl.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
ha' : a' ≠ a₂'
⊢ curry (update f (a, a₂') b) a a' = update (curry f) (a, a₂').fst (update (curry f (a, a₂').fst) (a, a₂').snd b) a a'

Tactic:
simp [*]

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

Goal state before:
pp: case inr.inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
ha : a ≠ a₂
⊢ curry (update f (a₂, a') b) a a' = update (curry f) (a₂, a').fst (update (curry f (a₂, a').fst) (a₂, a').snd b) a a'

Tactic:
simp [*]

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

Goal state before:
pp: case inr.inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
ha' : a' ≠ a₂'
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
b : α
motive : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : motive b ⋯
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯
⊢ motive a h

Tactic:
induction h with
  | refl => exact refl
  | @tail b c _ hbc ih =>
  apply ih
  · exact head hbc _ refl
  · exact fun h1 h2 ↦ head h1 (h2.tail hbc)

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

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

Tactic:
iterate_succ_apply'

Goal state after:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ f (f^[l.length] b) = f (f^[l.length] b)
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inl i → Sum.elim f g x_1 = Sum.elim (update f i x) g x_1

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inr i → Sum.elim f g x_1 = Sum.elim f (update g i x) x_1

Tactic:
by simp +contextual

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
obtain ⟨c, h⟩ := exists_lt a

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder α
x✝ : α × β
a : α
b : β
c : α
h : c < a
⊢ ∃ b_1, b_1 < (a, b)
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ a = b

Tactic:
exact le_antisymm (ha _) (hb _)

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

Goal state before:
pp: case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a ^ (b + 1)

Tactic:
rw [Nat.pow_succ']

Goal state after:
case succ.inr
a : ℕ
ha : a ≠ 1
b : ℕ
ha0 : a > 0
ha1 : a > 1
⊢ a * (b + 1) ≤ a * a ^ b
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case pos
P Q : Prop
h✝¹ : P
h✝ : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case neg
P Q : Prop
h✝¹ : P
h✝ : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case pos
P Q : Prop
h✝¹ : ¬P
h✝ : Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: case neg
P Q : Prop
h✝¹ : ¬P
h✝ : ¬Q
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictMono f

Tactic:
rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥

Tactic:
rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm,
      h'.inf_eq_bot, inf_bot_eq]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

Tactic:
rw [← sup_assoc, ← sup_assoc, @sup_comm α _ a]

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

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s ∩ tᶜ = tᶜ ∩ s

Tactic:
inter_comm

Goal state after:
α : Type u_1
s t : Set α
⊢ tᶜ ∩ s = tᶜ ∩ s
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (t ∩ s).Nonempty ↔ (s ∩ t).Nonempty

Tactic:
inter_comm

Goal state after:
α : Type u_1
s t : Set α
⊢ (s ∩ t).Nonempty ↔ (s ∩ t).Nonempty
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
b : α
hbt : ¬b ∈ t
⊢ b ∈ insert b (s \ t)

Tactic:
simp [*]

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

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
a b : α
hbt : ¬b ∈ t
hbs : b ∈ s
⊢ b ∈ insert a (s \ t)

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
rw [h, hi.eq_bot]

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

Goal state before:
pp: case pos
α✝ : 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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : a = default
⊢ Option.elim' default Subtype.val none = a

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α✝ : 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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
a : α
h✝ : ¬a = default
⊢ Option.elim' default Subtype.val (some ⟨a, h✝⟩) = a

Tactic:
simp [*]

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
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 : { x // p₂ x }
⊢ (fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯)
      ((fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯) a) =
    a

Tactic:
obtain ⟨a, ha⟩ := a

Goal state after:
α : 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₁
ha : p₂ a
⊢ (fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯)
      ((fun a ↦ Quotient.hrecOn (motive := fun x ↦ p₂ x → Quotient s₂) (↑a) (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯) ⟨a, ha⟩) =
    ⟨a, ha⟩
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case pos
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : r = a
⊢ a = r

Tactic:
simp [*]

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

Goal state before:
pp: case neg
α : Sort u_1
inst✝ : DecidableEq α
r a : α
h✝ : ¬r = a
⊢ r = r

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
⊢ GeneralizedBooleanAlgebra α

Tactic:
let bot := e.bot
  let sdiff := e.sdiff
  let distribLattice := e.distribLattice
  apply e.injective.generalizedBooleanAlgebra <;> intros <;>
  first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b

Tactic:
← symmDiff_of_le ha

Goal state after:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ s → f x = f y → x = y
b : β
x✝ : b ∈ f '' s ∩ f '' t
a₁ : α
ha₁ : a₁ ∈ s
h₁ : f a₁ = b
a₂ : α
ha₂ : a₂ ∈ t
h₂ : f a₂ = b
⊢ f a₂ = f a₁

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
s : Set α
t : Set γ
⊢ Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)

Tactic:
ext
  aesop

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

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : i ∈ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : ¬i ∈ s
⊢ s.piecewise f₁ f₂ i ≤ g i

Tactic:
simp [*]

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

Goal state before:
pp: case h₁
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : i✝ ∈ s
⊢ f₁ i✝ ≤ s.piecewise g₁ g₂ i✝

Tactic:
simp [*]

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

Goal state before:
pp: case h₂
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i✝ : α
a✝ : ¬i✝ ∈ s
⊢ f₂ i✝ ≤ s.piecewise g₁ g₂ i✝

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s)

Tactic:
rw [← exists_range_iff, range_image]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a
Module: Mathlib.Data.Set.Piecewise

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

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
⊢ univ.pi t = ∅ ↔ ∃ i, t i = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, univ_pi_nonempty_iff]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ f '' f ⁻¹' s = f '' t ↔ s = f '' t

Tactic:
hf.2.image_preimage

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ s = f '' t ↔ s = f '' t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ f '' s = f '' f ⁻¹' t ↔ f '' s = t

Tactic:
hf.2.image_preimage

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ f '' s = t ↔ f '' s = t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ s₁ ⊆ s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁

Tactic:
h.image_subset_image_iff h₂ h₁

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
⊢ BijOn g (p₁ '' s) (p₂ '' t)

Tactic:
obtain ⟨h1, h2, h3⟩ := hbij
  refine ⟨?_, hinj, ?_⟩
  · rintro _ ⟨a, ha, rfl⟩
    exact ⟨f a, h1 ha, by rw [comm a]⟩
  · rintro _ ⟨b, hb, rfl⟩
    obtain ⟨a, ha, rfl⟩ := h3 hb
    grind

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
ha : a ≠ 1
⊢ a ^ n = 1 ↔ n = 0

Tactic:
simp [*]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
n : ℤ
a : G
ha : a ≠ 1
⊢ a ^ n = 1 ↔ n = 0

Tactic:
simp [*]

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

Goal state before:
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)
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

Tactic:
refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_

Goal state after:
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)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t
Module: Mathlib.Algebra.Group.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : AddZeroClass α
⊢ unop 0 = 0

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoid α
⊢ unop 0 = 0

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : SubNegMonoid α
⊢ unop 0 = 0

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroup α
⊢ unop 0 = 0

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : MulOneClass α
⊢ unop 1 = 1

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
⊢ unop 1 = 1

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
⊢ unop 1 = 1

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
⊢ unop 1 = 1

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
⊢ unop 1 = 1

Tactic:
by exact rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
⊢ unop 1 = 1

Tactic:
by exact rfl

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

Goal state before:
pp: case succ
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)

Tactic:
simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
x✝ : G
⊢ (fun x ↦ x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)

Tactic:
simp [zpow_iterate, Int.pow_succ', zpow_mul]

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

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

Tactic:
rw [Commute, SemiconjBy, inv_mul, mul_inv]

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:
by
  rw [mul_comm, h.mul_div_cancel_right]

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

Goal state before:
pp: case inl
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
a : M₀
inst✝¹ : IsReduced M₀
inst✝ : Nontrivial M₀
⊢ a ^ 0 = 0 ↔ a = 0 ∧ 0 ≠ 0

Tactic:
simp [*]

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

Goal state before:
pp: case inr
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
a : M₀
n : ℕ
inst✝¹ : IsReduced M₀
inst✝ : Nontrivial M₀
hn : n ≠ 0
⊢ a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

Tactic:
simp [*]

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

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

Tactic:
by cases h

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
a : α
f : F
x✝ : IsSquare a
r : α
h✝ : a = r * r
⊢ f a = f r * f r

Tactic:
simp [*]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
hf : Function.Surjective ⇑f
b : β
x✝ : b ∈ {b | IsSquare b}
r : α
h✝ : b = f r * f r
⊢ r * r ∈ {a | IsSquare a} ∧ f (r * r) = b

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)

Tactic:
aesop (add simp Commute.mul_zpow)

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

Goal state before:
pp: m n : ℤ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
  rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
  simp [even_iff, h₁, h₂, Int.mul_emod]

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

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

Tactic:
by
  rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]

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

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit z
h1 : x * z = y
⊢ x = y * z⁻¹ʳ

Tactic:
by rw [← h1, mul_inverse_cancel_right _ _ h]

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a / 0 * 0 = a

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a * 0 / 0 = a

Tactic:
simp [*]

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

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

Tactic:
simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a⁻¹ʳ = a⁻¹

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0
  · simp
  · exact Ring.inverse_unit (Units.mk0 a ha)

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

Goal state before:
pp: α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℕ
⊢ n • a = ↑↑n * a

Tactic:
nsmul_eq_mul,

Goal state after:
α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℕ
⊢ ↑n * a = ↑↑n * a
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (-x * y) = f (-(x * y))

Tactic:
neg,

Goal state after:
R : Type u_1
S : Type u_2
f✝ : S → R
hf✝ : Injective f✝
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
f : S → R
hf : Injective f
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : S), f (-a) = -f a
mul : ∀ (a b : S), f (a * b) = f a * f b
x y : S
⊢ f (-x * y) = -f (x * y)