harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/Log.lean
theorem self_le_zpow_clog {b : ℕ} (hb : 1 < b) (r : R) : r ≤ (b : R) ^ clog b r

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r ≤ ↑b ^ clog b r

Tactic:
rw [← neg_log_inv_eq_clog, zpow_neg, le_inv_comm₀ hr (zpow_pos ..)]

Result:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ ↑b ^ log b r⁻¹ ≤ r⁻¹

R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ 0 < ↑b

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
⊢ r ≤ ↑b ^ clog b r

Tactic:
rcases le_or_lt r 0 with hr | hr

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ ↑b ^ clog b r

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ r ≤ ↑b ^ clog b r

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ ↑b ^ clog b r

Tactic:
rw [clog_of_right_le_zero _ hr, zpow_zero]

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ 1

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ ↑b ^ log b r⁻¹ ≤ r⁻¹

Tactic:
exact zpow_log_le_self hb (inv_pos.mpr hr)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : 0 < r
⊢ 0 < ↑b

Tactic:
exact Nat.cast_pos.mpr (zero_le_one.trans_lt hb)

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
r : R
hr : r ≤ 0
⊢ r ≤ 1

Tactic:
exact hr.trans zero_le_one

Result:
no goals
-- Mathlib/Logic/Small/Defs.lean
theorem not_small_type : ¬Small.{u} (Type max u v)
  | ⟨⟨S, ⟨e⟩⟩⟩ =>
    @Function.cantor_injective (Σα, e.symm α) (fun a => ⟨_, cast (e.3 _).symm a⟩) fun a b e => by
      dsimp at e
      injection e with h₁ h₂
      simpa using h₂

Proof state:
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × e✝.symm α)
e : ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩ = ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ b⟩
⊢ a = b

Tactic:
injection e with h₁ h₂

Result:
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × e.symm α)
h₁ : e (Set ((α : S) × e.symm α)) = e (Set ((α : S) × e.symm α))
h₂ : cast ⋯ a = cast ⋯ b
⊢ a = b

Proof state:
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × e.symm α)
h₁ : e (Set ((α : S) × e.symm α)) = e (Set ((α : S) × e.symm α))
h₂ : cast ⋯ a = cast ⋯ b
⊢ a = b

Tactic:
simpa using h₂

Result:
no goals

Proof state:
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × e✝.symm α)
e :
  (fun a => ⟨e✝.toFun (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩) a =
    (fun a => ⟨e✝.toFun (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩) b
⊢ a = b

Tactic:
dsimp at e

Result:
S : Type u
e✝ : Type (max u v) ≃ S
a b : Set ((α : S) × e✝.symm α)
e : ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ a⟩ = ⟨e✝ (Set ((α : S) × e✝.symm α)), cast ⋯ b⟩
⊢ a = b
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P2_neg_right : P2 x₁ x₂ y ↔ P2 x₁ x₂ (-y)

Proof state:
x₁ x₂ y : PGame
⊢ P2 x₁ x₂ y ↔ P2 x₁ x₂ (-y)

Tactic:
rw [P2, P2, quot_mul_neg, quot_mul_neg, neg_inj]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem add_eq_top_iff {a b : PartENat} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Proof state:
case refine_2.refine_2
a b : PartENat
⊢ ∀ (n n_1 : ℕ), ¬↑n_1 + ↑n = ⊤

Tactic:
simp only [← Nat.cast_add, PartENat.natCast_ne_top, forall_const, not_false_eq_true]

Result:
no goals

Proof state:
a b : PartENat
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
refine PartENat.casesOn a ?_ ?_
<;> refine PartENat.casesOn b ?_ ?_
<;> simp [top_add, add_top]

Result:
case refine_2.refine_2
a b : PartENat
⊢ ∀ (n n_1 : ℕ), ¬↑n_1 + ↑n = ⊤
-- Mathlib/Tactic/DeriveEncodable.lean
private lemma nat_unpair_lt_2 {n : ℕ} (h : (Nat.unpair n).1 ≠ 0) : (Nat.unpair n).2 < n

Proof state:
case intro.mk
a b : ℕ
h : a ≠ 0
⊢ b < if a < b then b * b + a else a * a + a + b

Tactic:
have := Nat.le_mul_self a

Result:
case intro.mk
a b : ℕ
h : a ≠ 0
this : a ≤ a * a
⊢ b < if a < b then b * b + a else a * a + a + b

Proof state:
case intro.mk
a b : ℕ
h : a ≠ 0
this : a ≤ a * a
⊢ b < if a < b then b * b + a else a * a + a + b

Tactic:
have := Nat.le_mul_self b

Result:
case intro.mk
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
⊢ b < if a < b then b * b + a else a * a + a + b

Proof state:
case intro.mk
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
⊢ b < if a < b then b * b + a else a * a + a + b

Tactic:
split <;> omega

Result:
no goals

Proof state:
case intro.mk
a b : ℕ
h : a ≠ 0
⊢ b < Nat.pair a b

Tactic:
unfold Nat.pair

Result:
case intro.mk
a b : ℕ
h : a ≠ 0
⊢ b < if a < b then b * b + a else a * a + a + b

Proof state:
n : ℕ
h : (Nat.unpair n).1 ≠ 0
⊢ (Nat.unpair n).2 < n

Tactic:
obtain ⟨⟨a, b⟩, rfl⟩ := Nat.pairEquiv.surjective n

Result:
case intro.mk
a b : ℕ
h : (Nat.unpair (Nat.pairEquiv (a, b))).1 ≠ 0
⊢ (Nat.unpair (Nat.pairEquiv (a, b))).2 < Nat.pairEquiv (a, b)

Proof state:
case intro.mk
a b : ℕ
h : (Nat.unpair (Nat.pairEquiv (a, b))).1 ≠ 0
⊢ (Nat.unpair (Nat.pairEquiv (a, b))).2 < Nat.pairEquiv (a, b)

Tactic:
simp only [Nat.pairEquiv_apply, Function.uncurry_apply_pair, Nat.unpair_pair] at *

Result:
case intro.mk
a b : ℕ
h : a ≠ 0
⊢ b < Nat.pair a b
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem image_Ioo (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Ioo x y = Ioo (e x) (e y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ioo x y = Ioo (e x) (e y)

Tactic:
rw [← e.preimage_Ioo, image_preimage_eq_inter_range,
  inter_eq_left.2 <| Ioo_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
lemma shiftIso_add'_inv_app (n m mn : M) (hnm : m + n = mn) (a a' a'' : M)
    (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).inv.app X =
      (shiftIso F m a' a'' ha'').inv.app X ≫
        (shiftIso F n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫
        (shift F a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X)

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.61736, u_1} C
inst✝⁵ : Category.{?u.61740, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).inv.app X =
    (F.shiftIso m a' a'' ha'').inv.app X ≫
      (F.shiftIso n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫
        (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X)

Tactic:
simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem obj_surjective_of_im_eq_top (hφ : Function.Injective φ.obj) (hφ' : im φ hφ = ⊤) :
    Function.Surjective φ.obj

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
⊢ Function.Surjective φ.obj

Tactic:
rintro d

Result:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
d : D
⊢ ∃ a, φ.obj a = d

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
d : D
⊢ d ∈ ⊤.objs

Tactic:
apply mem_top_objs

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
d : D
⊢ ∃ a, φ.obj a = d

Tactic:
rw [← mem_im_objs_iff, hφ']

Result:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
hφ : Function.Injective φ.obj
hφ' : im φ hφ = ⊤
d : D
⊢ d ∈ ⊤.objs
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
lemma IsDominant.of_comp [H : IsDominant (f ≫ g)] : IsDominant g

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
⊢ IsDominant g

Tactic:
rw [isDominant_iff, denseRange_iff_closure_range, ← Set.univ_subset_iff] at H ⊢

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Set.univ ⊆ closure (Set.range ⇑(ConcreteCategory.hom (f ≫ g).base))
⊢ Set.univ ⊆ closure (Set.range ⇑(ConcreteCategory.hom g.base))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Set.univ ⊆ closure (Set.range ⇑(ConcreteCategory.hom (f ≫ g).base))
⊢ Set.univ ⊆ closure (Set.range ⇑(ConcreteCategory.hom g.base))

Tactic:
exact H.trans (closure_mono (Set.range_comp_subset_range f.base g.base))

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem ext_of_Ico_finite {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α)
    [IsFiniteMeasure μ] (hμν : μ univ = ν univ) (h : ∀ ⦃a b⦄, a < b → μ (Ico a b) = ν (Ico a b)) :
    μ = ν

Proof state:
case intro.intro.intro
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
a b : α
hlt : a < b
⊢ μ (Ico a b) = ν (Ico a b)

Tactic:
exact h hlt

Result:
no goals

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
⊢ μ = ν

Tactic:
refine
  ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α))
    (isPiSystem_Ico (id : α → α) id) ?_ hμν

Result:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
⊢ ∀ s ∈ {S | ∃ l u, l < u ∧ Ico l u = S}, μ s = ν s

Tactic:
rintro - ⟨a, b, hlt, rfl⟩

Result:
case intro.intro.intro
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ico a b) = ν (Ico a b)
a b : α
hlt : a < b
⊢ μ (Ico a b) = ν (Ico a b)
-- Mathlib/Analysis/Complex/Angle.lean
/-- The angle between two non-zero complex numbers is the absolute value of the argument of their
quotient.

Note that this does not hold when `x` or `y` is `0` as the LHS is `π / 2` while the RHS is `0`. -/
lemma angle_eq_abs_arg (hx : x ≠ 0) (hy : y ≠ 0) : angle x y = |(x / y).arg|

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖

Tactic:
have := norm_ne_zero_iff.mpr hy

Result:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
this : ‖y‖ ≠ 0
⊢ inner x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
this : ‖y‖ ≠ 0
⊢ (x.re * y.re + x.im * y.im) * (‖y‖⁻¹ * ‖x‖⁻¹) =
    (x.re * (y.re * (‖y‖ ^ 2)⁻¹) + x.im * (y.im * (‖y‖ ^ 2)⁻¹)) * (‖y‖ * ‖x‖⁻¹)

Tactic:
field_simp

Result:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
this : ‖y‖ ≠ 0
⊢ (x.re * y.re + x.im * y.im) * (‖y‖ ^ 2 * ‖x‖) = (x.re * y.re + x.im * y.im) * ‖y‖ * (‖y‖ * ‖x‖)

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
this : ‖y‖ ≠ 0
⊢ (x.re * y.re + x.im * y.im) * (‖y‖ ^ 2 * ‖x‖) = (x.re * y.re + x.im * y.im) * ‖y‖ * (‖y‖ * ‖x‖)

Tactic:
ring

Result:
no goals

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
this : ‖y‖ ≠ 0
⊢ inner x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖

Tactic:
simp [div_eq_mul_inv, Complex.normSq_eq_norm_sq]

Result:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
this : ‖y‖ ≠ 0
⊢ (x.re * y.re + x.im * y.im) * (‖y‖⁻¹ * ‖x‖⁻¹) =
    (x.re * (y.re * (‖y‖ ^ 2)⁻¹) + x.im * (y.im * (‖y‖ ^ 2)⁻¹)) * (‖y‖ * ‖x‖⁻¹)

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle x y = |(x / y).arg|

Tactic:
refine Real.arccos_eq_of_eq_cos (abs_nonneg _) (abs_arg_le_pi _) ?_

Result:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner x y / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner x y / (‖x‖ * ‖y‖) = Real.cos |(x / y).arg|

Tactic:
rw [Real.cos_abs, Complex.cos_arg (div_ne_zero hx hy)]

Result:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ inner x y / (‖x‖ * ‖y‖) = (x / y).re / ‖x / y‖
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem card_memberSubfamily_add_card_nonMemberSubfamily (a : α) (𝒜 : Finset (Finset α)) :
    #(𝒜.memberSubfamily a) + #(𝒜.nonMemberSubfamily a) = #𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) = #𝒜

Tactic:
rw [memberSubfamily, nonMemberSubfamily, card_image_of_injOn]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(filter (fun s => a ∈ s) 𝒜) + #(filter (fun s => a ∉ s) 𝒜) = #𝒜

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s => s.erase a) ↑(filter (fun s => a ∈ s) 𝒜)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ↑(filter (fun s => a ∈ s) 𝒜) ⊆ {s | a ∈ s}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(filter (fun s => a ∈ s) 𝒜) + #(filter (fun s => a ∉ s) 𝒜) = #𝒜

Tactic:
conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun s => (a ∈ s))]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s => s.erase a) ↑(filter (fun s => a ∈ s) 𝒜)

Tactic:
apply (erase_injOn' _).mono

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ↑(filter (fun s => a ∈ s) 𝒜) ⊆ {s | a ∈ s}
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_eq_one_iff [h : Nonempty M] :
    commProb M = 1 ↔ Std.Commutative ((· * ·) : M → M → M)

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card ↑{x | Commute x.1 x.2}) / ↑(card M) ^ 2 = 1 ↔ Std.Commutative fun x1 x2 => x1 * x2

Tactic:
rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
  set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]

Result:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.1 x.2}) ↔ Std.Commutative fun x1 x2 => x1 * x2

