harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_map_iff_of_preservesHomology [F.ReflectsIsomorphisms] :
    QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i

Proof state:
ι : Type u_1
c : ComplexShape ι
C₁ : Type u_2
C₂ : Type u_3
inst✝¹⁰ : Category.{u_4, u_2} C₁
inst✝⁹ : Category.{u_5, u_3} C₂
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
K L : HomologicalComplex C₁ c
φ : K ⟶ L
F : C₁ ⥤ C₂
inst✝⁶ : F.Additive
inst✝⁵ : F.PreservesHomology
i : ι
inst✝⁴ : K.HasHomology i
inst✝³ : L.HasHomology i
inst✝² : ((F.mapHomologicalComplex c).obj K).HasHomology i
inst✝¹ : ((F.mapHomologicalComplex c).obj L).HasHomology i
inst✝ : F.ReflectsIsomorphisms
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C₂ c i).map ((F.mapHomologicalComplex c).map φ)) ↔
    ShortComplex.QuasiIso ((shortComplexFunctor C₁ c i).map φ)

Tactic:
exact ShortComplex.quasiIso_map_iff_of_preservesLeftHomology F
  ((shortComplexFunctor C₁ c i).map φ)

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
C₁ : Type u_2
C₂ : Type u_3
inst✝¹⁰ : Category.{u_4, u_2} C₁
inst✝⁹ : Category.{u_5, u_3} C₂
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
K L : HomologicalComplex C₁ c
φ : K ⟶ L
F : C₁ ⥤ C₂
inst✝⁶ : F.Additive
inst✝⁵ : F.PreservesHomology
i : ι
inst✝⁴ : K.HasHomology i
inst✝³ : L.HasHomology i
inst✝² : ((F.mapHomologicalComplex c).obj K).HasHomology i
inst✝¹ : ((F.mapHomologicalComplex c).obj L).HasHomology i
inst✝ : F.ReflectsIsomorphisms
⊢ QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i

Tactic:
simp only [quasiIsoAt_iff]

Result:
ι : Type u_1
c : ComplexShape ι
C₁ : Type u_2
C₂ : Type u_3
inst✝¹⁰ : Category.{u_4, u_2} C₁
inst✝⁹ : Category.{u_5, u_3} C₂
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
K L : HomologicalComplex C₁ c
φ : K ⟶ L
F : C₁ ⥤ C₂
inst✝⁶ : F.Additive
inst✝⁵ : F.PreservesHomology
i : ι
inst✝⁴ : K.HasHomology i
inst✝³ : L.HasHomology i
inst✝² : ((F.mapHomologicalComplex c).obj K).HasHomology i
inst✝¹ : ((F.mapHomologicalComplex c).obj L).HasHomology i
inst✝ : F.ReflectsIsomorphisms
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C₂ c i).map ((F.mapHomologicalComplex c).map φ)) ↔
    ShortComplex.QuasiIso ((shortComplexFunctor C₁ c i).map φ)
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_mul (n : ℕ) (φ ψ : R⟦X⟧) :
    coeff R n (φ * ψ) = ∑ p ∈ antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ p ∈ antidiagonal (single () n), (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ =
    ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ

Tactic:
rw [Finsupp.antidiagonal_single, Finset.sum_map]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ x ∈ antidiagonal n,
      (MvPowerSeries.coeff R (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).1) φ *
        (MvPowerSeries.coeff R (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).2) ψ =
    ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ x ∈ antidiagonal n,
      (MvPowerSeries.coeff R (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).1) φ *
        (MvPowerSeries.coeff R (({ toFun := single (), inj' := ⋯ }.prodMap { toFun := single (), inj' := ⋯ }) x).2) ψ =
    ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ (coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ

Tactic:
refine (MvPowerSeries.coeff_mul _ φ ψ).trans ?_

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
⊢ ∑ p ∈ antidiagonal (single () n), (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ =
    ∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ
-- Mathlib/Data/Set/Equitable.lean
theorem equitableOn_iff_exists_image_subset_icc {s : Set α} {f : α → ℕ} :
    s.EquitableOn f ↔ ∃ b, f '' s ⊆ Icc b (b + 1)

Proof state:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ b, f '' s ⊆ Icc b (b + 1)

Tactic:
simpa only [image_subset_iff] using equitableOn_iff_exists_le_le_add_one

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.braid_natural {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
    biprod.map f g ≫ (biprod.braiding _ _).hom = (biprod.braiding _ _).hom ≫ biprod.map g f

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : X ⟶ Y
g : Z ⟶ W
⊢ map f g ≫ (braiding Y W).hom = (braiding X Z).hom ≫ map g f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma coborder_eq_compl_frontier_iff :
    coborder s = (frontier s)ᶜ ↔ IsOpen s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = (frontier s)ᶜ ↔ IsOpen s

Tactic:
simp_rw [coborder_eq_union_frontier_compl, union_eq_right, subset_compl_iff_disjoint_left,
  disjoint_frontier_iff_isOpen]

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem cancel_left {g : SupBotHom β γ} {f₁ f₂ : SupBotHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => SupBotHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝⁵ : Max α
inst✝⁴ : Bot α
inst✝³ : Max β
inst✝² : Bot β
inst✝¹ : Max γ
inst✝ : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_singleton_iff {f : α → β} {l : List α} {b : β} :
    map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
b : β
⊢ map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b

Tactic:
simp [map_eq_cons_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFreeOn_singleton : G.CliqueFreeOn {a} n ↔ 1 < n

Proof state:
α : Type u_1
G : SimpleGraph α
a : α
n : ℕ
⊢ G.CliqueFreeOn {a} n ↔ 1 < n

Tactic:
obtain _ | _ | n := n <;>
  simp [CliqueFreeOn, isNClique_iff, ← subset_singleton_iff', (Nat.succ_ne_zero _).symm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negDblY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q)
    (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
    (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) : W.negDblY P / W.dblZ P ^ 3 =
    W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.negDblY P / W.dblZ P ^ 3 =
    (toAffine W).negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
rw [negDblY, dblX, toAffine_slope_of_eq hP hQ hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
  toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem closedAbsConvexHull_closure_eq_closedAbsConvexHull {s : Set E} :
    closedAbsConvexHull 𝕜 (closure s) = closedAbsConvexHull 𝕜 s :=
  subset_antisymm (by simpa using ((closedAbsConvexHull 𝕜).monotone
      (closure_subset_closedAbsConvexHull (𝕜 := 𝕜) (E := E))))
    ((closedAbsConvexHull 𝕜).monotone subset_closure)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : SMul 𝕜 E
inst✝² : SMul ℝ E
inst✝¹ : AddCommMonoid E
inst✝ : TopologicalSpace E
s : Set E
⊢ (closedAbsConvexHull 𝕜) (closure s) ⊆ (closedAbsConvexHull 𝕜) s

Tactic:
simpa using ((closedAbsConvexHull 𝕜).monotone
(closure_subset_closedAbsConvexHull (𝕜 := 𝕜) (E := E)))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem isNone_attachWith {p : α → Prop} (o : Option α) (H : ∀ a ∈ o, p a) :
    (o.attachWith p H).isNone = o.isNone

Proof state:
α : Type u_1
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
⊢ (o.attachWith p H).isNone = o.isNone

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.findIdx?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
    l₂.findIdx? p = none → l₁.findIdx? p = none

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ findIdx? p l₂ = none → findIdx? p l₁ = none

Tactic:
simp only [findIdx?_eq_none_iff]

Result:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∀ (x : α), x ∈ l₂ → p x = false) → ∀ (x : α), x ∈ l₁ → p x = false

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∀ (x : α), x ∈ l₂ → p x = false) → ∀ (x : α), x ∈ l₁ → p x = false

Tactic:
exact fun w x m => w x (h.mem m)

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem subtype_eq_empty {p : α → Prop} [DecidablePred p] {s : Finset α} :
    s.subtype p = ∅ ↔ ∀ x, p x → x ∉ s

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s

Tactic:
simp [Finset.ext_iff, Subtype.forall, Subtype.coe_mk]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_inv_eq_iff_eq_mul {a c : α} : a * ↑b⁻¹ = c ↔ a = c * b :=
  ⟨fun h => by rw [← h, inv_mul_cancel_right], fun h => by rw [h, mul_inv_cancel_right]⟩

Proof state:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a = c * ↑b
⊢ a * ↑b⁻¹ = c

Tactic:
rw [h, mul_inv_cancel_right]

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
b : αˣ
a c : α
h : a * ↑b⁻¹ = c
⊢ a = c * ↑b

Tactic:
rw [← h, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem countP_map (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] :
    countP p (map f s) = card (s.filter fun a => p (f a))

Proof state:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countP p (map f s) = (filter (fun a => p (f a)) s).card

Tactic:
refine Multiset.induction_on s ?_ fun a t IH => ?_

Result:
case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countP p (map f 0) = (filter (fun a => p (f a)) 0).card

case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a => p (f a)) t).card
⊢ countP p (map f (a ::ₘ t)) = (filter (fun a => p (f a)) (a ::ₘ t)).card

Proof state:
case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a => p (f a)) t).card
⊢ countP p (map f (a ::ₘ t)) = (filter (fun a => p (f a)) (a ::ₘ t)).card

Tactic:
rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
  Nat.add_comm]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countP p (map f 0) = (filter (fun a => p (f a)) 0).card

Tactic:
rw [map_zero, countP_zero, filter_zero, card_zero]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp)]
lemma edist_one_right (a : E) : edist a 1 = ‖a‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ edist a 1 = ‖a‖ₑ

Tactic:
simp [edist_nndist, nndist_one_right, enorm]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Finset.card_fin (n : ℕ) : #(univ : Finset (Fin n)) = n

Proof state:
n : ℕ
⊢ #univ = n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem dichotomy (b : Bool) : b = false ∨ b = true

Proof state:
b : Bool
⊢ b = false ∨ b = true

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem of_dist_le' {K : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) :
    LipschitzOnWith (Real.toNNReal K) f s :=
  of_dist_le_mul fun x hx y hy =>
    le_trans (h x hx y hy) <| by gcongr; apply Real.le_coe_toNNReal

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K ≤ ↑K.toNNReal

Tactic:
apply Real.le_coe_toNNReal

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K * dist x y ≤ ↑K.toNNReal * dist x y

Tactic:
gcongr

Result:
case h
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K ≤ ↑K.toNNReal
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_restrict (h : I ⊆ E) (R : Set α) :
    (uniqueBaseOn I E) ↾ R = uniqueBaseOn (I ∩ R) R

Proof state:
α : Type u_1
E I : Set α
h : I ⊆ E
R : Set α
⊢ uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R) R

