harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Hall/Finite.lean
theorem hall_cond_of_restrict {ι : Type u} {t : ι → Finset α} {s : Finset ι}
    (ht : ∀ s : Finset ι, #s ≤ #(s.biUnion t)) (s' : Finset (s : Set ι)) :
    #s' ≤ #(s'.biUnion fun a' => t a')

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #s' ≤ #(s'.biUnion fun a' => t ↑a')

Tactic:
rw [← card_image_of_injective s' Subtype.coe_injective]

Result:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #(image (fun a => ↑a) s') ≤ #(s'.biUnion fun a' => t ↑a')

Proof state:
case h.e'_4.h
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ (s'.biUnion fun a' => t ↑a') = (image (fun z => ↑z) s').biUnion t

Tactic:
ext y

Result:
case h.e'_4.h.h
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
y : α
⊢ (y ∈ s'.biUnion fun a' => t ↑a') ↔ y ∈ (image (fun z => ↑z) s').biUnion t

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #s' ≤ #(s'.biUnion fun a' => t ↑a')

Tactic:
classical
  rw [← card_image_of_injective s' Subtype.coe_injective]
  convert ht (s'.image fun z => z.1) using 1
  apply congr_arg
  ext y
  simp

Result:
no goals

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #(image (fun a => ↑a) s') ≤ #(s'.biUnion fun a' => t ↑a')

Tactic:
convert ht (s'.image fun z => z.1) using 1

Result:
case h.e'_4
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #(s'.biUnion fun a' => t ↑a') = #((image (fun z => ↑z) s').biUnion t)

Proof state:
case h.e'_4
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ #(s'.biUnion fun a' => t ↑a') = #((image (fun z => ↑z) s').biUnion t)

Tactic:
apply congr_arg

Result:
case h.e'_4.h
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
⊢ (s'.biUnion fun a' => t ↑a') = (image (fun z => ↑z) s').biUnion t

Proof state:
case h.e'_4.h.h
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑↑s
y : α
⊢ (y ∈ s'.biUnion fun a' => t ↑a') ↔ y ∈ (image (fun z => ↑z) s').biUnion t

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/NatAntidiagonal.lean
theorem antidiagonal_succ' (n : ℕ) :
    antidiagonal (n + 1) =
      cons (n + 1, 0)
        ((antidiagonal n).map
          (Embedding.prodMap (Embedding.refl _) ⟨Nat.succ, Nat.succ_injective⟩))
        (by simp)

Proof state:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val

Tactic:
exact Multiset.Nat.antidiagonal_succ'

Result:
no goals

Proof state:
n : ℕ
⊢ antidiagonal (n + 1) =
    cons (n + 1, 0)
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯

Tactic:
apply eq_of_veq

Result:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (n + 1, 0)
        (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯).val

Proof state:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (n + 1, 0)
        (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯).val

Tactic:
rw [cons_val, map_val]

Result:
case a
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val

Proof state:
n : ℕ
⊢ (n + 1, 0) ∉ map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma ih₂₁ (ih' : ∀ a, ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : IH24 x₂ x₁ y := ih₁₂ <| by
  simp_rw [ArgsRel, InvImage, Args.toMultiset, Multiset.pair_comm] at ih' ⊢
  suffices {x₁, y, x₂} = {x₂, y, x₁} by rwa [← this]
  dsimp only [Multiset.insert_eq_cons, ← Multiset.singleton_add] at ih' ⊢
  abel

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ ∀ (a : Args), ArgsRel a (Args.P24 x₂ x₁ y) → P124 a

Tactic:
simp_rw [ArgsRel, InvImage, Args.toMultiset, Multiset.pair_comm] at ih' ⊢

Result:
x₁ x₂ y : PGame
ih' :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₁, y, x₂} →
      P124 a
⊢ ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₂, y, x₁} →
      P124 a

Proof state:
x₁ x₂ y : PGame
ih' :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₁, y, x₂} →
      P124 a
this : {x₁, y, x₂} = {x₂, y, x₁}
⊢ ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₂, y, x₁} →
      P124 a

Tactic:
rwa [← this]

Result:
no goals

Proof state:
x₁ x₂ y : PGame
ih' :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₁, y, x₂} →
      P124 a
⊢ {x₁, y, x₂} = {x₂, y, x₁}

Tactic:
dsimp only [Multiset.insert_eq_cons, ← Multiset.singleton_add] at ih' ⊢

Result:
x₁ x₂ y : PGame
ih' :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y} + {x}
        | Args.P24 x₁ x₂ y => {x₁} + ({y} + {x₂}))
        ({x₁} + ({y} + {x₂})) →
      P124 a
⊢ {x₁} + ({y} + {x₂}) = {x₂} + ({y} + {x₁})

Proof state:
x₁ x₂ y : PGame
ih' :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₁, y, x₂} →
      P124 a
⊢ ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₂, y, x₁} →
      P124 a

Tactic:
suffices {x₁, y, x₂} = {x₂, y, x₁} by rwa [← this]

Result:
x₁ x₂ y : PGame
ih' :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y, x}
        | Args.P24 x₁ x₂ y => {x₁, y, x₂})
        {x₁, y, x₂} →
      P124 a
⊢ {x₁, y, x₂} = {x₂, y, x₁}

Proof state:
x₁ x₂ y : PGame
ih' :
  ∀ (a : Args),
    TransGen (CutExpand IsOption)
        (match a with
        | Args.P1 x y => {y} + {x}
        | Args.P24 x₁ x₂ y => {x₁} + ({y} + {x₂}))
        ({x₁} + ({y} + {x₂})) →
      P124 a
⊢ {x₁} + ({y} + {x₂}) = {x₂} + ({y} + {x₁})

Tactic:
abel

Result:
no goals
-- Mathlib/Algebra/Homology/AlternatingConst.lean
/-- The `n`-th homology of the alternating constant complex is `X` for `n ≠ 0`. -/
lemma alternatingConst_exactAt (X : C) (n : ℕ) (hn : n ≠ 0) :
    (alternatingConst.obj X).ExactAt n

Proof state:
case inr
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
exact ⟨(alternatingConstHomologyDataOdd X _ h), isZero_zero C⟩

Result:
no goals

Proof state:
case inl
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
exact ⟨(alternatingConstHomologyDataEvenNEZero X _ h hn), isZero_zero C⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
rcases n.even_or_odd with h | h

Result:
case inl
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

case inr
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_cons :
    (x :: xs : List α).dropWhile p = if p x then xs.dropWhile p else x :: xs

Proof state:
α : Type u_1
x : α
xs : List α
p : α → Bool
⊢ dropWhile p (x :: xs) = if p x = true then dropWhile p xs else x :: xs

Tactic:
split <;> simp_all [dropWhile]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudoZero_aux {P : C} (Q : C) (f : Over P) : f ≈ (0 : Q ⟶ P) ↔ f.hom = 0 :=
  ⟨fun ⟨R, p, q, _, _, comm⟩ => zero_of_epi_comp p (by simp [comm]), fun hf =>
    ⟨biprod f.1 Q, biprod.fst, biprod.snd, inferInstance, inferInstance, by
      rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]⟩⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
x✝ : f ≈ Over.mk 0
R : C
p : R ⟶ f.left
q : R ⟶ (Over.mk 0).left
w✝¹ : Epi p
w✝ : Epi q
comm : p ≫ f.hom = q ≫ (Over.mk 0).hom
⊢ p ≫ f.hom = 0

Tactic:
simp [comm]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ biprod.fst ≫ f.hom = biprod.snd ≫ (Over.mk 0).hom

Tactic:
rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
lemma specializingMap_iff_closure_singleton_subset :
    SpecializingMap f ↔ ∀ x, closure {f x} ⊆ f '' closure {x}

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}

Tactic:
simp only [SpecializingMap, Relation.Fibration, flip, specializes_iff_mem_closure]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ ⦃a : X⦄ ⦃b : Y⦄, b ∈ closure {f a} → ∃ a' ∈ closure {a}, f a' = b) ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ ⦃a : X⦄ ⦃b : Y⦄, b ∈ closure {f a} → ∃ a' ∈ closure {a}, f a' = b) ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_mono {s t : Set X} (h : s ⊆ t) : dimH s ≤ dimH t

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s t : Set X
h : s ⊆ t
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s ≤ dimH t

Tactic:
exact dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top <| top_unique <| hd ▸ measure_mono h

Result:
no goals

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s t : Set X
h : s ⊆ t
⊢ dimH s ≤ dimH t

Tactic:
borelize X

Result:
X : Type u_2
inst✝ : EMetricSpace X
s t : Set X
h : s ⊆ t
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ dimH s ≤ dimH t
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem nhds_mul (x y : G) : 𝓝 (x * y) = 𝓝 x * 𝓝 y :=
  calc
    𝓝 (x * y) = map (x * ·) (map (· * y) (𝓝 1 * 𝓝 1))

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map (fun x_1 => x * x_1) (map (fun x => x * y) (𝓝 1 * 𝓝 1)) = map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1)

Tactic:
rw [← map₂_mul, map_map₂, map_map₂]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ 𝓝 (x * y) = map (fun x_1 => x * x_1) (map (fun x => x * y) (𝓝 1 * 𝓝 1))

Tactic:
simp

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1) = 𝓝 x * 𝓝 y

Tactic:
rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
  map₂_map_right]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1)

Tactic:
simp only [mul_assoc]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem intValuation_le_one (x : R) : v.intValuationDef x ≤ 1

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x = 0
⊢ 0 ≤ 1

Tactic:
exact WithZero.zero_le 1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
⊢ (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) ≤ 1

Tactic:
by_cases hx : x = 0

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x = 0
⊢ (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) ≤ 1

case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : ¬x = 0
⊢ (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) ≤ 1

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x = 0
⊢ (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) ≤ 1

Tactic:
rw [if_pos hx]

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x = 0
⊢ 0 ≤ 1

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : ¬x = 0
⊢ (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) ≤ 1

Tactic:
rw [if_neg hx, ← WithZero.coe_one, ← ofAdd_zero, WithZero.coe_le_coe, ofAdd_le,
  Right.neg_nonpos_iff]

Result:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : ¬x = 0
⊢ 0 ≤ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
⊢ v.intValuationDef x ≤ 1

Tactic:
rw [intValuationDef]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
⊢ (if x = 0 then 0 else ↑(ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)))) ≤ 1

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : ¬x = 0
⊢ 0 ≤ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)

Tactic:
exact Int.natCast_nonneg _

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma divConst_empty_right (A : Finset G) : δₘ[A, ∅] = 0

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
⊢ δₘ[A, ∅] = 0

Tactic:
simp [divConst]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem ncard_block_eq_relindex (hB : IsBlock G B) {x : X} (hx : x ∈ B) :
    B.ncard = (stabilizer G x).relindex (stabilizer G B)

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (↥(stabilizer G B)) x
⊢ B.ncard = (stabilizer G x).relindex (stabilizer G B)

Tactic:
rw [Subgroup.relindex, key, index_stabilizer, hB.orbit_stabilizer_eq hx]

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ B.ncard = (stabilizer G x).relindex (stabilizer G B)

Tactic:
have key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (stabilizer G B) x := by
  ext; rfl

