internlm/Lean-Github huggingface dataset:
Theorem: Nat.Combination_compl_bijective
Proof state before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ ∃ a, (Combination_compl G α hm) a = { val := s, property := hs }
Tactic:
have hn : n + m = Fintype.card α := by rw [add_comm]; exact hm
Proof state after:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ ∃ a, (Combination_compl G α hm) a = { val := s, property := hs }
Theorem: Nat.Combination_compl_bijective
Proof state before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ ∃ a, (Combination_compl G α hm) a = { val := s, property := hs }
Tactic:
use Nat.Combination_compl G α hn ⟨s, hs⟩
Proof state after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs }) = { val := s, property := hs }
Theorem: Nat.Combination_compl_bijective
Proof state before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs }) = { val := s, property := hs }
Tactic:
apply Subtype.coe_injective
Proof state after:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (fun a => ↑a) ((Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs })) =
    (fun a => ↑a) { val := s, property := hs }
Theorem: Nat.Combination_compl_bijective
Proof state before:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ (fun a => ↑a) ((Combination_compl G α hm) ((Combination_compl G α hn) { val := s, property := hs })) =
    (fun a => ↑a) { val := s, property := hs }
Tactic:
change sᶜᶜ = s
Proof state after:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ sᶜᶜ = s
Theorem: Nat.Combination_compl_bijective
Proof state before:
case h.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
hn : n + m = Fintype.card α
⊢ sᶜᶜ = s
Tactic:
rw [compl_compl]
Proof state after:
no goals
Theorem: Nat.Combination_compl_bijective
Proof state before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ n + m = Fintype.card α
Tactic:
rw [add_comm]
Proof state after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ m + n = Fintype.card α
Theorem: Nat.Combination_compl_bijective
Proof state before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : Finset α
hs : s ∈ Combination α m
⊢ m + n = Fintype.card α
Tactic:
exact hm
Proof state after:
no goals
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Bijective ⇑(toCombination_one_equivariant G α)
Tactic:
constructor
Proof state after:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Injective ⇑(toCombination_one_equivariant G α)

