mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod

Tactic:
← one_mul (List.prod _)⁻¹,

Goal state after:
G : Type u_7
inst✝ : Group G
a : G
l : List G
n : ℕ
hl : (take (n % (a :: l).length) (a :: l) ++ drop (n % (a :: l).length) (a :: l)).prod = 1
this : n % (a :: l).length ≤ (a :: l).length
⊢ 1 * (drop (n % (a :: l).length) (a :: l)).prod⁻¹ = (take (n % (a :: l).length) (a :: l)).prod
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
b : α
hb : b ∈ n • {a}
⊢ p b

Tactic:
mem_singleton.mp (mem_of_mem_nsmul hb)

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
b : α
hb : b ∈ n • {a}
⊢ p a
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ n • {a}
⊢ ¬p b

Tactic:
mem_singleton.mp (mem_of_mem_nsmul hb)

Goal state after:
case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ n • {a}
⊢ ¬p a
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case zero
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ countP p (0 • s) = 0 * countP p s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case succ
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n✝ : ℕ
a✝ : countP p (n✝ • s) = n✝ * countP p s
⊢ countP p ((n✝ + 1) • s) = (n✝ + 1) * countP p s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case zero
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a (0 • s) = 0 * count a s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n✝ : ℕ
a✝ : count a (n✝ • s) = n✝ * count a s
⊢ count a ((n✝ + 1) • s) = (n✝ + 1) * count a s

Tactic:
simp [*, succ_nsmul, succ_mul, zero_nsmul]

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
by
  have : ∀ a, ∃ l : List β, f a = l := fun a => Quot.induction_on (f a) fun l => ⟨l, rfl⟩
  choose f' h' using this
  have : f = fun a ↦ ofList (f' a) := funext h'
  have _ : Std.Symm fun a b : List β ↦ List.Disjoint a b := { symm a b h := h.symm }
  exact Quot.induction_on s <| by
    unfold Function.onFun
    simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise]

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).sigma fun a ↦ ↑(l₂ a)) = ↑(l₁.sigma l₂)

Tactic:
rw [Multiset.sigma, List.sigma, ← coe_bind]

Goal state after:
α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).bind fun a ↦ map (Sigma.mk a) ↑(l₂ a)) = (↑l₁).bind fun a ↦ ↑(List.map (Sigma.mk a) (l₂ a))
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)

Tactic:
← Nat.sub_eq_of_eq_add e,

Goal state after:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ (n + 1) * n.choose k - n.choose k * (k + 1) = n.choose k * (n - k)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

Tactic:
· subst h
      rwa [Pi.cons_same]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_7
x✝¹ x✝ : I → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
⊢ ⇑f ∘ 1 = 1

Tactic:
by ext; simp

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝¹ x✝ : I → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
by ext; simp

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

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x = g / mulSingle i (g i) * mulSingle i x

Tactic:
ext j

Goal state after:
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
by
  constructor
  · contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.pow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_pow hn

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f y = f 1 * f y

Tactic:
h1,

Goal state after:
M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y
x y : M
⊢ f y = 1 * f y
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p = ↑q.toSubmonoid
⊢ p = q

Tactic:
coe_toSubmonoid

Goal state after:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p = ↑q
⊢ p = q
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ f.range = map f ⊤

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 * ↑x.2 = ↑y.2
⊢ x = y

Tactic:
← mul_inv_eq_one,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * ↑x.1 * ↑x.2 * (↑y.2)⁻¹ = 1
⊢ x = y
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
⊢ domRestrict 1 M' = 1

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝¹ x✝ : M →* A
⊢ (x✝¹ * x✝).domRestrict M' = x✝¹.domRestrict M' * x✝.domRestrict M'

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective ⇑f
y : ↥N'
x : M
hx : f x = ↑y
⊢ ∃ a, (f.submonoidComap N') a = y

Tactic:
use ⟨x, mem_comap.mpr (hx ▸ y.2)⟩

Goal state after:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
f : M →* N
N' : Submonoid N
hf : Surjective ⇑f
y : ↥N'
x : M
hx : f x = ↑y
⊢ (f.submonoidComap N') ⟨x, ⋯⟩ = y
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ (∃ i, ∃ (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x

Tactic:
simp only [conjugatesOf, isConj_iff, Set.mem_ofPred_eq, exists_prop]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ g (f_inv (x * y)) = g (f_inv x * f_inv y)

Tactic:
← mul_inv_eq_one,

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ g (f_inv (x * y)) * (g (f_inv x * f_inv y))⁻¹ = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x)) = g x

Tactic:
← mul_inv_eq_one,

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ g (f_inv (f x)) * (g x)⁻¹ = 1
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂✝ → 1 ≤ a_1
⊢ l₁✝.prod ≤ (a :: l₂✝).prod

Tactic:
| cons a _ ih' =>

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r s a b → r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

Tactic:
rintro (⟨a, b, hij⟩ | ⟨a, b, hab⟩)

Goal state after:
case mp.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
⊢ r ⟨i✝, a⟩.fst ⟨j✝, b⟩.fst ∨ ∃ h, s ⟨j✝, b⟩.fst (h ▸ ⟨i✝, a⟩.snd) ⟨j✝, b⟩.snd

case mp.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ r ⟨i✝, a⟩.fst ⟨i✝, b⟩.fst ∨ ∃ h, s ⟨i✝, b⟩.fst (h ▸ ⟨i✝, a⟩.snd) ⟨i✝, b⟩.snd
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Total (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
exact Or.inl (Lex.right _ _ hab)

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

Goal state before:
pp: case inr.inl.inl
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hab : s i a b
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
exact Or.inl (Lex.right _ _ hab)

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : a₁ < a₂
⊢ ∃ a, (a₁, b₁) < a ∧ a < (a₂, b₂)

Tactic:
obtain ⟨c, h₁, h₂⟩ := exists_between h
      exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DenselyOrdered α
inst✝ : DenselyOrdered β
⊢ ∀ (a₁ a₂ : Lex (α × β)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro _ _ (@⟨a₁, b₁, a₂, b₂, h⟩ | @⟨a, b₁, b₂, h⟩)
    · obtain ⟨c, h₁, h₂⟩ := exists_between h
      exact ⟨(c, b₁), left _ _ h₁, left _ _ h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := exists_between h
      exact ⟨(a, c), right _ h₁, right _ h₂⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ mrange (FreeMonoid.lift f) = closure (Set.range f)

Tactic:
by
  rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]

Goal state after:
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k ≤ 0
⊢ False

Tactic:
rw [le_zero_eq] at contra

Goal state after:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k = 0
⊢ False
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
suffices ∃ a ∈ @decodeSum α β _ _ n, encodeSum a = bit (bodd n) (div2 n) by
      simpa [bit_bodd_div2]
    simp only [decodeSum, decode_eq_ofNat, Option.map_some, Sum.exists]
    cases bodd n <;> simp [bit_val, encodeSum]

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists = map reverse l.reverse.sublists'

Tactic:
by
  rw [← sublists_reverse, reverse_reverse]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g ((cons c t hc).sup f) = (cons c t hc).sup (g ∘ f)

Tactic:
by
    rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
hxt : x ⊆ t
hxn : #x = n
hsx : s ⊆ x
⊢ #x - #s = n - #s

Tactic:
hxn

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
hxt : x ⊆ t
hxn : #x = n
hsx : s ⊆ x
⊢ n - #s = n - #s
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ map Embedding.some (eraseNone s) = s.erase none

Tactic:
map_eq_image,

Goal state after:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image (⇑Embedding.some) (eraseNone s) = s.erase none
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ max (f a) (s.sup f) ∈ f '' insert a ↑s

Tactic:
rw [sup_eq_left.mpr ha]

Goal state after:
case insert.inr.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s✝ : Finset ι
f : ι → α
a : ι
s : Finset ι
a✝ : a ∉ s
h : s.Nonempty → s.sup f ∈ f '' ↑s
hs✝ : (insert a s).Nonempty
hs : s.Nonempty
ha : s.sup f ≤ f a
⊢ f a ∈ f '' insert a ↑s
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
⊢ ↑(⨅ i ∈ s, f i) ≤ ⨅ i ∈ s, ↑(f i)

Tactic:
by simpa using fun _ ↦ biInf_le _

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
⊢ a < ⨅ i ∈ s, f i

Tactic:
have := hs.ciInf_mem_image _ h

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
this : ⨅ i ∈ s, f i ∈ f '' s
⊢ a < ⨅ i ∈ s, f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
⊢ ∀ (x : Subtype p), f x ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
intro ⟨i, h⟩

Goal state after:
case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this : Nonempty ι
i : ι
h : p i
⊢ f ⟨i, h⟩ ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
hs : BddAbove s
h : sSup ∅ ≤ sSup s
⊢ sSup ∅ ≤ ⨆ i, ↑i

Tactic:
· convert! h
    rw [← sSup_range, Subtype.range_coe]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
⊢ ∀ (x : ↑s), g (f ↑x) ≤ ⨆ i, g ↑i

Tactic:
intro ⟨i, h⟩

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
⊢ g (f ↑⟨i, h⟩) ≤ ⨆ i, g ↑i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)

Tactic:
have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
x✝ : a ⋖ c ∧ c ⋖ b
hac : a ⋖ c
hcb : c ⋖ b
⊢ Ioo a b = {c}

Tactic:
rw [← Ioc_union_Ico_eq_Ioo hac.lt hcb.lt, hac.Ioc_eq, hcb.Ico_eq, union_self]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ (a₁, b) ⩿ (a₂, b) ∧ (a₁, b) < (a₂, b) ↔ a₁ ⩿ a₂ ∧ a₁ < a₂

Tactic:
mk_wcovBy_mk_iff_left,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b : β
⊢ a₁ ⩿ a₂ ∧ (a₁, b) < (a₂, b) ↔ a₁ ⩿ a₂ ∧ a₁ < a₂
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ a₂ : α
b₁ : β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂

Tactic:
· exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
⊢ False

Tactic:
have hcb : Function.update a i ci ≤ b := by simpa [update_le_iff, h₂.le] using fun j hj ↦ h.1 j

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update a i ci ≤ b
⊢ False
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯

Tactic:
map_eq_image,

Goal state after:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ image (⇑f) s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
g : β → α
s : Finset α
hgf : LeftInvOn g f ↑s
ginj : InjOn g (g ⁻¹' ↑s)
⊢ image f s = s.preimage g ginj

Tactic:
by
  simp only [SetLike.ext'_iff, coe_preimage, coe_image]
  rw [Set.image_eq_preimage_of_leftInvOn_injOn hgf ginj]

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
map_eq_image,

Goal state after:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ image (⇑f) t ↔ ∃ u ⊆ t, s = image (⇑f) u
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: case h
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
b : α
⊢ b ≤ a

Tactic:
obtain ⟨c, hc, hbc⟩ := hs' b

Goal state after:
case h
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun x ↦ x ∈ s) a
b c : α
hc : c ∈ s
hbc : b ≤ c
⊢ b ≤ a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : LocallyFiniteOrderTop α
inst✝² : One α
inst✝¹ : IsBotOneClass α
inst✝ : Fintype α
⊢ Ici 1 = univ

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ (Set.Ioo a b).Nonempty ↔ a < b

Tactic:
Set.nonempty_Ioo

Goal state after:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ a < b ↔ a < b