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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n / 2 = n

Tactic:
rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
  · cases b <;> decide
  · decide

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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * b * x = z * (a * b)

Tactic:
rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]

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

Goal state before:
pp: case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
h₃ : r b a
⊢ r a c

Tactic:
exact absurd h₃ h₁

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

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
⊢ r a c

Tactic:
rcases trichotomous_of r b c with (h₃ | rfl | h₃)

Goal state after:
case inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c

case inr.inl
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

case inr.inr
α : Sort u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
reg : IsLeftRegular a
eq : a * b = 1
⊢ (fun x ↦ a * x) (b * a) = (fun x ↦ a * x) 1

Tactic:
by simp [← mul_assoc, eq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
q : Prop
p : α → Prop
inst✝ : Decidable q
⊢ (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

Tactic:
by simp [or_comm, Decidable.forall_or_left]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
f : α → β
g : β → α
hf : Injective f
hg : RightInverse g f
b : β
⊢ f (invFun f b) = f (g b)

Tactic:
rw [hg b]
        exact invFun_eq ⟨g b, hg b⟩

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
rw [← and_forall_ne a, update_self]

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
b : α₂
h₂ : ¬∃ c, f₁₂ c = b
⊢ extend (f₂₃ ∘ f₁₂) g e' (f₂₃ b) = extend f₁₂ g (e' ∘ f₂₃) b

Tactic:
· rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]
      exact fun h ↦ h₂ (Exists.casesOn h fun c hc ↦ Exists.intro c (h₂₃ hc))

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c

Tactic:
by
  induction hbc with
  | refl => exact refl.tail hab
  | tail _ hcd hac => exact hac.tail hcd

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (ReflGen r) = ReflTransGen r

Tactic:
simp only [← transGen_reflGen, reflGen_eq_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ gb x = gb (f (f' x))

Tactic:
hf₂

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ gb x = gb x
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : { a // p a } ≃ { b // q b }
⊢ (∃ a, p a) ↔ ∃ b, q b

Tactic:
simp [← nonempty_subtype, nonempty_congr e]

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h✝ : Surjective (Sum.map f g)
d : δ
b : β
h : Sum.map f g (inr b) = inr d
⊢ ∃ a, g a = d

Tactic:
exact ⟨b, inr_injective h⟩

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), a * 1 = a

Tactic:
intros; ext; exact mul_one _

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]
    rfl

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: α : Sort u_1
x y : α
p : x ≍ y → Prop
h : ∀ (he : x = y), p ⋯
he : x ≍ y
⊢ p he

Tactic:
cases he
  exact h rfl

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

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

Tactic:
rw [Int.lt_iff_le_and_ne, Int.mul_nonneg_iff, ne_comm, Int.mul_ne_zero_iff]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (Monotone fun x ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g

Tactic:
by
  simp_rw [Monotone, Prod.mk_le_mk, forall_and]

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

Goal state before:
pp: case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + (m + 1) ≤ f (n + (m + 1))

Tactic:
rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]

Goal state after:
case succ
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m < f (n + m + 1)
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬IsEmpty ↑s ↔ ¬s = ∅

Tactic:
simpa using! nonempty_iff_ne_empty

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s ⊂ univ ↔ sᶜ.Nonempty

Tactic:
by
  rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
  simp

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

Goal state before:
pp: α : Type u
s : Set α
⊢ sᶜ ⊂ univ ↔ s.Nonempty

Tactic:
by
  rw [ssubset_def, Set.not_univ_subset, Set.nonempty_def]
  simp

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

Goal state before:
pp: case neg
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
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1

Tactic:
have hg_anti : Antitone g := by grind [Antitone]

Goal state after:
case neg
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
heq : ¬f 0 = f 1
hlt : f 1 < f 0
g : ℕ → ℕ := fun i ↦ f (i + 1)
hg_anti : Antitone g
⊢ ∃ n_1, n_1 ≤ n ∧ ∀ (m : ℕ), n_1 ≤ m → f m = f n_1
Module: Mathlib.Order.Lattice

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

Tactic:
sup_assoc

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ c ⊔ (b ⊔ a) = c ⊔ (b ⊔ a)
Module: Mathlib.Order.Lattice

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

Tactic:
sup_assoc

Goal state after:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ b ⊔ (c ⊔ a) = b ⊔ (c ⊔ a)
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}

Tactic:
by
  rw [Set.subset_pair_iff_eq, or_iff_right]; exact hs.ne_empty

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c

Tactic:
rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ← inf_assoc, himp_inf_self, inf_assoc]

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ c ⊓ (b ⊓ a) ≤ c
Module: Mathlib.Order.Heyting.Basic

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

Tactic:
sup_assoc

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

Goal state before:
pp: α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s

Tactic:
rw [← ite_inter, ← h, ite_same]

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

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ a = a ∧ f ≍ g

Tactic:
simpa [funext_iff] using h

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
sdiff_idem

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
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:
sup_assoc

Goal state after:
case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ✝ : Sort u_7
δ : Sort u_8
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
h : p ⟨a, b⟩
⊢ γ (↑default).fst (↑default).snd = γ a b