case right
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Surjective ⇑(toCombination_one_equivariant G α)
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Injective ⇑(toCombination_one_equivariant G α)
Tactic:
intro a b h
Proof state after:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h : (toCombination_one_equivariant G α) a = (toCombination_one_equivariant G α) b
⊢ a = b
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h : (toCombination_one_equivariant G α) a = (toCombination_one_equivariant G α) b
⊢ a = b
Tactic:
simp only [toCombination_one_equivariant, Combination.eq_iff] at h
Proof state after:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ a = b
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ a = b
Tactic:
apply Finset.singleton_injective
Proof state after:
case left.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ {a} = {b}
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case left.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ {a} = {b}
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case right
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Surjective ⇑(toCombination_one_equivariant G α)
Tactic:
rintro ⟨s, hs⟩
Proof state after:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }
Tactic:
simp [Nat.Combination.mem_iff, Finset.card_eq_one] at hs
Proof state after:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs✝ : s ∈ Combination α 1
hs : ∃ a, s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs✝ }
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs✝ : s ∈ Combination α 1
hs : ∃ a, s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs✝ }
Tactic:
obtain ⟨a, ha⟩ := hs
Proof state after:
case right.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case right.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }
Tactic:
use a
Proof state after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ (toCombination_one_equivariant G α) a = { val := s, property := hs }
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ (toCombination_one_equivariant G α) a = { val := s, property := hs }
Tactic:
simp only [toCombination_one_equivariant, ha]
Proof state after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ { toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a = { val := {a}, property := ⋯ }
Theorem: Nat.bijective_toCombination_one_equivariant
Proof state before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ { toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a = { val := {a}, property := ⋯ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.image_smul_setₑ
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ ⇑f '' (m • s) = φ m • ⇑f '' s
Tactic:
change f.toFun '' ((fun a => m • a) '' s) = (fun b => φ m • b) '' (f.toFun '' s)
Proof state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ f.toFun '' ((fun a => m • a) '' s) = (fun b => φ m • b) '' (f.toFun '' s)
Theorem: Set.image_smul_setₑ
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ f.toFun '' ((fun a => m • a) '' s) = (fun b => φ m • b) '' (f.toFun '' s)
Tactic:
simp only [Set.image_image]
Proof state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ (fun x => f.toFun (m • x)) '' s = (fun x => φ m • f.toFun x) '' s
Theorem: Set.image_smul_setₑ
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ (fun x => f.toFun (m • x)) '' s = (fun x => φ m • f.toFun x) '' s
Tactic:
apply Set.image_congr
Proof state after:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ ∀ a ∈ s, f.toFun (m • a) = φ m • f.toFun a
Theorem: Set.image_smul_setₑ
Proof state before:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
⊢ ∀ a ∈ s, f.toFun (m • a) = φ m • f.toFun a
Tactic:
intro a _
Proof state after:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
a : α
a✝ : a ∈ s
⊢ f.toFun (m • a) = φ m • f.toFun a
Theorem: Set.image_smul_setₑ
Proof state before:
case h
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝¹ : SMul M α
inst✝ : SMul N β
f : α →ₑ[φ] β
m : M
s : Set α
a : α
a✝ : a ∈ s
⊢ f.toFun (m • a) = φ m • f.toFun a
Tactic:
rw [f.map_smul']
Proof state after:
no goals
Theorem: Set.image_smul_set
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type u_5
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
s : Set α
⊢ ⇑f₁ '' (m • s) = m • ⇑f₁ '' s
Tactic:
simp
Proof state after:
no goals
Theorem: Set.preimage_smul_setₑ_le
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
⊢ m • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (φ m • t)
Tactic:
rintro x ⟨y, hy, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
y : α
hy : y ∈ ⇑f ⁻¹' t
⊢ (fun x => m • x) y ∈ ⇑f ⁻¹' (φ m • t)
Theorem: Set.preimage_smul_setₑ_le
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
y : α
hy : y ∈ ⇑f ⁻¹' t
⊢ (fun x => m • x) y ∈ ⇑f ⁻¹' (φ m • t)
Tactic:
refine ⟨f y, hy, (by rw [map_smulₛₗ])⟩
Proof state after:
no goals
Theorem: Set.preimage_smul_setₑ_le
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.2413
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
t : Set β
y : α
hy : y ∈ ⇑f ⁻¹' t
⊢ (fun x => φ m • x) (f y) = f ((fun x => m • x) y)
Tactic:
rw [map_smulₛₗ]
Proof state after:
no goals
Theorem: Set.preimage_smul_setₑ'
Proof state before:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ ⇑f ⁻¹' (φ m • t) = m • ⇑f ⁻¹' t
Tactic:
apply Set.Subset.antisymm
Proof state after:
case h₁
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ ⇑f ⁻¹' (φ m • t) ⊆ m • ⇑f ⁻¹' t

case h₂
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ m • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (φ m • t)
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₂
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ m • ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (φ m • t)
Tactic:
exact preimage_smul_setₑ_le t
Proof state after:
no goals
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
⊢ ⇑f ⁻¹' (φ m • t) ⊆ m • ⇑f ⁻¹' t
Tactic:
rintro x ⟨y, yt, hy⟩
Proof state after:
case h₁.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : (fun x => φ m • x) y = f x
⊢ x ∈ m • ⇑f ⁻¹' t
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : (fun x => φ m • x) y = f x
⊢ x ∈ m • ⇑f ⁻¹' t
Tactic:
dsimp at hy
Proof state after:
case h₁.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
⊢ x ∈ m • ⇑f ⁻¹' t
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
⊢ x ∈ m • ⇑f ⁻¹' t
Tactic:
obtain ⟨x', hx' : m • x' = x⟩ := hmα.surjective x
Proof state after:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x ∈ m • ⇑f ⁻¹' t
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x ∈ m • ⇑f ⁻¹' t
Tactic:
refine ⟨x',  ?_, hx'⟩
Proof state after:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x' ∈ ⇑f ⁻¹' t
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
hy : φ m • y = f x
x' : α
hx' : m • x' = x
⊢ x' ∈ ⇑f ⁻¹' t
Tactic:
simp only [← hx', map_smulₛₗ] at hy
Proof state after:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ x' ∈ ⇑f ⁻¹' t
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ x' ∈ ⇑f ⁻¹' t
Tactic:
simp only [mem_preimage]
Proof state after:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ f x' ∈ t
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ f x' ∈ t
Tactic:
rw [← hmβ.injective hy]
Proof state after:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ y ∈ t
Theorem: Set.preimage_smul_setₑ'
Proof state before:
case h₁.intro.intro.intro
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
φ : M → N
inst✝² : SMul M α
inst✝¹ : SMul N β
f : α →ₑ[φ] β
β₁ : Type ?u.4258
inst✝ : SMul M β₁
f₁ : α →ₑ[id] β₁
m : M
hmα : Function.Bijective fun a => m • a
hmβ : Function.Bijective fun b => φ m • b
t : Set β
x : α
y : β
yt : y ∈ t
x' : α
hx' : m • x' = x
hy : φ m • y = φ m • f x'
⊢ y ∈ t
Tactic:
exact yt
Proof state after:
no goals
Theorem: isPretransitive.of_surjective_map
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ IsPretransitive N β
Tactic:
apply MulAction.IsPretransitive.mk
Proof state after:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ ∀ (x y : β), ∃ g, g • x = y
Theorem: isPretransitive.of_surjective_map
Proof state before:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
⊢ ∀ (x y : β), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
α✝ : Type u_1
β✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
φ✝ : M✝ → N✝
inst✝⁵ : SMul M✝ α✝
inst✝⁴ : SMul N✝ β✝
f✝ : α✝ →ₑ[φ✝] β✝
M : Type u_8
inst✝³ : Group M
α : Type u_6
inst✝² : MulAction M α
N : Type u_7
β : Type u_5
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x y : β
⊢ ∃ g, g • x = y