mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Semiconj.Defs

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

Tactic:
| zero =>

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m n : M
hk : 0 ≠ 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)) 0
      m n =
    m * npowRec' 0 n

Tactic:
| zero =>

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

Goal state before:
pp: 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

Tactic:
npowRec'_succ (by lia),

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') n * n)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a b : M
⊢ (a * b) ^ 0 * a = a * (b * a) ^ 0

Tactic:
| zero =>

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

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

Tactic:
rw [mul_comm, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q : Prop
⊢ ¬Xor P Q ↔ (P ↔ Q)

Tactic:
by
  simp only [not_and, Xor, not_or, not_not, ← iff_iff_implies_and_implies]

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

Goal state before:
pp: case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s ↦ ⟨U, cast ⋯ s⟩
hg : Injective g
⊢ False

Tactic:
exact cantor_injective g hg

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : β → α
h : β → γ
i : γ → β
hf : LeftInverse f g
hh : LeftInverse h i
a : γ
⊢ h (f (g (i a))) = a

Tactic:
rw [hf (i a), hh a]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.inl.inl
α : Type u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
ac : ReflTransGen r a b✝
IH : ReflTransGen r b✝ b✝
⊢ ReflTransGen r c✝ b✝ ∨ ReflTransGen r b✝ c✝

Tactic:
exact Or.inr (single bd)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen r ≤ ReflTransGen r

Tactic:
intro a

Goal state after:
α : Type u_1
r : α → α → Prop
a : α
⊢ TransGen r a ≤ ReflTransGen r a
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
⊢ TransGen r ≤ (TransGen p on f)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a : α
⊢ TransGen r a ≤ (TransGen p on f) a
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α β : Sort u_1
h : α = β
a : α
b : β
⊢ (Equiv.cast h) a = b ↔ a ≍ b

Tactic:
subst h; simp

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

Goal state before:
pp: case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g (0 + k))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[0] = f^[0] ∘ g^[0]

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_4
⊢ IsEmpty (ULift α) ↔ IsEmpty α

Tactic:
simp only [← not_nonempty_iff, nonempty_ulift]

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) → Group (f i)
⊢ ∀ (a : (i : I) → f i), a⁻¹ * a = 1

Tactic:
by intros; ext; exact inv_mul_cancel _

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

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
x₁ : α
y₁ : β
P : Sort u_5
w : x₁ = x₁ → y₁ = y₁ → P
⊢ P

Tactic:
exact w rfl rfl

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

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

Tactic:
by
  cases le_total b c <;> simp [min_eq_left, min_eq_right, *]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
a b : α
⊢ A_lt a b = B_lt a b

Tactic:
rw [A_iff, B_iff]

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

Goal state before:
pp: α : Type u
inst✝¹ : Top α
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
ha : ∀ (h : p), a h ≠ ⊤
hb : ∀ (h : ¬p), b h ≠ ⊤
⊢ (if h : p then a h else b h) ≠ ⊤

Tactic:
split <;> solve_by_elim

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

Goal state before:
pp: case zero
a : ℕ
ha : a ≠ 1
⊢ a * 0 ≤ a ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case succ.inl
b : ℕ
ha : 0 ≠ 1
⊢ 0 * (b + 1) ≤ 0 ^ (b + 1)

Tactic:
rw [Nat.zero_mul]; exact Nat.zero_le _

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
· have hab : Compares Ordering.gt a b := hab
    rwa [ho.inj (h hab)]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ ∀ (a a' : α), a' ≤ a → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
intro a

Goal state after:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
⊢ ∀ (a' : α), a' ≤ a → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ ¬(P ∧ Q) ∧ Codisjoint P Q ↔ ¬(P ↔ Q)

Tactic:
Prop.codisjoint_iff,

Goal state after:
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ ¬(P ↔ Q)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case zero
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
⊢ f n + 0 ≤ f (n + 0)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
⊢ (Monotone fun n ↦ f (n + k)) ↔ MonotoneOn f {x | k ≤ x}

Tactic:
by
  refine ⟨fun h x hx y hy hle ↦ ?_, fun h x y hle ↦ ?_⟩
  · rw [← Nat.sub_add_cancel hx, ← Nat.sub_add_cancel hy]
    rw [← Nat.sub_le_sub_iff_right hy] at hle
    exact h hle
  · rw [← Nat.add_le_add_iff_right] at hle
    exact h (Nat.le_add_left k x) (Nat.le_add_left k y) hle

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

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

Tactic:
| zero =>

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

Goal state before:
pp: case zero
f : ℕ → ℕ
mono_f : Monotone f
hc : ∀ (n : ℕ), f n ≤ 0
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x

Tactic:
rw [← sup_inf_sdiff x y, sup_comm]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
s : x ⊓ y ⊔ z = x
i : x ⊓ y ⊓ z = ⊥
| x \ y ⊔ x ⊓ y
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ aᶜᶜ ⊓ bᶜᶜ ≤ (a ⊓ b)ᶜᶜ

Tactic:
rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
    disjoint_left_comm, disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]

Goal state after:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint (a ⊓ b) (a ⊓ b)ᶜ
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ e (some x) = e none ↔ e.symm none = some x

Tactic:
have h1 := congr_arg e.symm h

Goal state after:
case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
h1 : e.symm (e (some x)) = e.symm (some a)
⊢ e (some x) = e none ↔ e.symm none = some x
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
⊢ GeneralizedHeytingAlgebra α

Tactic:
by
  let lattice := e.lattice
  let top := e.top
  let himp := e.himp
  apply e.injective.generalizedHeytingAlgebra <;> intros <;>
  first | rfl | exact e.apply_symm_apply _

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
⊢ GeneralizedCoheytingAlgebra α

Tactic:
apply e.injective.generalizedCoheytingAlgebra <;> intros

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := ⋯
bot : Bot α := ⋯
sdiff : SDiff α := ⋯
⊢ e ⊥ = ⊥

case map_sdiff
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedCoheytingAlgebra β
lattice : Lattice α := e.lattice
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
a✝ b✝ : α
⊢ e (a✝ \ b✝) = e a✝ \ e b✝
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inr
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ (if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, h⟩) = Sum.inr ⟨x, hx⟩

Tactic:
dif_neg

Goal state after:
case inr
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ Sum.inr ⟨x, ?inr.hnc⟩ = Sum.inr ⟨x, hx⟩

case inr.hnc
α✝ : 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
p : α → Prop
inst✝ : DecidablePred p
x : α
hx : ¬p x
⊢ ¬p x
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
f : ℕ → Type u
⊢ LeftInverse (Sum.elim (Sigma.mk 0) (Sigma.map Nat.succ fun x ↦ id)) fun x ↦
    Sigma.casesOn x fun n ↦
      Nat.casesOn (motive := fun i ↦ f i → f 0 ⊕ (n : ℕ) × f (n + 1)) n (fun x ↦ inl x) fun n x ↦ inr ⟨n, x⟩

Tactic:
rintro ⟨n | n, x⟩ <;> rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ a = ⊥

Tactic:
rw [symmDiff, sup_idem, sdiff_self]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

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

Tactic:
· rw [sup_right_comm]
    exact le_sup_of_le_left le_sdiff_sup

Goal state after:
case refine_2
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case zero
α : Type u_1
f : α → α
⊢ preimage f^[0] = (preimage f)^[0]

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
t : α
s : Set α
⊢ t ∈ compl '' s ↔ tᶜ ∈ s

Tactic:
simp [← preimage_compl_eq_image_compl]

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

Goal state before:
pp: case zero
α : Type u_1
f : α → α
⊢ image f^[0] = (image f)^[0]

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
⊢ ↑((restrict f s s h)^[0] x) = f^[0] ↑x

Tactic:
| zero =>

Goal state after:
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' : restrict f s t h ⟨a, ha⟩ = ⟨b, hb⟩
⊢ b ∈ f '' s

Tactic:
replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'

Goal state after:
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
⊢ b ∈ f '' s
Module: Mathlib.Data.Set.Prod

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

Tactic:
intro x hxt

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : α
hxs : x✝ ∈ s
x : β
hxt : x ∈ t
⊢ g x = g' x
Module: Mathlib.Data.Set.Image

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

Tactic:
simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' univ.pi t = univ.pi fun i ↦ t (f i)

Tactic:
by
  simpa [f.surjective.range_eq] using piCongrLeft_preimage_pi f univ t

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

Goal state before:
pp: case h₁
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s

Tactic:
rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩
    exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case ofNat.zero
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
⊢ motive (ofNat 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case negSucc.zero
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i : ℕ
⊢ motive (-↑0)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
⊢ MapsTo (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩; exact ⟨_, h ha, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩

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

Goal state before:
pp: case zero
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
⊢ P (g ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
⊢ P (g ^ 0)

Tactic:
| zero =>

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

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

Tactic:
rw [div_eq_iff_eq_mul, mul_comm]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * (f b c * (f c a * f a c)) = f a b * f b c

Tactic:
hf_swap (symm pac),

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
rca : r c a
⊢ f a b * (f b c * 1) = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Bijective ⇑f
u v : N
uv : u * v = 1
vu : v * u = 1
⊢ ∃ a, (map f) a = { val := u, inv := v, val_inv := uv, inv_val := vu }

Tactic:
rcases hf.surjective u, hf.surjective v with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩

Goal state after:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Bijective ⇑f
u v : M
uv : f u * f v = 1
vu : f v * f u = 1
⊢ ∃ a, (map f) a = { val := f u, inv := f v, val_inv := uv, inv_val := vu }
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : M
⊢ ((f.coprod g).comp (inl M N)) x = f x

Tactic:
simp [coprod_apply]

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

Goal state before:
pp: M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M →* P
g : N →* P
x : N
⊢ ((f.coprod g).comp (inr M N)) x = g x

Tactic:
simp [coprod_apply]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b) = (fun b a ↦ f a b) <$> b <*> a

Tactic:
rw [@CommApplicative.commutative_prod m h]

Goal state after:
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (fun p ↦ f p.fst p.snd) <$> ((fun b a ↦ (a, b)) <$> b <*> a) = (fun b a ↦ f a b) <$> b <*> a
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case zero
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
⊢ ∀ (y : M₀), f (x ^ 0 * y) = f x ^ 0 * f y

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
⊢ f.subtypePerm hf ^ 0 = (f ^ 0).subtypePerm ⋯

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ∀ (x_1 : α), (ofSubtype x) x_1 = (ofSubtype y) x_1
⊢ ∀ (x_1 : Subtype p), x x_1 = y x_1

Tactic:
intro a

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ∀ (x_1 : α), (ofSubtype x) x_1 = (ofSubtype y) x_1
a : Subtype p
⊢ x a = y a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case zero
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : 0 ≠ 0
⊢ IsNilpotent (x ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
ha : a ^ 0 = 0
⊢ a = 0

Tactic:
simpa using congr_arg (a * ·) ha

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

Goal state before:
pp: case zero
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
ha : a ^ 0 = 0
⊢ a = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ ↑(m + 0) = ↑m + ↑0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case ind.zero
R : Type u_1
inst✝ : AddMonoidWithOne R
hk : ∀ (m : ℕ), m < 0 → m.binCast = ↑m
⊢ Nat.binCast 0 = ↑0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 2 + 1 = 3

Tactic:
← one_add_one_eq_two,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 = 3
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 2 + 1 + 1 = 4

Tactic:
← one_add_one_eq_two,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 + 1 + 1 = 4
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case zero
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ 0 = n

Tactic:
| zero =>

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ 2 • x = x + x

Tactic:
← one_add_one_eq_two,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ (1 + 1) • x = x + x
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: case inl.zero
α : Type u_1
inst✝ : NonAssocRing α
⊢ ∀ (n : ℤ), ↑(↑0 * n) = ↑↑0 * ↑n

Tactic:
| zero =>

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

Goal state before:
pp: case inr.zero
α : Type u_1
inst✝ : NonAssocRing α
⊢ ∀ (n : ℤ), ↑(-↑0 * n) = ↑(-↑0) * ↑n

Tactic:
| zero =>

Goal state after: