harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_ofList_of_mem [LawfulBEq α]
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h} :
    get (ofList l) k' h = v

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
h : k' ∈ ofList l
⊢ get (ofList l) k' h = v

Tactic:
simp_to_raw using Raw₀.Const.get_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem polarCoord_apply (a : ℂ) :
    Complex.polarCoord a = (‖a‖, Complex.arg a)

Proof state:
a : ℂ
⊢ ↑Complex.polarCoord a = (√(a.re ^ 2 + a.im ^ 2), a.arg)

Tactic:
rfl

Result:
no goals

Proof state:
a : ℂ
⊢ ↑Complex.polarCoord a = (‖a‖, a.arg)

Tactic:
simp_rw [Complex.norm_def, Complex.normSq_apply, ← pow_two]

Result:
a : ℂ
⊢ ↑Complex.polarCoord a = (√(a.re ^ 2 + a.im ^ 2), a.arg)
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
lemma deriv_eqOn {f' : 𝕜 → F} (hs : IsOpen s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
    s.EqOn (deriv f) f' := fun x hx ↦ by
  rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin <| hs.uniqueDiffWithinAt hx]

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
f' : 𝕜 → F
hs : IsOpen s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
x : 𝕜
hx : x ∈ s
⊢ deriv f x = f' x

Tactic:
rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin <| hs.uniqueDiffWithinAt hx]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem encode : Primrec (@encode α _) :=
  (@Primcodable.prim α _).of_eq fun n => by cases @decode α _ n <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ encode (decode n) = encode (Option.map encode (decode n))

Tactic:
cases @decode α _ n <;> rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/CompareReals.lean
theorem Rat.uniformSpace_eq :
    (AbsoluteValue.abs : AbsoluteValue ℚ ℚ).uniformSpace = PseudoMetricSpace.toUniformSpace

Proof state:
⊢ AbsoluteValue.abs.uniformSpace = PseudoMetricSpace.toUniformSpace

Tactic:
ext s

Result:
case h.h
s : Set (ℚ × ℚ)
⊢ s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ

Proof state:
case h.h
s : Set (ℚ × ℚ)
⊢ s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ

Tactic:
rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]

Result:
case h.h
s : Set (ℚ × ℚ)
⊢ (∃ i, 0 < i ∧ {p | AbsoluteValue.abs (p.2 - p.1) < i} ⊆ s) ↔ ∃ i, 0 < i ∧ {p | dist p.1 p.2 < ↑i} ⊆ s

Proof state:
case h.h
s : Set (ℚ × ℚ)
⊢ (∃ i, 0 < i ∧ {p | AbsoluteValue.abs (p.2 - p.1) < i} ⊆ s) ↔ ∃ i, 0 < i ∧ {p | dist p.1 p.2 < ↑i} ⊆ s

Tactic:
simp only [Rat.dist_eq, AbsoluteValue.abs_apply, ← Rat.cast_sub, ← Rat.cast_abs, Rat.cast_lt,
  abs_sub_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.and_false (b : Bool) : (b && false) = false

Proof state:
b : Bool
⊢ (b && false) = false

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffAt_zero : ContDiffAt 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffWithinAt 𝕜 0 f univ x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u

Tactic:
simp [contDiffWithinAt_zero, nhdsWithin_univ]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffAt 𝕜 0 f x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u

Tactic:
rw [← contDiffWithinAt_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ContDiffWithinAt 𝕜 0 f univ x ↔ ∃ u ∈ 𝓝 x, ContinuousOn f u
-- Mathlib/Data/Finset/Basic.lean
theorem erase_sdiff_comm (s t : Finset α) (a : α) : s.erase a \ t = (s \ t).erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a \ t = (s \ t).erase a

Tactic:
simp_rw [erase_eq, sdiff_right_comm]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem sorted_last_eq_max'_aux (s : Finset α)
    (h : (s.sort (· ≤ ·)).length - 1 < (s.sort (· ≤ ·)).length) (H : s.Nonempty) :
    (s.sort (· ≤ ·))[(s.sort (· ≤ ·)).length - 1] = s.max' H

Proof state:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.max' H ∈ l
⊢ s.max' H ≤ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1]

Tactic:
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this

Result:
case a.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
⊢ s.max' H ≤ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1]

Proof state:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : l.get ⟨(sort (fun x1 x2 => x1 ≤ x2) s).length - 1, h⟩ ∈ s
⊢ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1] ≤ s.max' H

Tactic:
exact s.le_max' _ this

Result:
no goals

Proof state:
case a.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
⊢ s.max' H ≤ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1]

Tactic:
rw [← hi]

Result:
case a.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.max' H ∈ l
i : Fin l.length
hi : l.get i = s.max' H
⊢ l.get i ≤ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
⊢ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1] = s.max' H

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
⊢ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1] ≤ s.max' H

case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
⊢ s.max' H ≤ (sort (fun x1 x2 => x1 ≤ x2) s)[(sort (fun x1 x2 => x1 ≤ x2) s).length - 1]
-- Mathlib/Data/Set/Lattice.lean
theorem image2_sInter_subset_left (S : Set (Set α)) (t : Set β) :
    image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
rw [sInter_eq_biInter]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
S : Set (Set α)
t : Set β
⊢ image2 f (⋂ i ∈ S, i) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
exact image2_iInter₂_subset_left ..

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
@[simp] lemma smoothNumbers_one : smoothNumbers 1 = {1}

Proof state:
⊢ smoothNumbers 1 = {1}

Tactic:
simp +decide only [not_false_eq_true, smoothNumbers_succ, smoothNumbers_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_map_iff {f g : α → β} {l : Array α} :
    map f l = map g l ↔ ∀ a ∈ l, f a = g a

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
l : Array α
⊢ map f l = map g l ↔ ∀ (a : α), a ∈ l → f a = g a

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem reducible_not_mem_factorSet {p : Associates α} (hp : ¬Irreducible p) (s : FactorSet α) :
    ¬p ∈ s := fun h ↦ by
  rwa [← factorSetMem_eq_mem, FactorSetMem, dif_neg hp] at h

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : Associates α
hp : ¬Irreducible p
s : FactorSet α
h : p ∈ s
⊢ False

Tactic:
rwa [← factorSetMem_eq_mem, FactorSetMem, dif_neg hp] at h

Result:
no goals
-- Mathlib/Algebra/Vertex/VertexOperator.lean
theorem ncoeff_add (A B : VertexOperator R V) (n : ℤ) : (A + B) [[n]] = A [[n]] + B [[n]]

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A B : VertexOperator R V
n : ℤ
⊢ (A + B)[[n]] = A[[n]] + B[[n]]

Tactic:
rw [ncoeff, ncoeff, ncoeff, coeff_add, Pi.add_apply]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.isBase_of_spanning (hI : M.Indep I) (hIs : M.Spanning I) : M.IsBase I

Proof state:
case intro.intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.IsBase B
hBI : B ⊆ I
⊢ M.IsBase I

Tactic:
rwa [← hB.eq_of_subset_indep hI hBI]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
⊢ M.IsBase I

Tactic:
obtain ⟨B, hB, hBI⟩ := hIs.exists_isBase_subset

Result:
case intro.intro
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
hIs : M.Spanning I
B : Set α
hB : M.IsBase B
hBI : B ⊆ I
⊢ M.IsBase I
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sub_cos : cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2) :=
  ofReal_injective <| by simp [cos_sub_cos]

Proof state:
x y : ℝ
⊢ ↑(cos x - cos y) = ↑(-2 * sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
simp [cos_sub_cos]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem mulLeftMap_eq_mulMap_comp {ι : Type*} [DecidableEq ι] (m : ι → M) :
    mulLeftMap N m = mulMap M N ∘ₗ LinearMap.rTensor N (Finsupp.linearCombination R m) ∘ₗ
      (TensorProduct.finsuppScalarLeft R N ι).symm.toLinearMap

Proof state:
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
m : ι → ↥M
⊢ mulLeftMap N m =
    M.mulMap N ∘ₗ
      LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm

Tactic:
ext

Result:
case h.h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
m : ι → ↥M
a✝ : ι
x✝ : ↥N
⊢ (mulLeftMap N m ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝

Proof state:
case h.h
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
M N : Submodule R S
ι : Type u_1
inst✝ : DecidableEq ι
m : ι → ↥M
a✝ : ι
x✝ : ↥N
⊢ (mulLeftMap N m ∘ₗ Finsupp.lsingle a✝) x✝ =
    ((M.mulMap N ∘ₗ
          LinearMap.rTensor (↥N) (Finsupp.linearCombination R m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm) ∘ₗ
        Finsupp.lsingle a✝)
      x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Functor.lean
theorem map_traverse {G : Type* → Type _} [Applicative G] [CommApplicative G] {α β γ : Type _}
    (g : α → G β) (h : β → γ) (x : Multiset α) :
    Functor.map (Functor.map h) (traverse g x) = traverse (Functor.map h ∘ g) x

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ (fun a => h <$> ↑a) <$> Traversable.traverse g a✝ =
    ofList <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝

Tactic:
simp only [fmap_def, Function.comp_apply, Functor.map_map, List.map_eq_map, map_coe]

Result:
no goals

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x

Tactic:
refine Quotient.inductionOn x ?_

Result:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ ∀ (a : List α), Functor.map h <$> traverse g ⟦a⟧ = traverse (Functor.map h ∘ g) ⟦a⟧

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ ∀ (a : List α), Functor.map h <$> traverse g ⟦a⟧ = traverse (Functor.map h ∘ g) ⟦a⟧

Tactic:
intro

Result:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ Functor.map h <$> traverse g ⟦a✝⟧ = traverse (Functor.map h ∘ g) ⟦a✝⟧

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ Functor.map h <$> traverse g ⟦a✝⟧ = traverse (Functor.map h ∘ g) ⟦a✝⟧

Tactic:
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, map_comp_coe]

Result:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ (fun a => h <$> ↑a) <$> Traversable.traverse g a✝ = ofList <$> Traversable.traverse (Functor.map h ∘ g) a✝

Proof state:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ (fun a => h <$> ↑a) <$> Traversable.traverse g a✝ = ofList <$> Traversable.traverse (Functor.map h ∘ g) a✝

Tactic:
rw [Traversable.map_traverse']

Result:
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
a✝ : List α
⊢ (fun a => h <$> ↑a) <$> Traversable.traverse g a✝ =
    ofList <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝
-- Mathlib/Data/TypeVec.lean
theorem lastFun_prod {α α' β β' : TypeVec (n + 1)} (f : α ⟹ β) (f' : α' ⟹ β') :
    lastFun (f ⊗' f') = Prod.map (lastFun f) (lastFun f')

Proof state:
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
⊢ lastFun (f ⊗' f') = Prod.map (lastFun f) (lastFun f')

Tactic:
ext i : 1

Result:
case h
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : (α ⊗ α').last
⊢ lastFun (f ⊗' f') i = Prod.map (lastFun f) (lastFun f') i

Proof state:
case h.mk
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : α.last
snd✝ : α'.last
⊢ lastFun (f ⊗' f') (fst✝, snd✝) = Prod.map (lastFun f) (lastFun f') (fst✝, snd✝)

Tactic:
simp [lastFun, *]

Result:
case h.mk
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : α.last
snd✝ : α'.last
⊢ (f ⊗' f') Fin2.fz (fst✝, snd✝) = (f Fin2.fz fst✝, f' Fin2.fz snd✝)

Proof state:
case h
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
i : (α ⊗ α').last
⊢ lastFun (f ⊗' f') i = Prod.map (lastFun f) (lastFun f') i

Tactic:
induction i

Result:
case h.mk
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : α.last
snd✝ : α'.last
⊢ lastFun (f ⊗' f') (fst✝, snd✝) = Prod.map (lastFun f) (lastFun f') (fst✝, snd✝)

Proof state:
case h.mk
n : ℕ
α α' β β' : TypeVec.{u_1} (n + 1)
f : α ⟹ β
f' : α' ⟹ β'
fst✝ : α.last
snd✝ : α'.last
⊢ (f ⊗' f') Fin2.fz (fst✝, snd✝) = (f Fin2.fz fst✝, f' Fin2.fz snd✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_push_eq_append (l l' : Array α) : l.foldl push l' = l' ++ l

Proof state:
case mk
α : Type u_1
l' : Array α
toList✝ : List α
⊢ foldl push l' { toList := toList✝ } = l' ++ { toList := toList✝ }

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ foldl push { toList := toList✝ } { toList := toList✝¹ } = { toList := toList✝ } ++ { toList := toList✝¹ }

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ foldl push { toList := toList✝ } { toList := toList✝¹ } = { toList := toList✝ } ++ { toList := toList✝¹ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l l' : Array α
⊢ foldl push l' l = l' ++ l

Tactic:
cases l

Result:
case mk
α : Type u_1
l' : Array α
toList✝ : List α
⊢ foldl push l' { toList := toList✝ } = l' ++ { toList := toList✝ }
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubsemiring R} :
    (↑(⨅ i, S i) : Set R) = ⋂ i, S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_1
S : ι → NonUnitalSubsemiring R
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_of_mem_singleton (h : a ∈ #v[b]) : a = b

Proof state:
α✝ : Type u_1
b a : α✝
h : a ∈ { toArray := #[b], size_toArray := ⋯ }
⊢ a = b

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem image_empty : r.image ∅ = ∅

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
x : β
⊢ x ∈ r.image ∅ ↔ x ∈ ∅

Tactic:
simp [mem_image]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r.image ∅ = ∅

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
x : β
⊢ x ∈ r.image ∅ ↔ x ∈ ∅
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem abs_moebius {n : ℕ} :
    |μ n| = if Squarefree n then 1 else 0

Proof state:
case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0

Tactic:
simp only [moebius_eq_zero_of_not_squarefree h, abs_zero]

Result:
no goals

Proof state:
n : ℕ
⊢ |μ n| = if Squarefree n then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
h : Squarefree n
⊢ |μ n| = 1

case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0

Proof state:
case pos
n : ℕ
h : Squarefree n
⊢ |μ n| = 1

Tactic:
exact abs_moebius_eq_one_of_squarefree h

Result:
no goals
-- Mathlib/Algebra/Field/Power.lean
theorem Odd.neg_one_zpow (h : Odd n) : (-1 : α) ^ n = -1

Proof state:
α : Type u_1
inst✝ : DivisionRing α
n : ℤ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
rw [h.neg_zpow, one_zpow]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
lemma disjoint_of_disjoint_support {H K : Subgroup (Perm α)}
    (h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support) :
    _root_.Disjoint H K

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ H ⊓ K ≤ ⊥

Tactic:
intro x ⟨hx1, hx2⟩

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
x : Perm α
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
x : Perm α
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
⊢ x ∈ ⊥

Tactic:
specialize h x hx1 x hx2

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
h : _root_.Disjoint x.support x.support
⊢ x ∈ ⊥

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ _root_.Disjoint H K

Tactic:
rw [disjoint_iff_inf_le]

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ H ⊓ K ≤ ⊥

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
x : Perm α
hx1 : x ∈ ↑H.toSubmonoid
hx2 : x ∈ ↑K.toSubmonoid
h : _root_.Disjoint x.support x.support
⊢ x ∈ ⊥

Tactic:
rwa [disjoint_self, Finset.bot_eq_empty, support_eq_empty_iff] at h

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
lemma forall_some_ne_iff_eq_none {o : Option α} : (∀ (x : α), some x ≠ o) ↔ o = none

Proof state:
α : Type u_1
o : Option α
⊢ (∀ (x : α), some x ≠ o) ↔ o = none

Tactic:
apply not_iff_not.1

Result:
α : Type u_1
o : Option α
⊢ (¬∀ (x : α), some x ≠ o) ↔ ¬o = none

Proof state:
α : Type u_1
o : Option α
⊢ (¬∀ (x : α), some x ≠ o) ↔ ¬o = none

Tactic:
simpa only [not_forall, not_not] using Option.ne_none_iff_exists.symm

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem cos_eq_one_iff {x : ℂ} : cos x = 1 ↔ ∃ k : ℤ, k * (2 * π) = x

Proof state:
x : ℂ
⊢ (∃ k, x = 2 * ↑k * ↑π + 0 ∨ x = 2 * ↑k * ↑π - 0) ↔ ∃ k, ↑k * (2 * ↑π) = x

Tactic:
simp [mul_assoc, mul_left_comm, eq_comm]

Result:
no goals

Proof state:
x : ℂ
⊢ cos x = 1 ↔ ∃ k, ↑k * (2 * ↑π) = x

Tactic:
rw [← cos_zero, eq_comm, cos_eq_cos_iff]

Result:
x : ℂ
⊢ (∃ k, x = 2 * ↑k * ↑π + 0 ∨ x = 2 * ↑k * ↑π - 0) ↔ ∃ k, ↑k * (2 * ↑π) = x
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesCoimage.factorThruCoimage_iso_hom :
    (PreservesCoimage.iso F f).hom ≫ Abelian.factorThruCoimage (F.map f) =
      F.map (Abelian.factorThruCoimage f)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ (iso F f).hom ≫ Abelian.factorThruCoimage (F.map f) = F.map (Abelian.factorThruCoimage f)

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals