harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion (h₀ : (s ∪ t).PairwiseDisjoint f)
    (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i) : s ⊆ t

Proof state:
case intro.intro.intro
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t

Tactic:
rwa [h₀.eq (subset_union_left hi) (subset_union_right hj)
    (not_disjoint_iff.2 ⟨a, hai, haj⟩)]

Result:
no goals

Proof state:
case intro
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t

Tactic:
obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)

Result:
case intro.intro.intro
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t

Proof state:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
⊢ s ⊆ t

Tactic:
rintro i hi

Result:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
⊢ i ∈ t

Proof state:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
⊢ i ∈ t

Tactic:
obtain ⟨a, hai⟩ := h₁ i hi

Result:
case intro
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem func_mem (x : PSet) (i : x.Type) : x.Func i ∈ x

Proof state:
x : PSet.{u_1}
i : x.Type
⊢ x.Func i ∈ x

Tactic:
cases x

Result:
case mk
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
i : (mk α✝ A✝).Type
⊢ (mk α✝ A✝).Func i ∈ mk α✝ A✝

Proof state:
case mk
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
i : (mk α✝ A✝).Type
⊢ (mk α✝ A✝).Func i ∈ mk α✝ A✝

Tactic:
apply Mem.mk

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findFinIdx?_toArray (p : α → Bool) (l : List α) :
    l.toArray.findFinIdx? p = l.findFinIdx? p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l = drop 0 l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ Array.findFinIdx? p l.toArray = findFinIdx? p l

Tactic:
rw [Array.findFinIdx?, findFinIdx?, findFinIdx?_loop_toArray]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ l = drop 0 l
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma isStandardSmooth_respectsIso : RespectsIso @IsStandardSmooth.{t, w}

Proof state:
⊢ RespectsIso @IsStandardSmooth

Tactic:
apply isStandardSmooth_stableUnderComposition.respectsIso

Result:
⊢ ∀ {R S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsStandardSmooth

Proof state:
⊢ ∀ {R S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsStandardSmooth

Tactic:
introv

Result:
R S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.IsStandardSmooth

Proof state:
R S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
⊢ e.toRingHom.IsStandardSmooth

Tactic:
exact (IsStandardSmoothOfRelativeDimension.equiv e).isStandardSmooth

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem pmul_zeta (f : ArithmeticFunction R) : f.pmul ↑ζ = f

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ f.pmul ↑ζ = f

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ (f.pmul ↑ζ) x = f x

Proof state:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ (f.pmul ↑ζ) x = f x

Tactic:
cases x <;> simp [Nat.succ_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a b : α}
    (hab : a == b) : get! m a = get! m b

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a b : α
hab : (a == b) = true
⊢ get! m a = get! m b

Tactic:
simp_to_model using List.getValue!_congr

Result:
no goals
-- Mathlib/Data/Setoid/Partition/Card.lean
theorem Setoid.IsPartition.ncard_eq_finsum {α : Type*} {P : Set (Set α)}
    (hP : Setoid.IsPartition P) (s : Set α) (hs : s.Finite

Proof state:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
⊢ s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Tactic:
have hst (t : Set α) : (s ∩ t).Finite := hs.inter_of_left t

Result:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
⊢ s.ncard = ∑ᶠ (t : ↑P), (s ∩ ↑t).ncard

Proof state:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
⊢ (Function.support fun t => (s ∩ ↑t).ncard).Finite

Tactic:
let f : Function.support (fun (t : P) ↦ (s ∩ (t : Set α)).ncard) → s := fun ⟨t, ht⟩ ↦
  ⟨(Set.nonempty_of_ncard_ne_zero ht).choose, (Set.nonempty_of_ncard_ne_zero ht).choose_spec.1⟩

Result:
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : autoParam s.Finite _auto✝
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
f : ↑(Function.support fun t => (s ∩ ↑t).ncard) → ↑s :=
  fun x =>
    match x with
    | ⟨t, ht⟩ => ⟨Exists.choose ⋯, ⋯⟩
⊢ (Function.support fun t => (s ∩ ↑t).ncard).Finite
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem det_of_card_zero (h : Fintype.card n = 0) (M : Matrix n n R) : M.det = 1

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : Fintype.card n = 0
M : Matrix n n R
⊢ M.det = 1

Tactic:
rw [Fintype.card_eq_zero_iff] at h

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : IsEmpty n
M : Matrix n n R
⊢ M.det = 1

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : IsEmpty n
M : Matrix n n R
⊢ M = 1

Tactic:
ext i

Result:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : IsEmpty n
M : Matrix n n R
i j✝ : n
⊢ M i j✝ = 1 i j✝

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : IsEmpty n
M : Matrix n n R
⊢ M.det = 1

Tactic:
suffices M = 1 by simp [this]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : IsEmpty n
M : Matrix n n R
⊢ M = 1

Proof state:
case a
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : IsEmpty n
M : Matrix n n R
i j✝ : n
⊢ M i j✝ = 1 i j✝

Tactic:
exact h.elim i

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
h : IsEmpty n
M : Matrix n n R
this : M = 1
⊢ M.det = 1

Tactic:
simp [this]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] :
    finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ (maximalIdeal R).IsPrincipal

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, span R {(Submodule.subtype (maximalIdeal R)) x} = maximalIdeal R) ↔ ∃ a, span R {a} = maximalIdeal R

Tactic:
exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, ⊤ = span (ResidueField R) {(maximalIdeal R).toCotangent x}) ↔ ∃ a, maximalIdeal R = span R {a}

Tactic:
simp_rw [← Set.image_singleton, eq_comm (a := ⊤), CotangentSpace.span_image_eq_top_iff,
  ← (map_injective_of_injective (injective_subtype _)).eq_iff, map_span, Set.image_singleton,
  Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, span R {(Submodule.subtype (maximalIdeal R)) x} = maximalIdeal R) ↔ ∃ a, span R {a} = maximalIdeal R

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ IsPrincipal (maximalIdeal R)

Tactic:
rw [Module.finrank_le_one_iff_top_isPrincipal, isPrincipal_iff,
  (maximalIdeal R).toCotangent_surjective.exists, isPrincipal_iff]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, ⊤ = span (ResidueField R) {(maximalIdeal R).toCotangent x}) ↔ ∃ a, maximalIdeal R = span R {a}
-- Mathlib/Analysis/Complex/Isometry.lean
theorem linear_isometry_complex (f : ℂ ≃ₗᵢ[ℝ] ℂ) :
    ∃ a : Circle, f = rotation a ∨ f = conjLIE.trans (rotation a)

Proof state:
f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ ∃ a, f = rotation a ∨ f = conjLIE.trans (rotation a)

Tactic:
let a : Circle := ⟨f 1, by simp [Submonoid.unitSphere, f.norm_map]⟩

Result:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
⊢ ∃ a, f = rotation a ∨ f = conjLIE.trans (rotation a)

Proof state:
case h.refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₁ : f.trans (rotation a).symm = LinearIsometryEquiv.refl ℝ ℂ
⊢ f = rotation a

Tactic:
simpa using eq_mul_of_inv_mul_eq h₁

Result:
no goals

Proof state:
case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
⊢ f = rotation a ∨ f = conjLIE.trans (rotation a)

Tactic:
refine (linear_isometry_complex_aux this).imp (fun h₁ => ?_) fun h₂ => ?_

Result:
case h.refine_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₁ : f.trans (rotation a).symm = LinearIsometryEquiv.refl ℝ ℂ
⊢ f = rotation a

case h.refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₂ : f.trans (rotation a).symm = conjLIE
⊢ f = conjLIE.trans (rotation a)

Proof state:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
⊢ ∃ a, f = rotation a ∨ f = conjLIE.trans (rotation a)

Tactic:
use a

Result:
case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
⊢ f = rotation a ∨ f = conjLIE.trans (rotation a)

Proof state:
f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ f 1 ∈ Submonoid.unitSphere ℂ

Tactic:
simp [Submonoid.unitSphere, f.norm_map]

Result:
no goals

Proof state:
case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
⊢ f = rotation a ∨ f = conjLIE.trans (rotation a)

Tactic:
have : (f.trans (rotation a).symm) 1 = 1 := by simpa [a] using rotation_apply a⁻¹ (f 1)

Result:
case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
⊢ f = rotation a ∨ f = conjLIE.trans (rotation a)

Proof state:
case h.refine_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
this : (f.trans (rotation a).symm) 1 = 1
h₂ : f.trans (rotation a).symm = conjLIE
⊢ f = conjLIE.trans (rotation a)

Tactic:
exact eq_mul_of_inv_mul_eq h₂

Result:
no goals

Proof state:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle := ⟨f 1, ⋯⟩
⊢ (f.trans (rotation a).symm) 1 = 1

Tactic:
simpa [a] using rotation_apply a⁻¹ (f 1)

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_unique [Unique m] [DecidableEq m] [Zero α] (d : m → α) :
    diagonal d = of fun _ _ => d default

Proof state:
m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
⊢ diagonal d = of fun x x => d default

Tactic:
ext i j

Result:
case a
m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
i j : m
⊢ diagonal d i j = of (fun x x => d default) i j

Proof state:
case a
m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
i j : m
⊢ diagonal d i j = of (fun x x => d default) i j

Tactic:
rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ne_empty_of_mem {a : α} {l : Array α} (h : a ∈ l) : l ≠ #[]

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ { toList := toList✝ } ≠ #[]

Tactic:
simp [List.ne_nil_of_mem (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ ?m.38664 ∈ ?m.38665

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ l
⊢ l ≠ #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ { toList := toList✝ } ≠ #[]
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem blockTriangular_inv_of_blockTriangular [LinearOrder α] [Invertible M]
    (hM : BlockTriangular M b) : BlockTriangular M⁻¹ b

Proof state:
case H.inl
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k
hbi : b i = k
⊢ M⁻¹ i j = 0

Tactic:
have : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, hbi.ge⟩ ⟨j, hbi ▸ hij⟩ = 0 := by
  simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]

Result:
case H.inl
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [inst_2 : Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i => b i < k) fun j => b j < k
hbi : b i = k
this : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, ⋯⟩ ⟨j, ⋯⟩ = 0
⊢ M⁻¹ i j = 0
-- Mathlib/Order/Heyting/Hom.lean
theorem cancel_left (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => CoheytingHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingAlgebra γ
f₁ f₂ : CoheytingHom α β
g : CoheytingHom β γ
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/Find.lean
theorem findIdx?_map (f : β → α) (l : List β) : findIdx? p (l.map f) = l.findIdx? (p ∘ f)

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ findIdx? p (map f l) = findIdx? (p ∘ f) l

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp only [map_cons, findIdx?_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case nil
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
⊢ findIdx? p (map f []) = findIdx? (p ∘ f) []

Tactic:
simp

Result:
no goals

Proof state:
case cons
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
x : β
xs : List β
ih : findIdx? p (map f xs) = findIdx? (p ∘ f) xs
⊢ findIdx? p (map f (x :: xs)) = findIdx? (p ∘ f) (x :: xs)

Tactic:
simp only [map_cons, findIdx?_cons]

Result:
case cons
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
x : β
xs : List β
ih : findIdx? p (map f xs) = findIdx? (p ∘ f) xs
⊢ (if p (f x) = true then some 0 else Option.map (fun i => i + 1) (findIdx? p (map f xs))) =
    if (p ∘ f) x = true then some 0 else Option.map (fun i => i + 1) (findIdx? (p ∘ f) xs)

Proof state:
case cons
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
x : β
xs : List β
ih : findIdx? p (map f xs) = findIdx? (p ∘ f) xs
⊢ (if p (f x) = true then some 0 else Option.map (fun i => i + 1) (findIdx? p (map f xs))) =
    if (p ∘ f) x = true then some 0 else Option.map (fun i => i + 1) (findIdx? (p ∘ f) xs)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem LinearEquiv.dualMap_refl :
    (LinearEquiv.refl R M₁).dualMap = LinearEquiv.refl R (Dual R M₁)

Proof state:
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
⊢ (refl R M₁).dualMap = refl R (Dual R M₁)

Tactic:
ext

Result:
case h.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ ((refl R M₁).dualMap x✝¹) x✝ = ((refl R (Dual R M₁)) x✝¹) x✝

Proof state:
case h.h
R : Type u
inst✝² : CommSemiring R
M₁ : Type v
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ ((refl R M₁).dualMap x✝¹) x✝ = ((refl R (Dual R M₁)) x✝¹) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem hasBasis_nhds_zero : (𝓝 (0 : Γ₀)).HasBasis (fun γ : Γ₀ => γ ≠ 0) Iio

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ DirectedOn (Iio ⁻¹'o fun x1 x2 => x1 ≥ x2) fun γ => γ = 0 → False

Tactic:
exact directedOn_iff_directed.2 (Monotone.directed_ge fun a b hab => Iio_subset_Iio hab)

Result:
no goals

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ (𝓝 0).HasBasis (fun γ => γ ≠ 0) Iio

Tactic:
rw [nhds_zero]

Result:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)).HasBasis (fun γ => γ ≠ 0) Iio

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)).HasBasis (fun γ => γ ≠ 0) Iio