Result:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
key : (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (↥(stabilizer G B)) x
⊢ B.ncard = (stabilizer G x).relindex (stabilizer G B)

Proof state:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
x✝ : ↥(stabilizer G B)
⊢ x✝ ∈ (stabilizer G x).subgroupOf (stabilizer G B) ↔ x✝ ∈ stabilizer (↥(stabilizer G B)) x

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
⊢ (stabilizer G x).subgroupOf (stabilizer G B) = stabilizer (↥(stabilizer G B)) x

Tactic:
ext

Result:
case h
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hB : IsBlock G B
x : X
hx : x ∈ B
x✝ : ↥(stabilizer G B)
⊢ x✝ ∈ (stabilizer G x).subgroupOf (stabilizer G B) ↔ x✝ ∈ stabilizer (↥(stabilizer G B)) x
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_div_self (ha : 0 ≤ a) (hb₀ : 0 < b) (hb₁ : b ≤ 1) : a ≤ a / b

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 ≤ a
hb₀ : 0 < b
hb₁ : b ≤ 1
⊢ a ≤ a / b

Tactic:
simpa only [div_one] using div_le_div_of_nonneg_left ha hb₀ hb₁

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
@[simp] lemma comp_zero (κ : Kernel β γ) : κ ∘ₖ (0 : Kernel α β) = 0

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ∘ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [comp_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
⊢ κ ∘ₖ 0 = 0

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel β γ
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((κ ∘ₖ 0) a✝¹) s✝ = (0 a✝¹) s✝
-- Mathlib/Data/Ordmap/Ordset.lean
theorem length_toList' : ∀ t : Ordnode α, (toList t).length = t.realSize
  | nil => rfl
  | node _ l _ r => by
    rw [toList_node, List.length_append, List.length_cons, length_toList' l,
        length_toList' r]; rfl

Proof state:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ l.realSize + (r.realSize + 1) = (node size✝ l x✝ r).realSize

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ (node size✝ l x✝ r).toList.length = (node size✝ l x✝ r).realSize

Tactic:
rw [toList_node, List.length_append, List.length_cons, length_toList' l,
    length_toList' r]

Result:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
⊢ l.realSize + (r.realSize + 1) = (node size✝ l x✝ r).realSize
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicInterior_nonempty (hs : Convex ℝ s) :
    (intrinsicInterior ℝ s).Nonempty ↔ s.Nonempty :=
  ⟨by simp_rw [nonempty_iff_ne_empty]; rintro h rfl; exact h intrinsicInterior_empty,
    Set.Nonempty.intrinsicInterior hs⟩

Proof state:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ (intrinsicInterior ℝ s).Nonempty → s.Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty]

Result:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅

Proof state:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hs : Convex ℝ ∅
h : intrinsicInterior ℝ ∅ ≠ ∅
⊢ False

Tactic:
exact h intrinsicInterior_empty

Result:
no goals

Proof state:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ intrinsicInterior ℝ s ≠ ∅ → s ≠ ∅

Tactic:
rintro h rfl

Result:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hs : Convex ℝ ∅
h : intrinsicInterior ℝ ∅ ≠ ∅
⊢ False
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem zero_measure (f : α → α) : @PreErgodic α m f 0 where
  aeconst_set _ _ _

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
x✝² : Set α
x✝¹ : MeasurableSet x✝²
x✝ : f ⁻¹' x✝² = x✝²
⊢ EventuallyConst x✝² (ae 0)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/HomCongr.lean
theorem map_isoCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ≅ Y) :
    F.mapIso (Iso.isoCongr α β f) = Iso.isoCongr (F.mapIso α) (F.mapIso β) (F.mapIso f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ≅ Y
⊢ F.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)

Tactic:
ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ≅ Y
⊢ (F.mapIso ((α.isoCongr β) f)).hom = (((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)).hom

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ≅ Y
⊢ (F.mapIso ((α.isoCongr β) f)).hom = (((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.card_part_eq_average_iff (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
    #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
h : #t = #s / #P.parts ∧ #t = #s / #P.parts + 1
⊢ False

Tactic:
exact absurd (h.1 ▸ h.2) (lt_add_one _).ne

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Tactic:
have b : ¬(#t = #s / #P.parts ∧ #t = #s / #P.parts + 1) := by
  by_contra h; exact absurd (h.1 ▸ h.2) (lt_add_one _).ne

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
b : ¬(#t = #s / #P.parts ∧ #t = #s / #P.parts + 1)
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
b : ¬(#t = #s / #P.parts ∧ #t = #s / #P.parts + 1)
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Tactic:
have a := hP.card_parts_eq_average ht

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
⊢ #t = #s / #P.parts ↔ #t ≠ #s / #P.parts + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
⊢ ¬(#t = #s / #P.parts ∧ #t = #s / #P.parts + 1)

Tactic:
by_contra h

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
a : #t = #s / #P.parts ∨ #t = #s / #P.parts + 1
h : #t = #s / #P.parts ∧ #t = #s / #P.parts + 1
⊢ False