Tactic:
rw [uniqueBaseOn_restrict', inter_right_comm, inter_eq_self_of_subset_left h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem PosSemidef.diagonal [StarOrderedRing R] [DecidableEq n] {d : n → R} (h : 0 ≤ d) :
    PosSemidef (diagonal d) :=
  ⟨isHermitian_diagonal_of_self_adjoint _ <| funext fun i => IsSelfAdjoint.of_nonneg (h i),
    fun x => by
      refine Fintype.sum_nonneg fun i => ?_
      simpa only [mulVec_diagonal, ← mul_assoc] using conjugate_nonneg (h i) _⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
h : 0 ≤ d
x : n → R
i : n
⊢ 0 i ≤ star x i * (diagonal d *ᵥ x) i

Tactic:
simpa only [mulVec_diagonal, ← mul_assoc] using conjugate_nonneg (h i) _

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
h : 0 ≤ d
x : n → R
⊢ 0 ≤ star x ⬝ᵥ diagonal d *ᵥ x

Tactic:
refine Fintype.sum_nonneg fun i => ?_

Result:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
h : 0 ≤ d
x : n → R
i : n
⊢ 0 i ≤ star x i * (diagonal d *ᵥ x) i
-- Mathlib/Combinatorics/Enumerative/Partition.lean
@[simp] lemma indiscrete_parts {n : ℕ} (hn : n ≠ 0) : (indiscrete n).parts = {n}

Proof state:
n : ℕ
hn : n ≠ 0
⊢ (indiscrete n).parts = {n}

Tactic:
simp [indiscrete, filter_eq_self, hn]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_left (a b : α) : toIcoMod hp a (p + b) = toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (p + b) = toIcoMod hp a b

Tactic:
rw [add_comm, toIcoMod_add_right]

Result:
no goals
-- Mathlib/Data/Ordering/Lemmas.lean
theorem ite_eq_gt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
    ((if c then a else b) = Ordering.gt) = if c then a = Ordering.gt else b = Ordering.gt

Proof state:
c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
by_cases c <;> simp [*]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem inter_cylinder_same (s : Finset ι) (S₁ : Set (∀ i : s, α i)) (S₂ : Set (∀ i : s, α i)) :
    cylinder s S₁ ∩ cylinder s S₂ = cylinder s (S₁ ∩ S₂)

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder (s ∪ s) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ ⋯ ⁻¹' S₂) = cylinder s (S₁ ∩ S₂)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder s S₁ ∩ cylinder s S₂ = cylinder s (S₁ ∩ S₂)

Tactic:
classical rw [inter_cylinder]; rfl

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder s S₁ ∩ cylinder s S₂ = cylinder s (S₁ ∩ S₂)

Tactic:
rw [inter_cylinder]

Result:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder (s ∪ s) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ ⋯ ⁻¹' S₂) = cylinder s (S₁ ∩ S₂)
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem lipschitzOnWith_of_nnnorm_hasDerivWithin_le {C : ℝ≥0} (hs : Convex ℝ s)
    (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C) :
    LipschitzOnWith C f s :=
  Convex.lipschitzOnWith_of_nnnorm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt)
    (fun x hx => le_trans (by simp) (bound x hx)) hs

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f f' : 𝕜 → G
s : Set 𝕜
C : ℝ≥0
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
x : 𝕜
hx : x ∈ s
⊢ ‖smulRight 1 (f' x)‖₊ ≤ ‖f' x‖₊

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma compProd_apply [SFinite μ] [IsSFiniteKernel κ] {s : Set (α × β)} (hs : MeasurableSet s) :
    (μ ⊗ₘ κ) s = ∫⁻ a, κ a (Prod.mk a ⁻¹' s) ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ κ) s = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

Tactic:
simp_rw [compProd, Kernel.compProd_apply hs, Kernel.const_apply, Kernel.prodMkLeft_apply']

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (b : α), (κ b) {c | (b, c) ∈ s} ∂μ = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (b : α), (κ b) {c | (b, c) ∈ s} ∂μ = ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' s) ∂μ

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem ucs_le_of_normalizer_eq_self (h : N₁.normalizer = N₁) (k : ℕ) :
    (⊥ : LieSubmodule R L M).ucs k ≤ N₁

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k ⊥ ≤ N₁

Tactic:
rw [← ucs_eq_self_of_normalizer_eq_self h k]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k ⊥ ≤ ucs k N₁

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ucs k ⊥ ≤ ucs k N₁

Tactic:
gcongr

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ⊥ ≤ N₁

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N₁ : LieSubmodule R L M
inst✝ : LieModule R L M
h : N₁.normalizer = N₁
k : ℕ
⊢ ⊥ ≤ N₁

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem comap_map (μ : Measure α) : (map f μ).comap f = μ

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
t : Set α
a✝ : MeasurableSet t
⊢ (Measure.comap f (Measure.map f μ)) t = μ t

Tactic:
rw [hf.comap_apply, hf.map_apply, preimage_image_eq _ hf.injective]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
⊢ Measure.comap f (Measure.map f μ) = μ

Tactic:
ext t _

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
t : Set α
a✝ : MeasurableSet t
⊢ (Measure.comap f (Measure.map f μ)) t = μ t
-- Mathlib/Probability/Independence/Basic.lean
theorem indepSets_singleton_iff {s t : Set Ω} :
    IndepSets {s} {t} μ ↔ μ (s ∩ t) = μ s * μ t

Proof state:
Ω : Type u_1
_mΩ : MeasurableSpace Ω
μ : Measure Ω
s t : Set Ω
⊢ IndepSets {s} {t} μ ↔ μ (s ∩ t) = μ s * μ t

Tactic:
simp only [IndepSets, Kernel.indepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure,
  Kernel.const_apply]

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem holor_index_cons_decomp (p : HolorIndex (d :: ds) → Prop) :
    ∀ t : HolorIndex (d :: ds),
      (∀ i is, ∀ h : t.1 = i :: is, p ⟨i :: is, by rw [← h]; exact t.2⟩) → p t
  | ⟨[], hforall₂⟩, _ => absurd (forall₂_nil_left_iff.1 hforall₂) (cons_ne_nil d ds)
  | ⟨i :: is, _⟩, hp => hp i is rfl

Proof state:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 => x1 < x2) (↑t) (d :: ds)

Tactic:
exact t.2

Result:
no goals

Proof state:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 => x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← h]

Result:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 => x1 < x2) (↑t) (d :: ds)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem back?_push (a : Array α) : (a.push x).back? = some x

Proof state:
α : Type u_1
x : α
a : Array α
⊢ (a.push x).back? = some x

Tactic:
simp [back?, ← getElem?_toList]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coverage.lean
lemma le_of_factorsThru_sieve {X : C} (S : Presieve X) (T : Sieve X) (h : S.FactorsThru T) :
    S ≤ T

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : S.FactorsThru T.arrows
⊢ S ≤ T.arrows

Tactic:
rintro Y f hf

Result:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : S.FactorsThru T.arrows
Y : C
f : Y ⟶ X
hf : f ∈ S
⊢ f ∈ T.arrows

Proof state:
case intro.intro.intro.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : S.FactorsThru T.arrows
Y W : C
i : Y ⟶ W
e : W ⟶ X
h1 : T.arrows e
hf : i ≫ e ∈ S
⊢ i ≫ e ∈ T.arrows

Tactic:
exact T.downward_closed h1 _

Result:
no goals

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : S.FactorsThru T.arrows
Y : C
f : Y ⟶ X
hf : f ∈ S
⊢ f ∈ T.arrows

Tactic:
obtain ⟨W, i, e, h1, rfl⟩ := h hf

Result:
case intro.intro.intro.intro
C : Type u_2
inst✝ : Category.{u_1, u_2} C
X : C
S : Presieve X
T : Sieve X
h : S.FactorsThru T.arrows
Y W : C
i : Y ⟶ W
e : W ⟶ X
h1 : T.arrows e
hf : i ≫ e ∈ S
⊢ i ≫ e ∈ T.arrows
-- Mathlib/SetTheory/Game/Nim.lean
theorem toLeftMovesNim_one_symm (i) :
    (@toLeftMovesNim 1).symm i = ⟨0, Set.mem_Iio.mpr zero_lt_one⟩

Proof state:
i : (nim 1).LeftMoves
⊢ toLeftMovesNim.symm i = ⟨0, ⋯⟩

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem iInf_adj {f : ι → SimpleGraph V} : (⨅ i, f i).Adj a b ↔ (∀ i, (f i).Adj a b) ∧ a ≠ b

Proof state:
ι : Sort u_1
V : Type u
a b : V
f : ι → SimpleGraph V
⊢ (⨅ i, f i).Adj a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ a ≠ b

Tactic:
simp [iInf]

Result:
no goals