Tactic:
by rw [← show ⟨⟨a, b⟩, h⟩ = uniq.default from uniq.uniq _]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
a : α
⊢ {a} ×ˢ t = Prod.mk a '' t

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
t : Set β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ Prod.mk a '' t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ s ×ˢ {b} = (fun a ↦ (a, b)) '' s

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ (fun a ↦ (a, b)) '' s
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
· rw [h]
    simp

Goal state after:
case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) i
Module: Mathlib.Data.Set.Image

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

Tactic:
Set.mem_singleton_iff

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ (∀ (x : α), (∃ y, f y = x) ↔ x = y) ↔ ∀ (x : ι), f x = y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
⊢ range Function.diag = diagonal α

Tactic:
ext ⟨x, y⟩

Goal state after:
α : Type u_1
x y : α
⊢ (x, y) ∈ range Function.diag ↔ (x, y) ∈ diagonal α
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
⊢ (restrict f s s h)^[n] = restrict f^[n] s s ⋯

Tactic:
ext
  simpa using coe_iterate_restrict _ _ _

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

Goal state before:
pp: M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : MulOne M
inst✝² : MulOne N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
a b : M
h : a * b = 1
⊢ f a * f b = 1

Tactic:
by
  rw [← map_mul, h, map_one]

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

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

Tactic:
by
  rw [SurjOn, image_comp g f]; exact image_mono hf

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

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

Tactic:
intro u hu
  rw [image_preimage_eq_inter_range]
  exact ⟨hu, mem_range.mpr (subset_range h hu)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
⊢ invFunOn f s '' f '' s ⊆ s

Tactic:
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s
Module: Mathlib.Data.Set.Function

Goal state before:
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 ∈ t ∪ f '' s₁ ∩ t'

Tactic:
exact .inr ⟨ht' hyt', hyt'⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
⊢ x = y

Tactic:
have := congr_arg f H

Goal state after:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : f (fa x) = f (fa y)
⊢ x = y
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1) * a = a ^ n

Tactic:
by
  rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]

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
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
rw [mk_mul_mk, mul_comm g₁, 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.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
⊢ 0 * x = 0

Tactic:
zero_mul

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 0 = 0
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
⊢ 0 = 0 * y

Tactic:
zero_mul

Goal state after:
M₀ : Type u_1
M₀' : Type u_2
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ 0 * b = 0

Tactic:
zero_mul

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
ha : a = 0
⊢ 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:
ofSubtype,

Goal state after:
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
⊢ ({ toFun := fun f ↦ f.extendDomain (Equiv.refl { x // p x }), map_one' := ⋯, map_mul' := ⋯ } (f.subtypePerm h₁)) x =
    f x
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j * swap i j = σ

Tactic:
rw [mul_assoc, swap_mul_self, mul_one]

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

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

Tactic:
zero_mul

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun h ↦ x✝¹ * x✝ * h * (x✝¹ * x✝)⁻¹, invFun := fun h ↦ (x✝¹ * x✝)⁻¹ * h * (x✝¹ * x✝), left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ } =
    { toFun := fun h ↦ x✝¹ * h * x✝¹⁻¹, invFun := fun h ↦ x✝¹⁻¹ * h * x✝¹, left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯ } *
      { toFun := fun h ↦ x✝ * h * x✝⁻¹, invFun := fun h ↦ x✝⁻¹ * h * x✝, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Tactic:
by ext; simp [mul_assoc]

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

Goal state before:
pp: 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 α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ 0 * g 0 = 0

Tactic:
zero_mul

Goal state after:
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 α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

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

Tactic:
zero_mul

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬0 * g⁻¹ • (g • 0)⁻¹ = 1

Tactic:
zero_mul

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬0 = 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 = 0 * 0 ^ n

Tactic:
zero_mul

Goal state after:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 = 0
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 0 ↔ n = 0

Tactic:
by rw [← cast_zero, cast_inj]

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

Goal state before:
pp: case zero
α : Type u
inst✝ : NonAssocSemiring α
a : α
⊢ 0 = 0 * a

Tactic:
zero_mul

Goal state after:
case zero
α : Type u
inst✝ : NonAssocSemiring α
a : α
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ 0 * b = 0

Tactic:
zero_mul

Goal state after:
α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ 0 = 0
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m✝ n m : ℕ
⊢ IsSquare m ↔ m.sqrt * m.sqrt = m

Tactic:
simp_rw [← Nat.exists_mul_self m, IsSquare, eq_comm]

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
r : R
h : IsRightRegular r
r' : R
eq : r' * r = 0
⊢ 0 = 0 * r

Tactic:
zero_mul

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 * (1 / -a)

Tactic:
by rw [← inv_eq_one_div, division_def]

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

Goal state before:
pp: case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ 0 = 0 * a⁻¹ʳ

Tactic:
zero_mul

Goal state after:
case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x✝ : IsUnit 0
a : M₀
a0 : 0 * a = 1
inv_val✝ : a * 0 = 1
⊢ 0 = 1

Tactic:
zero_mul

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x✝ : IsUnit 0
a : M₀
a0 : 0 = 1
inv_val✝ : a * 0 = 1
⊢ 0 = 1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 = 0 * (0 ^ n)⁻¹

Tactic:
zero_mul

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
h : n < m
⊢ 0 = 0
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x

Tactic:
exact ihn.add_left (Commute.one_left x)

Goal state after: