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

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec 0 m = npowBinRec.go 0 1 m

Tactic:
rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]

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

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

Tactic:
by
  rw [← mul_assoc, mul_inv_cancel, one_mul]

Goal state after:
Module: Mathlib.Logic.Basic

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

Tactic:
simp only [← @xor_not_right a, not_not]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a : α
B : ¬P → α
⊢ dite P (fun x ↦ a) B ≠ a ↔ ∃ h, a ≠ B h

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
⊢ (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y : α
⊢ f x = g y ↔ f = g

Tactic:
by
  refine ⟨fun h ↦ funext fun z ↦ ?_, fun h ↦ ?_⟩
  · rwa [Subsingleton.elim x z, Subsingleton.elim y z] at h
  · rw [h, Subsingleton.elim x y]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₁ = (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₂
⊢ x₁ = x₂

Tactic:
by
  grind

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

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
α : κ → Sort u_3
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
ctor : ι → κ
x✝ : Injective ctor
recursor : ((i : ι) → α (ctor i)) → (i : κ) → α i
h : ∀ (f : (i : ι) → α (ctor i)) (i : ι), recursor f (ctor i) = f i
h2 : ∀ (f₁ f₂ : (i : ι) → α (ctor i)) (k : κ), (∀ (i : ι), ctor i ≠ k) → recursor f₁ k = recursor f₂ k
f : (i : ι) → α (ctor i)
i : ι
x : α (ctor i)
⊢ recursor (update f i x) = update (recursor f) (ctor i) x

Tactic:
by
  grind

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

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
⊢ f j (update g i v j) = update (fun k ↦ f k (g k)) i (f i v) j

Tactic:
by
  grind

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

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
⊢ f j (update g i v j) (update h i w j) = update (fun k ↦ f k (g k) (h k)) i (f i v w) j

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
P : ⦃a : α⦄ → β a → Prop
f : (a : α) → β a
a' : α
v : β a'
a : α
⊢ P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
⊢ update (update f a v) b w = update (update f b w) a v

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
⊢ update (update f a v) a w = update f a w

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ cast ⋯ (C (g (f a))) = C a

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → β
⊢ (r ∘r fun x1 x2 ↦ x1 = f x2) = fun x1 x2 ↦ r x1 (f x2)

Tactic:
by
  ext x y
  simp [Comp]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → α
⊢ (fun x1 x2 ↦ f x1 = x2) ∘r r = fun x ↦ r (f x)

Tactic:
by
  ext x y
  simp [Comp]

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
cases U bd be

Goal state after:
case tail.inl.inr.refl
α : Type u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b✝ c✝ : α
a✝ : ReflTransGen r a b✝
bd : r b✝ c✝
IH : ReflTransGen r b✝ c
be : r b✝ c✝
ec : ReflTransGen r c✝ c
⊢ ReflTransGen r c✝ c ∨ ReflTransGen r c c✝
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[m + n.succ] = f^[m] ∘ f^[n.succ]

Tactic:
rw [Nat.add_succ, iterate_succ, iterate_succ, iterate_add m n]

Goal state after:
α : Type u
f : α → α
m n : ℕ
⊢ (f^[m] ∘ f^[n]) ∘ f = f^[m] ∘ f^[n] ∘ f
Module: Mathlib.Logic.Function.Iterate

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

Tactic:
by rwa [iterate_succ, ← comp_assoc, iterate_invariant h m]

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ f = e.symm.trans g

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ e = g.trans f.symm

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
f : α → γ
g : β → γ
⊢ Sum.elim f g ∘ swap = Sum.elim g f

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
⊢ x.getLeft?.isSome = true ↔ x.isLeft = true

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
⊢ x.getRight?.isSome = true ↔ x.isRight = true

Tactic:
by
  grind

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

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

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isLeft = true
⊢ ∃ a c, r a c ∧ x = inl a ∧ y = inl c

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isRight = true
⊢ ∃ b d, s b d ∧ x = inr b ∧ y = inr d

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
β : Type v
γ : Sort u_3
f : α → γ
g₁ g₂ : β → γ
hg : Sum.elim f g₁ = Sum.elim f g₂
b : β
⊢ g₁ b = g₂ b

Tactic:
simpa using congr_fun hg (Sum.inr b)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
h : Injective (map f g)
b₁ b₂ : β
hb : g b₁ = g b₂
⊢ b₁ = b₂

Tactic:
inhabit α
      injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb :)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this : Nonempty γ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
have := Nonempty.map g ‹_›

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
this✝ : Nonempty γ
this : Nonempty δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝² : Preorder β
inst✝¹ : LE α
inst✝ : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x✝¹ x✝ : α
⊢ x✝¹ < x✝ ↔ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹

Tactic:
rw [← le, ← le, ← lt, lt_iff_le_not_ge]

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:
by
  split <;> solve_by_elim

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤

Tactic:
map_top

Goal state after:
α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
⊢ P (a + 1) b

Tactic:
rcases this with (rfl | h)

Goal state after:
case a.inl
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
⊢ P (a + 1) (a + 1)

case a.inr
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h✝ : a + 1 < b + 1
h : a + 1 < b
⊢ P (a + 1) b
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' ∧ y' ≤ x'

Tactic:
le_iff_le_of_cmp_eq_cmp h,

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.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ min a b ≠ ⊥

Tactic:
by
  grind

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

pp: case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
· have hx : p x := hp h hy
    simpa [hx, hy] using hf h

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a b : α
h : Disjoint a b
ha : a ≠ ⊥
⊢ b ≠ ⊤

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
apply le_antisymm <;> simp

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

Goal state before:
pp: α : Type u_1
a b : α
s : Set α
⊢ insert a (insert b s) = insert b (insert a s)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
x y : β
hp : ∃ a, p a
hn : ∃ a, ¬p a
⊢ (range fun a ↦ if p a then x else y) = {x, y}

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_3
β : Type u_4
a : α
⊢ Prod.fst ⁻¹' {a} = range fun x ↦ (a, x)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_3
β : Type u_4
b : β
⊢ Prod.snd ⁻¹' {b} = range fun x ↦ (x, b)

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ≤ max b c ↔ a ≤ b ∨ a ≤ c

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a < max b c ↔ a < b ∨ a < c

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
s : Set α
x : α
hs : {x}.Nontrivial
H : s = {x}
⊢ False

Tactic:
exact not_nontrivial_singleton hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ

Tactic:
by
  grind

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ≤ f ⊤

Tactic:
map_top

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ f a ≤ ⊤
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s ⊂ t ↔ ∃ a, a ∈ t ∧ s ⊆ t \ {a}

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
h : ¬a ∈ s
⊢ s \ insert a t = s \ t

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
t : Set α
a : α
s : Set α
h : a ∈ t
⊢ insert a s \ t = s \ t

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
t : Set α
a : α
s : Set α
h : ¬a ∈ t
⊢ insert a s \ t = insert a (s \ t)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ s ⊆ insert a t ↔ s ⊆ t ∨ a ∈ s ∧ s \ {a} ⊆ t

Tactic:
by
  grind

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
⊢ GeneralizedHeytingAlgebra α

Tactic:
apply e.injective.generalizedHeytingAlgebra <;> intros <;>
  first | rfl | exact e.apply_symm_apply _

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
⊢ LeftInverse (Sum.elim Int.ofNat Int.negSucc) fun z ↦ Int.casesOn z inl inr

Tactic:
by rintro (m | n) <;> rfl

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
⊢ RightInverse (Sum.elim Int.ofNat Int.negSucc) fun z ↦ Int.casesOn z inl inr

Tactic:
by rintro (m | n) <;> rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊤ = f ⊤

Tactic:
map_top

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊤ = ⊤
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b : α
⊢ (swap a b) b = a

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ x ≠ a → x ≠ b → (swap a b) x = x

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
i j : α
⊢ ⇑(swap i j) = update (update id j i) i j

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
i j : α
f : α → β
⊢ f ∘ ⇑(swap i j) = update (update f j (f i)) i (f j)

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a b : α
e : α ≃ β
⊢ (e.symm.trans (swap a b)).trans e = swap (e a) (e b)

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
i j a : α
⊢ (swap i j) ((swap i j) a) = a

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
v : α → β
i j : α
hv : v i = v j
k : α
⊢ v ((swap i j) k) = v k

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
x y z w : α
⊢ (swap x y) z = w ↔ z = (swap x y) w

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a b x : α
⊢ (swap a b) x ≠ x ↔ a ≠ b ∧ (x = a ∨ x = b)

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y z : α
⊢ f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)

Tactic:
by
  grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
x✝¹ : β → P
x✝ : α
⊢ (piCongrLeft' (fun x ↦ P) e).symm x✝¹ x✝ = (piCongrLeft' (fun a ↦ P) e.symm) x✝¹ x✝

Tactic:
simp [piCongrLeft']

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

Goal state before:
pp: ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π (e (inl i))
g : (i : ι') → π (e (inr i))
i : ι
⊢ (piCongrLeft π e) ((sumPiEquivProdPi fun x ↦ π (e x)).symm (f, g)) (e (inl i)) = f i

Tactic:
by
  grind

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

Goal state before:
pp: ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π (e (inl i))
g : (i : ι') → π (e (inr i))
j : ι'
⊢ (piCongrLeft π e) ((sumPiEquivProdPi fun x ↦ π (e x)).symm (f, g)) (e (inr j)) = g j

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
s t u : Set α
⊢ (s ∪ t) ∆ u ⊆ s ∆ u ∪ t ∆ u

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
s t u : Set α
⊢ s ∆ (t ∪ u) ⊆ s ∆ t ∪ s ∆ u

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u
s t u v : Set α
⊢ (s ∪ t) ∆ (u ∪ v) ⊆ s ∆ u ∪ t ∆ v

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (x : α), f x = g x
⊢ f '' s = g '' s

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_5
β : Type u_6
s : Set α
t : Set β
⊢ (s ×ˢ t)ᶜ = sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint (𝒫 s) (insert a '' 𝒫 s)

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
u : Set α
u_mem : u ∈ 𝒫 s
v : Set α
v_mem : v ∈ 𝒫 s
eq : insert a u = insert a v
⊢ u = v

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ insert (f x) (f '' {x}ᶜ) = range f

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : Set β
⊢ f '' f ⁻¹' t = range f ∩ t

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : Set β
⊢ f '' f ⁻¹' t = t ∩ range f

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (α ⊕ β)
f : α → γ
g : β → γ
⊢ Sum.elim f g '' s = f '' Sum.inl ⁻¹' s ∪ g '' Sum.inr ⁻¹' s

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (f '' s).Nontrivial

Tactic:
exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : ¬a ∈ s
⊢ (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Tactic:
by
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ (f '' s)ᶜ = f '' sᶜ ∪ (range f)ᶜ

Tactic:
by
  grind

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
ht₁ : ∀ (i : ι), ¬i ∈ s₁ → t₁ i = univ
ht₂ : ∀ (i : ι), ¬i ∈ s₂ → t₂ i = univ
⊢ ((s₁ ∪ s₂).pi fun i ↦ t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂

Tactic:
by
  grind

Goal state after: