internlm/Lean-Github huggingface dataset:
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n + b n - (t + u)| = |a n - t + (b n - u)|
Tactic:
apply congrArg
Proof state after:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ a n + b n - (t + u) = a n - t + (b n - u)
Theorem: tends_to_add
Proof state before:
case h
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ a n + b n - (t + u) = a n - t + (b n - u)
Tactic:
ring
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n - t + (b n - u)| ≤ |a n - t| + |b n - u|
Tactic:
exact abs_add (a n - t) (b n - u)
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ |a n - t| + |b n - u| < ε / 2 + ε / 2
Tactic:
exact add_lt_add hNan hNbn
Proof state after:
no goals
Theorem: tends_to_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ ε > 0, ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : tends_to b u
ε : ℝ
hεpos : 0 < ε
Na : ℕ
ha' : ∀ (n : ℕ), Na ≤ n → |a n - t| < ε / 2
Nb : ℕ
hb' : ∀ (n : ℕ), Nb ≤ n → |b n - u| < ε / 2
Nab : ℕ := max Na Nb
n : ℕ
hn : Nab ≤ n
ha'' : Na ≤ n → |a n - t| < ε / 2
hb'' : Nb ≤ n → |b n - u| < ε / 2
hNan : |a n - t| < ε / 2
hNbn : |b n - u| < ε / 2
⊢ ε / 2 + ε / 2 = ε
Tactic:
ring
Proof state after:
no goals
Theorem: tends_to_sub
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
⊢ tends_to (fun n => a n - b n) (t - u)
Tactic:
have hb' := tends_to_neg hb
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
⊢ tends_to (fun n => a n - b n) (t - u)
Theorem: tends_to_sub
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
⊢ tends_to (fun n => a n - b n) (t - u)
Tactic:
have h'  := tends_to_add ha hb'
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
h' : tends_to (fun n => a n + -b n) (t + -u)
⊢ tends_to (fun n => a n - b n) (t - u)
Theorem: tends_to_sub
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : tends_to a t
hb : tends_to b u
hb' : tends_to (fun n => -b n) (-u)
h' : tends_to (fun n => a n + -b n) (t + -u)
⊢ tends_to (fun n => a n - b n) (t - u)
Tactic:
apply h'
Proof state after:
no goals
Theorem: Yb_ne_Yc
Proof state before:
⊢ Y.b ≠ Y.c
Tactic:
intro h
Proof state after:
h : Y.b = Y.c
⊢ False
Theorem: Yb_ne_Yc
Proof state before:
h : Y.b = Y.c
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: gYb_eq_gYc
Proof state before:
⊢ g Y.b = g Y.c
Tactic:
rw [g]
Proof state after:
no goals
Theorem: gf_injective
Proof state before:
⊢ Injective (g ∘ f)
Tactic:
rw [Injective]
Proof state after:
⊢ ∀ ⦃a₁ a₂ : X⦄, (g ∘ f) a₁ = (g ∘ f) a₂ → a₁ = a₂
Theorem: gf_injective
Proof state before:
⊢ ∀ ⦃a₁ a₂ : X⦄, (g ∘ f) a₁ = (g ∘ f) a₂ → a₁ = a₂
Tactic:
intro x₁ x₂ hgf
Proof state after:
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
⊢ x₁ = x₂
Theorem: gf_injective
Proof state before:
x₁ x₂ : X
hgf : (g ∘ f) x₁ = (g ∘ f) x₂
⊢ x₁ = x₂
Tactic:
cases x₁
Proof state after:
case a
x₂ : X
hgf : (g ∘ f) X.a = (g ∘ f) x₂
⊢ X.a = x₂
Theorem: gf_injective
Proof state before:
case a
x₂ : X
hgf : (g ∘ f) X.a = (g ∘ f) x₂
⊢ X.a = x₂
Tactic:
. rfl
Proof state after:
no goals
Theorem: gf_injective
Proof state before:
case a
x₂ : X
hgf : (g ∘ f) X.a = (g ∘ f) x₂
⊢ X.a = x₂
Tactic:
rfl
Proof state after:
no goals
Theorem: gf_surjective
Proof state before:
⊢ Surjective (g ∘ f)
Tactic:
intro z
Proof state after:
z : Z
⊢ ∃ a, (g ∘ f) a = z
Theorem: gf_surjective
Proof state before:
z : Z
⊢ ∃ a, (g ∘ f) a = z
Tactic:
use X.a
Proof state after:
no goals
Theorem: subset_def
Proof state before:
X : Type
A B C D : Set X
x y z : X
⊢ A ⊆ B ↔ ∀ x ∈ A, x ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: mem_union_iff
Proof state before:
X : Type
A B C D : Set X
x y z : X
⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: mem_inter_iff
Proof state before:
X : Type
A B C D : Set X
x y z : X
⊢ x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: inf_le_inf_left'
Proof state before:
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a ⊓ c
Tactic:
apply le_inf
Proof state after:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a

case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Theorem: inf_le_inf_left'
Proof state before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a

case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
. apply inf_le_left
Proof state after:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Theorem: inf_le_inf_left'
Proof state before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
. have h' : a ⊓ b ≤ b :=
    by
    apply inf_le_right
  apply le_trans h' h
Proof state after:
no goals
Theorem: inf_le_inf_left'
Proof state before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ a
Tactic:
apply inf_le_left
Proof state after:
no goals
Theorem: inf_le_inf_left'
Proof state before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
have h' : a ⊓ b ≤ b :=
  by
  apply inf_le_right
Proof state after:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
h' : a ⊓ b ≤ b
⊢ a ⊓ b ≤ c
Theorem: inf_le_inf_left'
Proof state before:
case a
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
h' : a ⊓ b ≤ b
⊢ a ⊓ b ≤ c
Tactic:
apply le_trans h' h
Proof state after:
no goals
Theorem: inf_le_inf_left'
Proof state before:
L : Type
inst✝ : Lattice L
a b c : L
h : b ≤ c
⊢ a ⊓ b ≤ b
Tactic:
apply inf_le_right
Proof state after:
no goals
Theorem: mem_def
Proof state before:
X : Type
P : X → Prop
a : X
⊢ a ∈ {x | P x} ↔ P a
Tactic:
rfl
Proof state after:
no goals
Theorem: tends_to_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
⊢ tends_to (fun n => 37 * a n) (37 * t)
Tactic:
rw [tends_to_def]
Proof state after:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
intro ε hεpos
Proof state after:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
have hεpos' : 0 < ε / 37 :=
  by
  apply div_pos hεpos (by norm_num)
Proof state after:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
have h' := h (ε / 37) hεpos'
Proof state after:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
h' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
h' : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
obtain ⟨N, hN⟩ := h'
Proof state after:
case intro
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
case intro
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 * a n - 37 * t| < ε
Tactic:
use N
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∀ (n : ℕ), N ≤ n → |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
⊢ ∀ (n : ℕ), N ≤ n → |37 * a n - 37 * t| < ε
Tactic:
intro n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
⊢ |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
⊢ |37 * a n - 37 * t| < ε
Tactic:
have h'' := hN n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ |37 * a n - 37 * t| < ε
Theorem: tends_to_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ |37 * a n - 37 * t| < ε
Tactic:
rw [← mul_sub, abs_mul, abs_of_nonneg]
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 37 * |a n - t| < ε

case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37
Theorem: tends_to_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 37 * |a n - t| < ε

case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37
Tactic:
linarith
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37
Theorem: tends_to_thirtyseven_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
hεpos' : 0 < ε / 37
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → |a n - t| < ε / 37
n : ℕ
hn : N ≤ n
h'' : |a n - t| < ε / 37
⊢ 0 ≤ 37
Tactic:
norm_num
Proof state after:
no goals
Theorem: tends_to_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
⊢ 0 < ε / 37
Tactic:
apply div_pos hεpos (by norm_num)
Proof state after:
no goals
Theorem: tends_to_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : tends_to a t
ε : ℝ
hεpos : 0 < ε
⊢ 0 < 37
Tactic:
norm_num
Proof state after:
no goals
Theorem: Finperm.coe_inj
Proof state before:
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
⊢ f = g
Tactic:
ext x
Proof state after:
case toPerm.H
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
x : α
⊢ f.toPerm x = g.toPerm x

case support.a
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
x : α
⊢ x ∈ f.support ↔ x ∈ g.support
Theorem: Finperm.coe_inj
Proof state before:
case support.a
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
x : α
⊢ x ∈ f.support ↔ x ∈ g.support
Tactic:
rw [mem_support_iff, mem_support_iff, ← toPerm_eq_coe, h, toPerm_eq_coe]
Proof state after:
no goals
Theorem: Finperm.coe_inj
Proof state before:
case toPerm.H
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.toPerm = g.toPerm
x : α
⊢ f.toPerm x = g.toPerm x
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Finperm.funext
Proof state before:
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
⊢ f = g
Tactic:
apply coe_inj
Proof state after:
case h
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
⊢ f.toPerm = g.toPerm
Theorem: Finperm.funext
Proof state before:
case h
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
⊢ f.toPerm = g.toPerm
Tactic:
ext x
Proof state after:
case h.H
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
x : α
⊢ f.toPerm x = g.toPerm x
Theorem: Finperm.funext
Proof state before:
case h.H
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : ∀ (x : α), f x = g x
x : α
⊢ f.toPerm x = g.toPerm x
Tactic:
exact h x
Proof state after:
no goals
Theorem: Finperm.funext_support
Proof state before:
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
⊢ f = g
Tactic:
refine funext <| fun x ↦ ?_
Proof state after:
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
⊢ f x = g x
Theorem: Finperm.funext_support
Proof state before:
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
⊢ f x = g x
Tactic:
obtain (hx | hx) := em (x ∈ f.support)
Proof state after:
case inl
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∈ f.support
⊢ f x = g x

case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
⊢ f x = g x
Theorem: Finperm.funext_support
Proof state before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
⊢ f x = g x
Tactic:
have hx' := hx
Proof state after:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx hx' : x ∉ f.support
⊢ f x = g x
Theorem: Finperm.funext_support
Proof state before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx hx' : x ∉ f.support
⊢ f x = g x
Tactic:
rw [h] at hx'
Proof state after:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
hx' : x ∉ g.support
⊢ f x = g x
Theorem: Finperm.funext_support
Proof state before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∉ f.support
hx' : x ∉ g.support
⊢ f x = g x
Tactic:
rw [mem_support_iff, not_not] at hx hx'
Proof state after:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : f x = x
hx' : g x = x
⊢ f x = g x
Theorem: Finperm.funext_support
Proof state before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : f x = x
hx' : g x = x
⊢ f x = g x
Tactic:
rw [hx, hx']
Proof state after:
no goals
Theorem: Finperm.funext_support
Proof state before:
case inl
α : Type u_1
x✝ y : α
f✝ g✝ f g : Finperm α
h : f.support = g.support
h' : ∀ i ∈ f.support, f i = g i
x : α
hx : x ∈ f.support
⊢ f x = g x
Tactic:
rw [h' x hx]
Proof state after:
no goals
Theorem: Finperm.funext_support_subset
Proof state before:
α : Type u_1
x y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
⊢ f = g
Tactic:
refine funext <| fun x ↦ ?_
Proof state after:
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
⊢ f x = g x
Theorem: Finperm.funext_support_subset
Proof state before:
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
⊢ f x = g x
Tactic:
obtain (hx | hx) := em (x ∈ s)
Proof state after:
case inl
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∈ s
⊢ f x = g x

case inr
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ f x = g x
Theorem: Finperm.funext_support_subset
Proof state before:
case inr
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ f x = g x
Tactic:
rw [(show f x = x by simpa using not_mem_mono hf hx),
  (show g x = x by simpa using not_mem_mono hg hx)]
Proof state after:
no goals
Theorem: Finperm.funext_support_subset
Proof state before:
case inl
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∈ s
⊢ f x = g x
Tactic:
exact h _ hx
Proof state after:
no goals
Theorem: Finperm.funext_support_subset
Proof state before:
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ f x = x
Tactic:
simpa using not_mem_mono hf hx
Proof state after:
no goals
Theorem: Finperm.funext_support_subset
Proof state before:
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
s : Finset α
f g : Finperm α
hf : f.support ⊆ s
hg : g.support ⊆ s
h : ∀ i ∈ s, f i = g i
x : α
hx : x ∉ s
⊢ g x = x
Tactic:
simpa using not_mem_mono hg hx
Proof state after:
no goals
Theorem: Finperm.funext_support_iff
Proof state before:
α : Type u_1
x y : α
f✝ g✝ f g : Finperm α
h : f = g
⊢ f.support = g.support ∧ ∀ i ∈ f.support, f i = g i
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Finperm.symm_symm
Proof state before:
α : Type u_1
x y : α
f✝ g f : Finperm α
⊢ f.symm.symm = f
Tactic:
apply coe_inj
Proof state after:
case h
α : Type u_1
x y : α
f✝ g f : Finperm α
⊢ f.symm.symm.toPerm = f.toPerm
Theorem: Finperm.symm_symm
Proof state before:
case h
α : Type u_1
x y : α
f✝ g f : Finperm α
⊢ f.symm.symm.toPerm = f.toPerm
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.support_eq_empty_iff
Proof state before:
α : Type u_1
x y : α
f✝ g f : Finperm α
h : f.support = ∅
⊢ f.support = refl.support
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Finperm.support_eq_empty_iff
Proof state before:
α : Type u_1
x y : α
f✝ g f : Finperm α
h : f.support = ∅
⊢ ∀ i ∈ f.support, f i = refl i
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Finperm.restrict_univ
Proof state before:
α✝¹ : Type u_1
x y : α✝¹
f✝ g : Finperm α✝¹
α✝ : Type u_2
β : Type u_3
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq β
f : Finperm α✝
α : Type u_4
inst✝ : DecidableEq α
⊢ restrict Set.univ = ⊤
Tactic:
ext
Proof state after:
case h
α✝¹ : Type u_1
x y : α✝¹
f✝ g : Finperm α✝¹
α✝ : Type u_2
β : Type u_3
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq β
f : Finperm α✝
α : Type u_4
inst✝ : DecidableEq α
x✝ : Finperm α
⊢ x✝ ∈ restrict Set.univ ↔ x✝ ∈ ⊤
Theorem: Finperm.restrict_univ
Proof state before:
case h
α✝¹ : Type u_1
x y : α✝¹
f✝ g : Finperm α✝¹
α✝ : Type u_2
β : Type u_3
inst✝² : DecidableEq α✝
inst✝¹ : DecidableEq β
f : Finperm α✝
α : Type u_4
inst✝ : DecidableEq α
x✝ : Finperm α
⊢ x✝ ∈ restrict Set.univ ↔ x✝ ∈ ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.mem_restrict_support
Proof state before:
α✝ : Type u_1
x y : α✝
f✝¹ g : Finperm α✝
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ f : Finperm α
⊢ f ∈ restrict ↑f.support
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.swap_self
Proof state before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ swap x x = refl
Tactic:
apply coe_inj
Proof state after:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ (swap x x).toPerm = refl.toPerm
Theorem: Finperm.swap_self
Proof state before:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ (swap x x).toPerm = refl.toPerm
Tactic:
simp only [swap_toPerm, Equiv.swap_self, refl_toPerm]
Proof state after:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ Equiv.refl α = 1
Theorem: Finperm.swap_self
Proof state before:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ Equiv.refl α = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Finperm.swap_support_of_ne
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hxy : x ≠ y
⊢ (swap x y).support = {x, y}
Tactic:
simp [swap, hxy]
Proof state after:
no goals
Theorem: Finperm.swap_comm
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ swap a b = swap b a
Tactic:
rw [funext_support_iff]
Proof state after:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).support = (swap b a).support ∧ ∀ i ∈ (swap a b).support, (swap a b) i = (swap b a) i
Theorem: Finperm.swap_comm
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ (swap a b).support = (swap b a).support ∧ ∀ i ∈ (swap a b).support, (swap a b) i = (swap b a) i
Tactic:
aesop
Proof state after:
no goals
Theorem: Finperm.swap_mul_swap
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
⊢ swap a b * swap a b = 1
Tactic:
obtain (rfl | hne) := eq_or_ne a b
Proof state after:
case inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a : α
⊢ swap a a * swap a a = 1

case inr
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ swap a b * swap a b = 1
Theorem: Finperm.swap_mul_swap
Proof state before:
case inr
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ swap a b * swap a b = 1
Tactic:
apply funext_support_subset (s := {a,b})
Proof state after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b * swap a b).support ⊆ {a, b}

case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ 1.support ⊆ {a, b}

case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ ∀ i ∈ {a, b}, (swap a b * swap a b) i = 1 i
Theorem: Finperm.swap_mul_swap
Proof state before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ ∀ i ∈ {a, b}, (swap a b * swap a b) i = 1 i
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.swap_mul_swap
Proof state before:
case inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a : α
⊢ swap a a * swap a a = 1
Tactic:
simp [one_def]
Proof state after:
no goals