Tactic:
refine hasBasis_biInf_principal ?_ ⟨1, one_ne_zero⟩

Result:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ DirectedOn (Iio ⁻¹'o fun x1 x2 => x1 ≥ x2) fun γ => γ = 0 → False
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_horiz_isIso [IsIso fst] [IsIso g] (sq : CommSq fst snd f g) : IsPullback fst snd f g :=
  of_isLimit' sq
    (by
      refine
        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
          (fun s => ?_) (by aesop_cat)
      simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (fun s => s.fst ≫ inv fst) s ≫ snd = s.snd

Tactic:
simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ IsLimit sq.cone

Tactic:
refine
  PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
    (fun s => ?_) (by aesop_cat)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (fun s => s.fst ≫ inv fst) s ≫ snd = s.snd

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g) (m : s.pt ⟶ P), m ≫ fst = s.fst → m ≫ snd = s.snd → m = (fun s => s.fst ≫ inv fst) s

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : IsIso fst
inst✝ : IsIso g
sq : CommSq fst snd f g
⊢ ∀ (s : PullbackCone f g), (fun s => s.fst ≫ inv fst) s ≫ fst = s.fst

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma continuousOn_cosKernel (a : UnitAddCircle) : ContinuousOn (cosKernel a) (Ioi 0)

Proof state:
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun u => (↑a', I * ↑u)) x

Tactic:
fun_prop

Result:
no goals

Proof state:
case H
a' : ℝ
⊢ ContinuousOn (cosKernel ↑a') (Ioi 0)

Tactic:
apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))

Result:
case H
a' : ℝ
⊢ ContinuousOn (fun x => ↑(cosKernel (↑a') x)) (Ioi 0)

Proof state:
a : UnitAddCircle
⊢ ContinuousOn (cosKernel a) (Ioi 0)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a' =>
apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))
simp only [cosKernel_def]
refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)
exact (continuousAt_jacobiTheta₂ a' <| by simpa).comp
  (f := fun u : ℝ ↦ ((a' : ℂ), I * u)) (by fun_prop)

Result:
no goals

Proof state:
a' x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < (I * ↑x).im

Tactic:
simpa

Result:
no goals

Proof state:
case H
a' : ℝ
⊢ ContinuousOn (fun x => jacobiTheta₂ (↑a') (I * ↑x)) (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)

Result:
case H
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂ (↑a') (I * ↑x)) x

Proof state:
case H
a' x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x => jacobiTheta₂ (↑a') (I * ↑x)) x

Tactic:
exact (continuousAt_jacobiTheta₂ a' <| by simpa).comp
  (f := fun u : ℝ ↦ ((a' : ℂ), I * u)) (by fun_prop)

Result:
no goals

Proof state:
case H
a' : ℝ
⊢ ContinuousOn (fun x => ↑(cosKernel (↑a') x)) (Ioi 0)

Tactic:
simp only [cosKernel_def]

Result:
case H
a' : ℝ
⊢ ContinuousOn (fun x => jacobiTheta₂ (↑a') (I * ↑x)) (Ioi 0)