harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_max [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β}
    (h₁ : f.IsCoboundedUnder (· ≤ ·) u

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₂ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₃ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup u f ⊔ limsup v f ≤ limsup (fun a => u a ⊔ v a) f

Tactic:
exact max_le (c := limsup (fun a ↦ max (u a) (v a)) f)
  (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_left (u a) (v a))) h₁ bddmax)
  (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_right (u a) (v a))) h₂ bddmax)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₂ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₃ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
b : β
hb : b > limsup u f ⊔ limsup v f
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
x✝ : α
⊢ x✝ ∈ {x | (fun a => u a < b) x} ∩ {x | (fun a => v a < b) x} → x✝ ∈ {x | (fun a => u a ⊔ v a < b) x}

Tactic:
simp

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₂ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₃ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
b : β
hb : b > limsup u f ⊔ limsup v f
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
⊢ ∀ᶠ (a : α) in f, u a ⊔ v a < b

Tactic:
refine mem_of_superset (inter_mem hu hv) (fun _ ↦ by simp)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
/-- For any `w`-small family `X : ι → Type u` of `w`-small types, there exists
a regular cardinal `κ : Cardinal.{w}` such that `HasCardinalLT (X i) κ` for all `i : ι`. -/
lemma exists_regular_cardinal_forall {ι : Type v} {X : ι → Type u} [Small.{w} ι]
    [∀ i, Small.{w} (X i)] :
    ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ

Proof state:
ι : Type v
X : ι → Type u
inst✝¹ : Small.{w, v} ι
inst✝ : ∀ (i : ι), Small.{w, u} (X i)
⊢ ∃ κ, κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ

Tactic:
obtain ⟨κ, hκ, h⟩ := exists_regular_cardinal.{w} (Sigma X)

Result:
case intro.intro
ι : Type v
X : ι → Type u
inst✝¹ : Small.{w, v} ι
inst✝ : ∀ (i : ι), Small.{w, u} (X i)
κ : Cardinal.{w}
hκ : κ.IsRegular
h : HasCardinalLT (Sigma X) κ
⊢ ∃ κ, κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ

Proof state:
case intro.intro
ι : Type v
X : ι → Type u
inst✝¹ : Small.{w, v} ι
inst✝ : ∀ (i : ι), Small.{w, u} (X i)
κ : Cardinal.{w}
hκ : κ.IsRegular
h : HasCardinalLT (Sigma X) κ
⊢ ∃ κ, κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT (X i) κ

Tactic:
exact ⟨κ, hκ, fun i ↦ h.of_injective _ sigma_mk_injective⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
    filterMap f l₁ <:+ filterMap f l₂

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <:+ List.filterMap f xs ++ List.filterMap f l₁

Tactic:
apply suffix_append

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
h : l₁ <:+ l₂
⊢ List.filterMap f l₁ <:+ List.filterMap f l₂

Tactic:
obtain ⟨xs, rfl⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <:+ List.filterMap f (xs ++ l₁)

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <:+ List.filterMap f (xs ++ l₁)

Tactic:
rw [filterMap_append]

Result:
case intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ xs : List α
⊢ List.filterMap f l₁ <:+ List.filterMap f xs ++ List.filterMap f l₁
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_closure_iff {s : Set α} {a : α} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε :=
  (mem_closure_iff_nhds_basis nhds_basis_ball).trans <| by simp only [mem_ball, dist_comm]

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
a : α
⊢ (∀ (i : ℝ), 0 < i → ∃ y ∈ s, y ∈ ball a i) ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Tactic:
simp only [mem_ball, dist_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isClique_compl : Gᶜ.IsClique s ↔ G.IsIndepSet s

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ s.Pairwise fun v w => ¬G.Adj v w

Tactic:
rw [Set.Pairwise]

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w => ¬G.Adj v w

Tactic:
repeat rw [Set.Pairwise]

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ Gᶜ.IsClique s ↔ G.IsIndepSet s

Tactic:
rw [isIndepSet_iff, isClique_iff]

Result:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ s.Pairwise Gᶜ.Adj ↔ s.Pairwise fun v w => ¬G.Adj v w

Proof state:
α : Type u_1
G : SimpleGraph α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → Gᶜ.Adj x y) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → ¬G.Adj x y

Tactic:
simp_all [compl_adj]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean
@[reassoc]
lemma cone_π_app_comp_Pi_π_pos (m n : ℕ) (h : n < m) : (cone f).π.app ⟨m⟩ ≫
    Pi.π (fun i ↦ if _ : i < m then M i else N i) n =
    Pi.π _ n ≫ eqToHom (functorObj_eq_pos h).symm

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
m n : ℕ
h : n < m
⊢ (cone f).π.app (Opposite.op m) ≫ Pi.π (fun i => if x : i < m then M i else N i) n = Pi.π M n ≫ eqToHom ⋯