M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0

Tactic:
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
⊢ commProb M = 1 ↔ Std.Commutative fun x1 x2 => x1 * x2

Tactic:
haveI := Fintype.ofFinite M

Result:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ commProb M = 1 ↔ Std.Commutative fun x1 x2 => x1 * x2

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.1 x.2}) ↔ Std.Commutative fun x1 x2 => x1 * x2

Tactic:
exact ⟨fun h ↦ ⟨fun x y ↦ h (x, y)⟩, fun h x ↦ h.comm x.1 x.2⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ commProb M = 1 ↔ Std.Commutative fun x1 x2 => x1 * x2

Tactic:
rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]

Result:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card ↑{x | Commute x.1 x.2}) / ↑(card M) ^ 2 = 1 ↔ Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib/CategoryTheory/Extensive.lean
theorem FinitaryExtensive.isVanKampen_finiteCoproducts [FinitaryExtensive C] {ι : Type*}
    [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsVanKampenColimit c

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsVanKampenColimit c

Proof state:
case intro.intro.hc
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc

Result:
no goals

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
apply FinitaryExtensive.isVanKampen_finiteCoproducts_Fin

Result:
case intro.intro.hc
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsVanKampenColimit c

Tactic:
apply (IsVanKampenColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsVanKampenColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
-- Mathlib/Analysis/MeanInequalities.lean
theorem rpow_sum_le_const_mul_sum_rpow (hp : 1 ≤ p) :
    (∑ i ∈ s, |f i|) ^ p ≤ (#s : ℝ) ^ (p - 1) * ∑ i ∈ s, |f i| ^ p

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i) ^ p) ≤ ↑(↑(#s) ^ (p - 1) * ∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p)
⊢ (∑ i ∈ s, |f i|) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, |f i| ^ p

Tactic:
push_cast at this

Result:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ x ∈ s, |f x|) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ x ∈ s, |f x| ^ p
⊢ (∑ i ∈ s, |f i|) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, |f i| ^ p

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ x ∈ s, |f x|) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ x ∈ s, |f x| ^ p
⊢ (∑ i ∈ s, |f i|) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, |f i| ^ p

Tactic:
exact this

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, |f i|) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, |f i| ^ p

Tactic:
have :=
  NNReal.coe_le_coe.2
    (NNReal.rpow_sum_le_const_mul_sum_rpow s (fun i => ⟨_, abs_nonneg (f i)⟩) hp)

Result:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i) ^ p) ≤ ↑(↑(#s) ^ (p - 1) * ∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p)
⊢ (∑ i ∈ s, |f i|) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, |f i| ^ p
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
private lemma factor_δ_σ {n : ℕ} (i : Fin (n + 1)) (i' : Fin (n + 2)) :
    ∃ (z : SimplexCategoryGenRel) (e : mk n ⟶ z) (m : z ⟶ mk n)
      (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Proof state:
i : Fin (0 + 1)
i' : Fin (0 + 2)
⊢ δ i' ≫ σ i = 𝟙 (mk 0) ≫ 𝟙 (mk 0)

Tactic:
simp [switch_δ_σ₀]

Result:
no goals

Proof state:
case succ
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'

Result:
case succ.inl
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
h : δ i' ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

case succ.inr.intro.intro
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
j : Fin (n + 1)
j' : Fin (n + 2)
h : δ i' ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Proof state:
case succ.inr.intro.intro
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
j : Fin (n + 1)
j' : Fin (n + 2)
h : δ i' ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.σ _, P_δ.δ _, h⟩

Result:
no goals

Proof state:
case zero
i : Fin (0 + 1)
i' : Fin (0 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [switch_δ_σ₀]⟩

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
h : δ i' ≫ σ i = 𝟙 (mk (n + 1))
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ≫ 𝟙 (mk (n + 1))

Tactic:
simp [h]

Result:
no goals

Proof state:
case succ.inl
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
h : δ i' ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [h]⟩

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
lemma toPartialHomeomorph_right_inv {x : Y} (hx : x ∈ Set.range f) :
    f ((h.toPartialHomeomorph f).symm x) = x

Proof state:
case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ x ∈ (toPartialHomeomorph f h).target

Tactic:
rwa [toPartialHomeomorph_target]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toPartialHomeomorph f h).symm x) = x

Tactic:
rw [← congr_fun (h.toPartialHomeomorph_apply f), PartialHomeomorph.right_inv]

Result:
case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ x ∈ (toPartialHomeomorph f h).target