harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Support.lean
theorem Disjoint.card_support_mul (h : Disjoint f g) :
    #(f * g).support = #f.support + #g.support

Proof state:
case e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support

Tactic:
ext

Result:
case e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a✝ : α
⊢ a✝ ∈ (f * g).support ↔ a✝ ∈ f.support ∪ g.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
simpa using h.disjoint_support

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #f.support + #g.support

Tactic:
rw [← Finset.card_union_of_disjoint]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #(f.support ∪ g.support)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Proof state:
case e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a✝ : α
⊢ a✝ ∈ (f * g).support ↔ a✝ ∈ f.support ∪ g.support

Tactic:
simp [h.support_mul]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #(f.support ∪ g.support)

Tactic:
congr

Result:
case e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β → AssocList α δ}
    {g : List ((a : α) × β a) → List ((a : α) × δ a)}
    (hfg : ∀ {l}, Perm ((f l).toList) (g l.toList))
    (hg : ∀ {l l'}, Perm (g (l ++ l')) (g l ++ g l')) :
    Perm (toListModel (updateAllBuckets m.1.buckets f)) (g (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
⊢ (List.foldl (fun x y => x ++ (f y).toList) [] m.val.buckets.toList).Perm
    (g (List.foldl (fun acc a => acc ++ a.toList) [] m.val.buckets.toList))

Tactic:
suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    Perm (g l'') l' →
    Perm (l.foldl (fun acc a => acc ++ (f a).toList) l')
      (g (l.foldl (fun acc a => acc ++ a.toList) l'')) by
  simpa using this m.1.buckets.toList [] [] (by simp [hg₀])

Result:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : AssocList α β → AssocList α δ
g : List ((a : α) × β a) → List ((a : α) × δ a)
hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList)
hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')
hg₀ : g [] = []
⊢ ∀ (l : List (AssocList α β)) (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
    (g l'').Perm l' →
      (List.foldl (fun acc a => acc ++ (f a).toList) l' l).Perm (g (List.foldl (fun acc a => acc ++ a.toList) l'' l))
-- Mathlib/Order/RelClasses.lean
lemma ssubset_of_eq_of_ssubset (hab : a = b) (hbc : b ⊂ c) : a ⊂ c

Proof state:
α : Type u
inst✝ : HasSSubset α
a b c : α
hab : a = b
hbc : b ⊂ c
⊢ a ⊂ c

Tactic:
rwa [hab]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem uniqueMDiffWithinAt_iff {s : Set M} {x : M} :
    UniqueMDiffWithinAt I s x ↔
      UniqueDiffWithinAt 𝕜 ((extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target)
        ((extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
⊢ UniqueMDiffWithinAt I s x ↔
    UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target) (↑(extChartAt I x) x)

Tactic:
apply uniqueDiffWithinAt_congr

Result:
case st
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
⊢ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x =
    𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target] ↑(extChartAt I x) x

Proof state:
case st
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
⊢ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x =
    𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target] ↑(extChartAt I x) x

Tactic:
rw [nhdsWithin_inter, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
lemma tensor_map_id_left_injective_of_injective (hf : Function.Injective f) :
    Function.Injective (AlgebraTensorModule.map LinearMap.id f :
        AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N)

Proof state:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(AlgebraTensorModule.map LinearMap.id f)

Tactic:
rw [tensor_map_id_left_eq_map I f]

Result:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective
    ⇑(↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M))

Proof state:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(map I f)

Tactic:
exact map_injective I hf

Result:
no goals

Proof state:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective
    ⇑(↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M))

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
  EquivLike.injective_comp]

Result:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑(map I f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_filter {l : List α} {p q : α → Bool} :
    (filter p l).any q = l.any fun a => p a && q a

Proof state:
case nil
α : Type u_1
p q : α → Bool
⊢ (filter p []).any q = [].any fun a => p a && q a

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
h : α
t : List α
ih : (filter p t).any q = t.any fun a => p a && q a
⊢ (if p h = true then h :: filter p t else filter p t).any q = (h :: t).any fun a => p a && q a

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
p q : α → Bool
⊢ (filter p l).any q = l.any fun a => p a && q a

Tactic:
induction l with
| nil => rfl
| cons h t ih =>
  simp only [filter_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
h : α
t : List α
ih : (filter p t).any q = t.any fun a => p a && q a
⊢ (filter p (h :: t)).any q = (h :: t).any fun a => p a && q a

Tactic:
simp only [filter_cons]

Result:
case cons
α : Type u_1
p q : α → Bool
h : α
t : List α
ih : (filter p t).any q = t.any fun a => p a && q a
⊢ (if p h = true then h :: filter p t else filter p t).any q = (h :: t).any fun a => p a && q a
-- Mathlib/Topology/LocallyConstant/Basic.lean
@[simp]
lemma piecewise_apply_right {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂)
    (h : C₁ ∪ C₂ = Set.univ) (f : LocallyConstant C₁ Z) (g : LocallyConstant C₂ Z)
    (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, hx.1⟩ = g ⟨x, hx.2⟩)
    [DecidablePred (· ∈ C₁)] (x : X) (hx : x ∈ C₂) :
    piecewise h₁ h₂ h f g hfg x = g ⟨x, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₂
⊢ (if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = g ⟨x, hx⟩

Tactic:
split_ifs with h

Result:
case pos
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∈ C₁
⊢ f ⟨x, h⟩ = g ⟨x, hx⟩

case neg
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∉ C₁
⊢ g ⟨x, ⋯⟩ = g ⟨x, hx⟩

Proof state:
case pos
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∈ C₁
⊢ f ⟨x, h⟩ = g ⟨x, hx⟩

Tactic:
exact hfg x ⟨h, hx⟩

Result:
no goals

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₂
⊢ (piecewise h₁ h₂ h f g hfg) x = g ⟨x, hx⟩

Tactic:
simp only [piecewise, Set.mem_preimage, continuous_subtype_val.restrictPreimage,
  coe_comap, Function.comp_apply, coe_mk]

Result:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₂
⊢ (if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = g ⟨x, hx⟩

Proof state:
case neg
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h✝ : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₂
h : x ∉ C₁
⊢ g ⟨x, ⋯⟩ = g ⟨x, hx⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem goldConj_sq : ψ ^ 2 = ψ + 1

Proof state:
⊢ ((1 - √5) / 2) ^ 2 - ((1 - √5) / 2 + 1) = 0

Tactic:
ring_nf

Result:
⊢ -5 / 4 + √5 ^ 2 * (1 / 4) = 0

Proof state:
⊢ ψ ^ 2 = ψ + 1

Tactic:
rw [goldenConj, ← sub_eq_zero]

Result:
⊢ ((1 - √5) / 2) ^ 2 - ((1 - √5) / 2 + 1) = 0

Proof state:
⊢ -5 / 4 + √5 ^ 2 * (1 / 4) = 0

Tactic:
rw [Real.sq_sqrt] <;> norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_cons :
    (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1

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

Tactic:
simp [findIdx?, findIdx?_go_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem image_parallelepiped (f : E →ₗ[ℝ] F) (v : ι → E) :
    f '' parallelepiped v = parallelepiped (f ∘ v)

Proof state:
ι : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
⊢ ⇑f '' parallelepiped v = parallelepiped (⇑f ∘ v)

Tactic:
simp only [parallelepiped, ← image_comp]

Result:
ι : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
⊢ (⇑f ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 = (fun t => ∑ i : ι, t i • (⇑f ∘ v) i) '' Icc 0 1

Proof state:
case h
ι : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
t : F
⊢ t ∈ (⇑f ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 ↔ t ∈ (fun t => ∑ i : ι, t i • (⇑f ∘ v) i) '' Icc 0 1

Tactic:
simp only [Function.comp_apply, _root_.map_sum, LinearMap.map_smulₛₗ, RingHom.id_apply]

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
⊢ (⇑f ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 = (fun t => ∑ i : ι, t i • (⇑f ∘ v) i) '' Icc 0 1

Tactic:
congr 1 with t

Result:
case h
ι : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
t : F
⊢ t ∈ (⇑f ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 ↔ t ∈ (fun t => ∑ i : ι, t i • (⇑f ∘ v) i) '' Icc 0 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
    (hj : j < (l.set i a).length) :
    (l.set i a)[j] = l[j]'(by simp at hj; exact hj) :=
  match l, i, j with
  | [], _, _ => by simp
  | _ :: _, 0, 0 => by contradiction
  | _ :: _, 0, _ + 1 => by simp
  | _ :: _, _ + 1, 0 => by simp
  | _ :: l, i + 1, j + 1 => by
    have g : i ≠ j := h ∘ congrArg (· + 1)
    simp [getElem_set_ne g]

Proof state:
α : Type u_1
l✝ : List α
i✝ j✝ : Nat
a head✝ : α
l : List α
i j : Nat
h : i + 1 ≠ j + 1
hj : j + 1 < ((head✝ :: l).set (i + 1) a).length
g : i ≠ j
⊢ ((head✝ :: l).set (i + 1) a)[j + 1] = (head✝ :: l)[j + 1]

Tactic:
simp [getElem_set_ne g]

Result:
no goals

Proof state:
α : Type ?u.62922
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < l.length
⊢ j < l.length

Tactic:
exact hj

Result:
no goals

Proof state:
α : Type ?u.62922
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < (l.set i a).length
⊢ j < l.length

Tactic:
simp at hj

Result:
α : Type ?u.62922
l : List α
i j : Nat
h : i ≠ j
a : α
hj : j < l.length
⊢ j < l.length

Proof state:
α : Type u_1
l : List α
i j : Nat
a head✝ : α
tail✝ : List α
h : 0 ≠ 0
hj : 0 < ((head✝ :: tail✝).set 0 a).length
⊢ ((head✝ :: tail✝).set 0 a)[0] = (head✝ :: tail✝)[0]

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
x✝¹ x✝ : Nat
h : x✝¹ ≠ x✝
hj : x✝ < ([].set x✝¹ a).length
⊢ ([].set x✝¹ a)[x✝] = [][x✝]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
a head✝ : α
tail✝ : List α
n✝ : Nat
h : 0 ≠ n✝ + 1
hj : n✝ + 1 < ((head✝ :: tail✝).set 0 a).length
⊢ ((head✝ :: tail✝).set 0 a)[n✝ + 1] = (head✝ :: tail✝)[n✝ + 1]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
a head✝ : α
tail✝ : List α
n✝ : Nat
h : n✝ + 1 ≠ 0
hj : 0 < ((head✝ :: tail✝).set (n✝ + 1) a).length
⊢ ((head✝ :: tail✝).set (n✝ + 1) a)[0] = (head✝ :: tail✝)[0]

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma birkhoffSet_apply [OrderBot α] (a : α) :
    birkhoffSet a = OrderIso.lowerSetSupIrred a

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
⊢ OrderIso.lowerSetSupIrred a = OrderIso.lowerSetSupIrred a

Tactic:
have : Subsingleton (OrderBot α) := inferInstance

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
this : Subsingleton (OrderBot α)
⊢ OrderIso.lowerSetSupIrred a = OrderIso.lowerSetSupIrred a

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
⊢ birkhoffSet a = ↑(OrderIso.lowerSetSupIrred a)

Tactic:
simp [birkhoffSet]

Result:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
⊢ OrderIso.lowerSetSupIrred a = OrderIso.lowerSetSupIrred a

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
a : α
this : Subsingleton (OrderBot α)
⊢ OrderIso.lowerSetSupIrred a = OrderIso.lowerSetSupIrred a

Tactic:
convert rfl

Result:
no goals
-- Mathlib/Topology/Irreducible.lean
theorem subset_closure_inter_of_isPreirreducible_of_isOpen {S U : Set X} (hS : IsPreirreducible S)
    (hU : IsOpen U) (h : (S ∩ U).Nonempty) : S ⊆ closure (S ∩ U)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure (S ∩ U)
⊢ False

Tactic:
obtain ⟨x, h₁, h₂, h₃⟩ :=
  hS _ (closure (S ∩ U))ᶜ hU isClosed_closure.isOpen_compl h (inter_compl_nonempty_iff.mpr h')

Result:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure (S ∩ U)
x : X
h₁ : x ∈ S
h₂ : x ∈ U
h₃ : x ∈ (closure (S ∩ U))ᶜ
⊢ False

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen U
h : (S ∩ U).Nonempty
⊢ S ⊆ closure (S ∩ U)

Tactic:
by_contra h'

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure (S ∩ U)
⊢ False

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S U : Set X
hS : IsPreirreducible S
hU : IsOpen U
h : (S ∩ U).Nonempty
h' : ¬S ⊆ closure (S ∩ U)
x : X
h₁ : x ∈ S
h₂ : x ∈ U
h₃ : x ∈ (closure (S ∩ U))ᶜ
⊢ False

Tactic:
exact h₃ (subset_closure ⟨h₁, h₂⟩)

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dZero_ker_eq_invariants : LinearMap.ker (dZero A) = invariants A.ρ

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ LinearMap.ker (dZero A) = A.ρ.invariants

Tactic:
ext x

Result:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
⊢ x ∈ LinearMap.ker (dZero A) ↔ x ∈ A.ρ.invariants

Proof state:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
⊢ x ∈ LinearMap.ker (dZero A) ↔ x ∈ A.ρ.invariants

Tactic:
simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, funext_iff]

Result:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
⊢ (∀ (x_1 : G), (dZero A) x x_1 = 0 x_1) ↔ ∀ (g : G), (A.ρ g) x - x = 0

Proof state:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A.V
⊢ (∀ (x_1 : G), (dZero A) x x_1 = 0 x_1) ↔ ∀ (g : G), (A.ρ g) x - x = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_not {x : BitVec w} {i : Nat} (h : i < w) : (~~~x)[i] = !x[i]

Proof state:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (2 ^ w - (x.toNat + 1)).testBit i = !x.toNat.testBit i

Tactic:
rw [Nat.testBit_two_pow_sub_succ x.isLt]

Result:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (decide (i < w) && !x.toNat.testBit i) = !x.toNat.testBit i

Proof state:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (~~~x)[i] = !x[i]

Tactic:
simp only [getElem_eq_testBit_toNat, toNat_not]

Result:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (2 ^ w - 1 - x.toNat).testBit i = !x.toNat.testBit i

Proof state:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (decide (i < w) && !x.toNat.testBit i) = !x.toNat.testBit i

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (2 ^ w - 1 - x.toNat).testBit i = !x.toNat.testBit i

Tactic:
rw [← Nat.sub_add_eq, Nat.add_comm 1]

Result:
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (2 ^ w - (x.toNat + 1)).testBit i = !x.toNat.testBit i
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_eq_integral_of_support_subset {a b} (h : support f ⊆ Ioc a b) :
    ∫ x in a..b, f x ∂μ = ∫ x, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
rcases le_total a b with hab | hab

Result:
case inl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

case inr
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Proof state:
case inl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
rw [integral_of_le hab, ← integral_indicator measurableSet_Ioc, indicator_eq_self.2 h]

Result:
no goals

Proof state:
case inr
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
rw [Ioc_eq_empty hab.not_lt, subset_empty_iff, support_eq_empty_iff] at h

Result:
case inr
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : f = 0
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Proof state:
case inr
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : f = 0
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ), f x ∂μ

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem of_union_of_dvd (h : ∀ s ∈ S, n ∣ s) (hS : S.Nonempty) [H : IsCyclotomicExtension S A B] :
    IsCyclotomicExtension (S ∪ {n}) A B

Proof state:
case refine_1.inr.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
obtain ⟨ζ, hζ⟩ := H.exists_prim_root hm

Result:
case refine_1.inr.intro.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ ∃ r, IsPrimitiveRoot r ↑s

Proof state:
case refine_1.inr.intro.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ IsPrimitiveRoot (ζ ^ ↑x) ↑s

Tactic:
convert hζ.pow_of_dvd x.ne_zero (dvd_mul_left (x : ℕ) s)

Result:
case h.e'_4
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ ↑s = ↑(s * x) / ↑x