harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem sum_card_inter_le (h : ∀ a ∈ s, #{b ∈ B | a ∈ b} ≤ n) : (∑ t ∈ B, #(s ∩ t)) ≤ #s * n

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #(filter (fun b => a ∈ b) B) ≤ n
⊢ (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0) ≤ ∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0

Tactic:
exact sum_comm.le

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #(filter (fun b => a ∈ b) B) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ ∑ x ∈ s, #(filter (fun b => x ∈ b) B)

Tactic:
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]

Result:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #(filter (fun b => a ∈ b) B) ≤ n
⊢ (∑ x ∈ B, ∑ a ∈ s, if a ∈ x then 1 else 0) ≤ ∑ x ∈ s, ∑ a ∈ B, if x ∈ a then 1 else 0

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #(filter (fun b => a ∈ b) B) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ #s * n

Tactic:
refine le_trans ?_ (s.sum_le_card_nsmul _ _ h)

Result:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ a ∈ s, #(filter (fun b => a ∈ b) B) ≤ n
⊢ ∑ t ∈ B, #(s ∩ t) ≤ ∑ x ∈ s, #(filter (fun b => x ∈ b) B)
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_diagonal' (i : m) : (v ⬝ᵥ fun j => diagonal w j i) = v i * w i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
⊢ (v ⬝ᵥ fun j => diagonal w j i) = v i * w i

Tactic:
have : ∀ j ≠ i, v j * diagonal w j i = 0 := fun j hij => by
  simp [diagonal_apply_ne _ hij]

Result:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ (v ⬝ᵥ fun j => diagonal w j i) = v i * w i

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i j : m
hij : j ≠ i
⊢ v j * diagonal w j i = 0

Tactic:
simp [diagonal_apply_ne _ hij]

Result:
no goals

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ (v ⬝ᵥ fun j => diagonal w j i) = v i * w i

Tactic:
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma mem_support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ ((finSuccEquiv R n f).coeff i).support ↔ x.cons i ∈ f.support

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin n →₀ ℕ
⊢ x ∈ (((finSuccEquiv R n) f).coeff i).support ↔ cons i x ∈ f.support

Tactic:
rw [← (Finsupp.cons_right_injective i).mem_finset_image (a := x),
  image_support_finSuccEquiv]

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin n →₀ ℕ
⊢ cons i x ∈ Finset.filter (fun m => m 0 = i) f.support ↔ cons i x ∈ f.support

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
x : Fin n →₀ ℕ
⊢ cons i x ∈ Finset.filter (fun m => m 0 = i) f.support ↔ cons i x ∈ f.support

Tactic:
simp only [Finset.mem_filter, mem_support_iff, ne_eq, cons_zero, and_true]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem fromEdgeSet_inter (s t : Set (Sym2 V)) :
    fromEdgeSet (s ∩ t) = fromEdgeSet s ⊓ fromEdgeSet t

Proof state:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet (s ∩ t)).Adj v w ↔ (fromEdgeSet s ⊓ fromEdgeSet t).Adj v w

Tactic:
simp only [fromEdgeSet_adj, Set.mem_inter_iff, Ne, inf_adj]

Result:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w

Proof state:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (s(v, w) ∈ s ∧ s(v, w) ∈ t) ∧ ¬v = w ↔ (s(v, w) ∈ s ∧ ¬v = w) ∧ s(v, w) ∈ t ∧ ¬v = w

Tactic:
tauto

Result:
no goals

Proof state:
V : Type u
s t : Set (Sym2 V)
⊢ fromEdgeSet (s ∩ t) = fromEdgeSet s ⊓ fromEdgeSet t

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet (s ∩ t)).Adj v w ↔ (fromEdgeSet s ⊓ fromEdgeSet t).Adj v w
-- Mathlib/Data/ENat/Lattice.lean
lemma sSup_add (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a

Proof state:
s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ sSup s + a = ⨆ b ∈ s, b + a

Tactic:
rw [sSup_eq_iSup, biSup_add hs]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem abs_norm_sub_norm_le' (a b : E) : |‖a‖ - ‖b‖| ≤ ‖a / b‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ |‖a‖ - ‖b‖| ≤ ‖a / b‖

Tactic:
simpa [dist_eq_norm_div] using abs_dist_sub_le a b 1

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma isClosed_iff_isLowerSet_and_dirSupClosed [IsScott α univ] :
    IsClosed s ↔ IsLowerSet s ∧ DirSupClosed s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ IsClosed s ↔ IsLowerSet s ∧ DirSupClosed s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl,
  dirSupInaccOn_univ, dirSupInacc_compl]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem add_div' (a b c : K) (hc : c ≠ 0) : b + a / c = (b * c + a) / c

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ b + a / c = (b * c + a) / c

Tactic:
rw [add_div, mul_div_cancel_right₀ _ hc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
lemma isIso_diagonal_iff : IsIso (diagonal f) ↔ Mono f :=
  ⟨fun H ↦ ⟨fun _ _ e ↦ by rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f)
    (diagonal f)).mp (by simp), lift_snd]⟩, fun _ ↦ inferInstance⟩

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ = x✝

Tactic:
rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f)
(diagonal f)).mp (by simp), lift_snd]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ diagonal f ≫ fst f f = diagonal f ≫ snd f f

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem preservesEpimorphisms.of_iso {F G : C ⥤ D} [PreservesEpimorphisms F] (α : F ≅ G) :
    PreservesEpimorphisms G :=
  { preserves := fun {X} {Y} f h => by
      suffices G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom from this ▸ epi_comp _ _
      rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.PreservesEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom

Tactic:
rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.PreservesEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
⊢ Epi (G.map f)

Tactic:
suffices G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom from this ▸ epi_comp _ _

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.PreservesEpimorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Epi f
⊢ G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom
-- Mathlib/Topology/Separation/Regular.lean
theorem exists_open_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) :
    ∃ u : Set X,
      x ∈ u ∧ IsOpen u ∧ ∃ v : Set X, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T25Space X
x y : X
h : x ≠ y
⊢ ∃ u, x ∈ u ∧ IsOpen u ∧ ∃ v, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)

Tactic:
simpa only [exists_prop, and_assoc] using
  ((nhds_basis_opens x).lift'_closure.disjoint_iff (nhds_basis_opens y).lift'_closure).1
    (disjoint_lift'_closure_nhds.2 h)

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[simp]
lemma map_g' : (h.map F).g' = F.map h.g'

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (h.map F).g' = F.map h.g'

Tactic:
rw [← cancel_epi (h.map F).p, p_g', map_g, map_p, ← F.map_comp, p_g']

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_singleton : [b].destutter' R a = if R a b then [a, b] else [a]

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
⊢ destutter' R a [b] = if R a b then [a, b] else [a]

Tactic:
split_ifs with h <;> simp! [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_push_eq_some {xs : Array α} :
    (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b))

Proof state:
α : Type u_1
a : α
p : α → Bool
b : α
xs : Array α
⊢ find? p (xs.push a) = some b ↔ find? p xs = some b ∨ find? p xs = none ∧ p a = true ∧ a = b

Tactic:
cases xs

Result:
case mk
α : Type u_1
a : α
p : α → Bool
b : α
toList✝ : List α
⊢ find? p ({ toList := toList✝ }.push a) = some b ↔
    find? p { toList := toList✝ } = some b ∨ find? p { toList := toList✝ } = none ∧ p a = true ∧ a = b

Proof state:
case mk
α : Type u_1
a : α
p : α → Bool
b : α
toList✝ : List α
⊢ find? p ({ toList := toList✝ }.push a) = some b ↔
    find? p { toList := toList✝ } = some b ∨ find? p { toList := toList✝ } = none ∧ p a = true ∧ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_iSup_of_directed {ι} [Nonempty ι] (S : ι → Submodule R M) (H : Directed (· ≤ ·) S) {x} :
    x ∈ iSup S ↔ ∃ i, x ∈ S i

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_9
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ (∃ i, x ∈ ↑(S i)) ↔ ∃ i, x ∈ S i

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_9
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ iSup S ↔ ∃ i, x ∈ S i

Tactic:
rw [← SetLike.mem_coe, coe_iSup_of_directed S H, mem_iUnion]

Result:
R : Type u_1
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_9
inst✝ : Nonempty ι
S : ι → Submodule R M
H : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ (∃ i, x ∈ ↑(S i)) ↔ ∃ i, x ∈ S i
-- Mathlib/SetTheory/Game/PGame.lean
theorem fuzzy_congr {x₁ y₁ x₂ y₂ : PGame} (hx : x₁ ≈ x₂) (hy : y₁ ≈ y₂) : x₁ ‖ y₁ ↔ x₂ ‖ y₂ :=
  show _ ∧ _ ↔ _ ∧ _ by rw [lf_congr hx hy, lf_congr hy hx]

Proof state:
x₁ y₁ x₂ y₂ : PGame
hx : x₁ ≈ x₂
hy : y₁ ≈ y₂
⊢ x₁ ⧏ y₁ ∧ y₁ ⧏ x₁ ↔ x₂ ⧏ y₂ ∧ y₂ ⧏ x₂

Tactic:
rw [lf_congr hx hy, lf_congr hy hx]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Lemmas.lean
theorem cast_ofScientific {K} [DivisionRing K] (m : ℕ) (s : Bool) (e : ℕ) :
    (OfScientific.ofScientific m s e : ℚ) = (OfScientific.ofScientific m s e : K)

Proof state:
K : Type u_2
inst✝ : DivisionRing K
m : ℕ
s : Bool
e : ℕ
⊢ ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

Tactic:
rw [← NNRat.cast_ofScientific (K := K), ← NNRat.cast_ofScientific, cast_nnratCast]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem coeff_restriction' {p : R[X]} {n : ℕ} : (coeff (restriction p) n).1 = coeff p n

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(p.restriction.coeff n) = p.coeff n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inv_neg {x : tsze R M} : (-x)⁻¹ = -(x⁻¹)

Proof state:
R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹ = -x⁻¹

Tactic:
ext <;> simp [inv_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
theorem cross_orthogonal_left {v w : ℙ F (Fin 3 → F)} (h : v ≠ w) :
    (cross v w).orthogonal v

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
w : ℙ F (Fin 3 → F)
v : Fin 3 → F
hv : v ≠ 0
h : mk F v hv ≠ w
⊢ ((mk F v hv).cross w).orthogonal (mk F v hv)

Tactic:
induction w with | h w hw =>
rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v

Tactic:
induction v with | h v hv =>
induction w with | h w hw =>
rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Result:
no goals

Proof state:
case h.h
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v : Fin 3 → F
hv : v ≠ 0
w : Fin 3 → F
hw : w ≠ 0
h : mk F v hv ≠ mk F w hw
⊢ ((mk F v hv).cross (mk F w hw)).orthogonal (mk F v hv)

Tactic:
rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem mem_or_subset (hx : x.IsOrdinal) (hy : y.IsOrdinal) : x ∈ y ∨ y ⊆ x

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ y ⊆ x → y ⊆ x

Tactic:
exact id

Result:
no goals

Proof state:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ y ⊆ x

Tactic:
rw [or_iff_not_imp_left, not_mem_iff_subset hx hy]

Result:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ y ⊆ x → y ⊆ x
-- Mathlib/Data/Nat/Init.lean
lemma mul_div_lt_iff_not_dvd : d * (n / d) < n ↔ ¬ d ∣ n

Proof state:
d n : ℕ
⊢ d * (n / d) < n ↔ ¬d ∣ n

Tactic:
simp [Nat.lt_iff_le_and_ne, mul_div_eq_iff_dvd, mul_div_le]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem Connected.ofBoxProdLeft (h : (G □ H).Connected) : G.Connected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this✝ : Nonempty α
this : Nonempty β
⊢ G.Connected

Tactic:
exact ⟨h.preconnected.ofBoxProdLeft⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ G.Connected

Tactic:
haveI := (nonempty_prod.1 h.nonempty).2

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this✝ : Nonempty α
this : Nonempty β
⊢ G.Connected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
⊢ G.Connected

Tactic:
haveI := (nonempty_prod.1 h.nonempty).1

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ G.Connected
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_one : order (1 : R⟦X⟧) = 0

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ order 1 = 0

Tactic:
simpa using order_monomial_of_ne_zero 0 (1 : R) one_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem min_findIdx_findIdx {xs : List α} {p q : α → Bool} :
    min (xs.findIdx p) (xs.findIdx q) = xs.findIdx (fun a => p a || q a)

Proof state:
case nil
α : Type u_1
p q : α → Bool
⊢ min (findIdx p []) (findIdx q []) = findIdx (fun a => p a || q a) []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : min (findIdx p xs) (findIdx q xs) = findIdx (fun a => p a || q a) xs
⊢ min (findIdx p (x :: xs)) (findIdx q (x :: xs)) = findIdx (fun a => p a || q a) (x :: xs)

Tactic:
simp [findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]

Result:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : min (findIdx p xs) (findIdx q xs) = findIdx (fun a => p a || q a) xs
⊢ min (if p x = true then 0 else findIdx p xs + 1) (if q x = true then 0 else findIdx q xs + 1) =
    if p x = true ∨ q x = true then 0 else findIdx (fun a => p a || q a) xs + 1

Proof state:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : min (findIdx p xs) (findIdx q xs) = findIdx (fun a => p a || q a) xs
⊢ min (if p x = true then 0 else findIdx p xs + 1) (if q x = true then 0 else findIdx q xs + 1) =
    if p x = true ∨ q x = true then 0 else findIdx (fun a => p a || q a) xs + 1

Tactic:
split <;> split <;> simp_all [Nat.add_min_add_right]

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p q : α → Bool
⊢ min (findIdx p xs) (findIdx q xs) = findIdx (fun a => p a || q a) xs

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp [findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]
  split <;> split <;> simp_all [Nat.add_min_add_right]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem union_assoc {s₁ s₂ s₃ : Finmap β} : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
  induction_on₃ s₁ s₂ s₃ fun s₁ s₂ s₃ => by
    simp only [AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ s₃✝ : Finmap β
s₁ s₂ s₃ : AList β
⊢ ⟦s₁⟧ ∪ ⟦s₂⟧ ∪ ⟦s₃⟧ = ⟦s₁⟧ ∪ (⟦s₂⟧ ∪ ⟦s₃⟧)

Tactic:
simp only [AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toArray_attach {α : Type _} {l : Vector α n} :
    l.attach.toArray = l.toArray.attachWith (· ∈ l) (by simp)

Proof state:
n : Nat
α : Type u_1
l : Vector α n
⊢ l.attach.toArray = l.attachWith (fun x => x ∈ l) ⋯

Tactic:
simp [attach]

Result:
no goals

Proof state:
n : Nat
α : Type ?u.4424
l : Vector α n
⊢ ∀ (x : α), x ∈ l.toArray → (fun x => x ∈ l) x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_left_Icc' {a : α} (h : 0 < a) (b c : α) :
    (a * ·) '' Icc b c = Icc (a * b) (a * c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c : α
⊢ (fun x => a * x) '' Icc b c = Icc (a * b) (a * c)

Tactic:
convert image_mul_right_Icc' b c h using 1 <;> simp only [mul_comm _ a]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma aleph0_mul_ofENat {m : ℕ∞} (hm : m ≠ 0) : ℵ₀ * m = ℵ₀

Proof state:
m : ℕ∞
hm : m ≠ 0
⊢ ℵ₀ * ↑m = ℵ₀

Tactic:
rw [mul_comm, ofENat_mul_aleph0 hm]

Result:
no goals
-- Mathlib/GroupTheory/PresentedGroup.lean
theorem ext {φ ψ : PresentedGroup rels →* G} (hx : ∀ (x : α), φ (.of x) = ψ (.of x)) : φ = ψ

Proof state:
case h.h
α : Type u_1
G : Type u_2
inst✝ : Group G
rels : Set (FreeGroup α)
φ ψ : PresentedGroup rels →* G
hx : ∀ (x : α), φ (of x) = ψ (of x)
a✝ : α
⊢ (φ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels))) (FreeGroup.of a✝) =
    (ψ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels))) (FreeGroup.of a✝)

Tactic:
apply hx

Result:
no goals

Proof state:
α : Type u_1
G : Type u_2
inst✝ : Group G
rels : Set (FreeGroup α)
φ ψ : PresentedGroup rels →* G
hx : ∀ (x : α), φ (of x) = ψ (of x)
⊢ φ = ψ

Tactic:
ext

Result:
case h.h
α : Type u_1
G : Type u_2
inst✝ : Group G
rels : Set (FreeGroup α)
φ ψ : PresentedGroup rels →* G
hx : ∀ (x : α), φ (of x) = ψ (of x)
a✝ : α
⊢ (φ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels))) (FreeGroup.of a✝) =
    (ψ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels))) (FreeGroup.of a✝)
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsGT_inv {a : H} : Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a)

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a)

Tactic:
simpa only [inv_inv] using @tendsto_inv_nhdsGT _ _ _ _ a⁻¹

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_irrefl' (h : ∃ᶠ x in l, ‖f' x‖ ≠ 0) : ¬f' =o[l] f'

Proof state:
case intro.intro
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖
hne : ‖f' x‖ ≠ 0
⊢ False

Tactic:
rw [one_div, ← div_eq_inv_mul] at hle

Result:
case intro.intro
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ ‖f' x‖ / 2
hne : ‖f' x‖ ≠ 0
⊢ False

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
⊢ False

Tactic:
rcases ((ho.bound one_half_pos).and_frequently h).exists with ⟨x, hle, hne⟩

Result:
case intro.intro
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ 1 / 2 * ‖f' x‖
hne : ‖f' x‖ ≠ 0
⊢ False

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
⊢ ¬f' =o[l] f'

Tactic:
intro ho

Result:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
⊢ False

Proof state:
case intro.intro
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
x : α
hle : ‖f' x‖ ≤ ‖f' x‖ / 2
hne : ‖f' x‖ ≠ 0
⊢ False

Tactic:
exact (half_lt_self (lt_of_le_of_ne (norm_nonneg _) hne.symm)).not_le hle

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Iio_succ_eq_Iic_of_not_isMax (hb : ¬ IsMax b) : Iio (succ b) = Iic b :=
  coe_injective <| by simpa using Set.Iio_succ_eq_Iic_of_not_isMax hb

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
⊢ ↑(Iio (succ b)) = ↑(Iic b)

Tactic:
simpa using Set.Iio_succ_eq_Iic_of_not_isMax hb

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem inl_pushoutZeroZeroIso_hom (X Y : C) [HasBinaryCoproduct X Y] :
    pushout.inl _ _ ≫ (pushoutZeroZeroIso X Y).hom = coprod.inl

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inl

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫ (pushoutZeroZeroIso X Y).hom = coprod.inl

Tactic:
dsimp [pushoutZeroZeroIso]

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl 0 0 ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr ⋯,
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inl
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem eval {α : ι → Type u} [∀ i, PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) :
    LipschitzWith 1 (Function.eval i : (∀ i, α i) → α i) :=
  LipschitzWith.of_edist_le fun f g => by convert edist_le_pi_edist f g i

Proof state:
ι : Type x
α : ι → Type u
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : Fintype ι
i : ι
f g : (x : ι) → α x
⊢ edist (eval i f) (eval i g) ≤ edist f g

Tactic:
convert edist_le_pi_edist f g i

Result:
no goals
-- Mathlib/Logic/Relation.lean
lemma transGen_minimal {r' : α → α → Prop} (hr' : Transitive r') (h : ∀ x y, r x y → r' x y)
    {x y : α} (hxy : TransGen r x y) : r' x y

Proof state:
α : Type u_1
r r' : α → α → Prop
hr' : Transitive r'
h : ∀ (x y : α), r x y → r' x y
x y : α
hxy : TransGen r x y
⊢ r' x y

Tactic:
simpa [transGen_eq_self hr'] using TransGen.mono h hxy

Result:
no goals