Tactic:
simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
  Discrete.functor_obj_eq_as, Discrete.natTrans_app]

Result:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
m n : ℕ
h : n < m
⊢ (limit.π (Discrete.functor fun m => M m) { as := n } ≫ if h : n < m then eqToHom ⋯ else f n ≫ eqToHom ⋯) =
    Pi.π M n ≫ eqToHom ⋯

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
m n : ℕ
h : n < m
⊢ (limit.π (Discrete.functor fun m => M m) { as := n } ≫ if h : n < m then eqToHom ⋯ else f n ≫ eqToHom ⋯) =
    Pi.π M n ≫ eqToHom ⋯

Tactic:
rw [dif_pos h]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem descFactorial_eq_factorial_mul_choose (n k : ℕ) : n.descFactorial k = k ! * n.choose k

Proof state:
case inl
n k : ℕ
h : n < k
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]

Result:
no goals

Proof state:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
rw [Nat.mul_comm]

Result:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = n.choose k * k !

Proof state:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = n.choose k * k !

Tactic:
apply Nat.mul_right_cancel (n - k).factorial_pos

Result:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!

Proof state:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k * (n - k)! = n.choose k * k ! * (n - k)!

Tactic:
rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]

Result:
no goals

Proof state:
n k : ℕ
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
obtain h | h := Nat.lt_or_ge n k

Result:
case inl
n k : ℕ
h : n < k
⊢ n.descFactorial k = k ! * n.choose k

case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = k ! * n.choose k
-- Mathlib/Topology/NhdsSet.lean
theorem mem_nhdsSet_empty : s ∈ 𝓝ˢ (∅ : Set X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ 𝓝ˢ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp (n * x) = exp x ^ n
  | 0 => by rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
  | Nat.succ n => by rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]

Proof state:
x : ℂ
n : ℕ
⊢ cexp (↑n.succ * x) = cexp x ^ n.succ

Tactic:
rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]

Result:
no goals

Proof state:
x : ℂ
⊢ cexp (↑0 * x) = cexp x ^ 0

Tactic:
rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_inverse_graph (x : f.domain) : (f x, (x : E)) ∈ (inverse f).graph

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
x : ↥f.domain
⊢ (↑f x, ↑x) ∈ f.inverse.graph

Tactic:
simp only [inverse_graph hf, Submodule.mem_map, mem_graph_iff, Subtype.exists, exists_and_left,
  exists_eq_left, LinearEquiv.prodComm_apply, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
x : ↥f.domain
⊢ ∃ a b, (∃ (h : a ∈ f.domain), ↑f ⟨a, ⋯⟩ = b) ∧ b = ↑f x ∧ a = ↑x

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
x : ↥f.domain
⊢ ∃ a b, (∃ (h : a ∈ f.domain), ↑f ⟨a, ⋯⟩ = b) ∧ b = ↑f x ∧ a = ↑x

Tactic:
exact ⟨(x : E), f x, ⟨x.2, Eq.refl _⟩, Eq.refl _, Eq.refl _⟩

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem quotient_mk_maps_eq (P : Ideal R[X]) :
    ((Quotient.mk (map (mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) P)).comp C).comp
        (Quotient.mk (P.comap (C : R →+* R[X]))) =
      (Ideal.quotientMap (map (mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) P)
            (mapRingHom (Quotient.mk (P.comap (C : R →+* R[X])))) le_comap_map).comp
        ((Quotient.mk P).comp C)

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
x : R
⊢ (Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)) (C ((Quotient.mk (comap C P)) x)) =
    (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)
      ((Quotient.mk P) (C x))

Tactic:
rw [quotientMap_mk, coe_mapRingHom, map_C]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ ((Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)).comp C).comp (Quotient.mk (comap C P)) =
    (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯).comp
      ((Quotient.mk P).comp C)

Tactic:
refine RingHom.ext fun x => ?_

Result:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
x : R
⊢ (((Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)).comp C).comp (Quotient.mk (comap C P))) x =
    ((quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯).comp
        ((Quotient.mk P).comp C))
      x

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
x : R
⊢ (((Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)).comp C).comp (Quotient.mk (comap C P))) x =
    ((quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯).comp
        ((Quotient.mk P).comp C))
      x

Tactic:
repeat' rw [RingHom.coe_comp, Function.comp_apply]

Result:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
x : R
⊢ (Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)) (C ((Quotient.mk (comap C P)) x)) =
    (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)
      ((Quotient.mk P) (C x))

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
x : R
⊢ (Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)) (C ((Quotient.mk (comap C P)) x)) =
    (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)
      (((Quotient.mk P).comp C) x)

Tactic:
rw [RingHom.coe_comp, Function.comp_apply]

Result:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
x : R
⊢ (Quotient.mk (map (mapRingHom (Quotient.mk (comap C P))) P)) (C ((Quotient.mk (comap C P)) x)) =
    (quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)
      ((Quotient.mk P) (C x))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b)

Proof state:
a b : Bool
⊢ a = b ↔ (a = true ↔ b = true)

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n

Proof state:
k m n : Nat
kpos : 0 < k
H : m * k ∣ n * k
⊢ m ∣ n

Tactic:
rw [Nat.mul_comm m k, Nat.mul_comm n k] at H

Result:
k m n : Nat
kpos : 0 < k
H : k * m ∣ k * n
⊢ m ∣ n

Proof state:
k m n : Nat
kpos : 0 < k
H : k * m ∣ k * n
⊢ m ∣ n

Tactic:
exact Nat.dvd_of_mul_dvd_mul_left kpos H

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_apply_finite' {s : Set α} (s_fin : s.Finite) (s_mble : MeasurableSet s) :
    count s = s_fin.toFinset.card

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_fin : s.Finite
s_mble : MeasurableSet s
⊢ count s = ↑s_fin.toFinset.card

Tactic:
simp [←
  @count_apply_finset' _ _ s_fin.toFinset (by simpa only [Finite.coe_toFinset] using s_mble)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_fin : s.Finite
s_mble : MeasurableSet s
⊢ MeasurableSet ↑s_fin.toFinset

Tactic:
simpa only [Finite.coe_toFinset] using s_mble

Result:
no goals
-- Mathlib/GroupTheory/Perm/Closure.lean
theorem closure_isCycle : closure { σ : Perm β | IsCycle σ } = ⊤

Proof state:
β : Type u_3
inst✝ : Finite β
⊢ closure {σ | σ.IsCycle} = ⊤

Tactic:
classical
  cases nonempty_fintype β
  exact
    top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))

Result:
no goals

Proof state:
case intro
β : Type u_3
inst✝ : Finite β
val✝ : Fintype β
⊢ closure {σ | σ.IsCycle} = ⊤

Tactic:
exact
  top_le_iff.mp (le_trans (ge_of_eq closure_isSwap) (closure_mono fun _ => IsSwap.isCycle))

Result:
no goals

Proof state:
β : Type u_3
inst✝ : Finite β
⊢ closure {σ | σ.IsCycle} = ⊤

Tactic:
cases nonempty_fintype β

Result:
case intro
β : Type u_3
inst✝ : Finite β
val✝ : Fintype β
⊢ closure {σ | σ.IsCycle} = ⊤
-- Mathlib/Data/List/Cycle.lean
theorem mem_map {β : Type*} {f : α → β} {b : β} {s : Cycle α} :
    b ∈ s.map f ↔ ∃ a, a ∈ s ∧ f a = b :=
  Quotient.inductionOn' s (by simp)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Cycle α
⊢ ∀ (a : List α), b ∈ map f (Quotient.mk'' a) ↔ ∃ a_1 ∈ Quotient.mk'' a, f a_1 = b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
lemma neg_div (a b : R) : -b / a = -(b / a)

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -b / a = -(b / a)

Tactic:
rw [neg_eq_neg_one_mul, mul_div_assoc, ← neg_eq_neg_one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_eq_false' {p : α → Bool} {xs : Vector α n} :
    xs.any p = false ↔ ∀ x, x ∈ xs → ¬p x

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.any p = false ↔ ∀ (x : α), x ∈ xs → ¬p x = true

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.any p = false ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → ¬p x = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.any p = false ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → ¬p x = true

Tactic:
simp only [any_mk, Array.any_eq_false']

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∀ (x : α), x ∈ xs → ¬p x = true) ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → ¬p x = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ (∀ (x : α), x ∈ xs → ¬p x = true) ↔ ∀ (x : α), x ∈ { toArray := xs, size_toArray := ⋯ } → ¬p x = true

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem algebraMap_injective [IsValExtension vK vA] [Nontrivial A] :
    Function.Injective (algebraMap vK.integer vA.integer)

Proof state:
A : Type u_2
inst✝⁶ : Ring A
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓK
inst✝² : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝¹ : IsValExtension vK vA
inst✝ : Nontrivial A
⊢ Function.Injective ⇑(algebraMap ↥vK.integer ↥vA.integer)

Tactic:
intro x y h

Result:
A : Type u_2
inst✝⁶ : Ring A
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓK
inst✝² : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝¹ : IsValExtension vK vA
inst✝ : Nontrivial A
x y : ↥vK.integer
h : (algebraMap ↥vK.integer ↥vA.integer) x = (algebraMap ↥vK.integer ↥vA.integer) y
⊢ x = y

Proof state:
A : Type u_2
inst✝⁶ : Ring A
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓK
inst✝² : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝¹ : IsValExtension vK vA
inst✝ : Nontrivial A
x y : ↥vK.integer
h : (algebraMap K A) ↑x = (algebraMap K A) ↑y
⊢ x = y

Tactic:
ext

Result:
case a
A : Type u_2
inst✝⁶ : Ring A
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓK
inst✝² : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝¹ : IsValExtension vK vA
inst✝ : Nontrivial A
x y : ↥vK.integer
h : (algebraMap K A) ↑x = (algebraMap K A) ↑y
⊢ ↑x = ↑y

Proof state:
case a
A : Type u_2
inst✝⁶ : Ring A
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓK
inst✝² : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝¹ : IsValExtension vK vA
inst✝ : Nontrivial A
x y : ↥vK.integer
h : (algebraMap K A) ↑x = (algebraMap K A) ↑y
⊢ ↑x = ↑y

Tactic:
apply RingHom.injective (algebraMap K A) h

Result:
no goals

Proof state:
A : Type u_2
inst✝⁶ : Ring A
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓK
inst✝² : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝¹ : IsValExtension vK vA
inst✝ : Nontrivial A
x y : ↥vK.integer
h : (algebraMap ↥vK.integer ↥vA.integer) x = (algebraMap ↥vK.integer ↥vA.integer) y
⊢ x = y

Tactic:
simp only [Subtype.ext_iff, val_algebraMap] at h

Result:
A : Type u_2
inst✝⁶ : Ring A
K : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝³ : LinearOrderedCommGroupWithZero ΓK
inst✝² : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝¹ : IsValExtension vK vA
inst✝ : Nontrivial A
x y : ↥vK.integer
h : (algebraMap K A) ↑x = (algebraMap K A) ↑y
⊢ x = y
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_pi_sub (θ : Angle) : ((π : Angle) - θ).sign = θ.sign

Proof state:
θ : Angle
⊢ (↑π - θ).sign = θ.sign

Tactic:
simp [sign_antiperiodic.sub_eq']

Result:
no goals
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem add_aux_left (x1 x2 y : ℕ × K) (H : R K p x1 x2) :
    mk K p (x1.1 + y.1, (frobenius K p)^[y.1] x1.2 + (frobenius K p)^[x1.1] y.2) =
      mk K p (x2.1 + y.1, (frobenius K p)^[y.1] x2.2 + (frobenius K p)^[x2.1] y.2) :=
  match x1, x2, H with
  | _, _, R.intro n x =>
    Quot.sound <| by
      rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add,
        Nat.succ_add]
      apply R.intro

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x + (⇑(frobenius K p))^[n] y.2))

Tactic:
apply R.intro

Result:
no goals

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + 1, (frobenius K p) x).1 + y.1,
      (⇑(frobenius K p))^[y.1] (n + 1, (frobenius K p) x).2 + (⇑(frobenius K p))^[(n + 1, (frobenius K p) x).1] y.2)

Tactic:
rw [← iterate_succ_apply, iterate_succ_apply', iterate_succ_apply', ← frobenius_add,
  Nat.succ_add]

Result:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x1 x2 y : ℕ × K
H : R K p x1 x2
n : ℕ
x : K
⊢ R K p ((n, x).1 + y.1, (⇑(frobenius K p))^[y.1] (n, x).2 + (⇑(frobenius K p))^[(n, x).1] y.2)
    ((n + y.1).succ, (frobenius K p) ((⇑(frobenius K p))^[y.1] x + (⇑(frobenius K p))^[n] y.2))
-- Mathlib/Data/Finset/Card.lean
theorem pred_card_le_card_erase : #s - 1 ≤ #(s.erase a)

Proof state:
case neg
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #s - 1 ≤ #(s.erase a)

Tactic:
rw [erase_eq_of_not_mem h]

Result:
case neg
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #s - 1 ≤ #s

Proof state:
case neg
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #s - 1 ≤ #s

Tactic:
exact Nat.sub_le _ _

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #s - 1 ≤ #(s.erase a)

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #s - 1 ≤ #(s.erase a)

case neg
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #s - 1 ≤ #(s.erase a)

Proof state:
case pos
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #s - 1 ≤ #(s.erase a)

Tactic:
exact (card_erase_of_mem h).ge

Result:
no goals