harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Subset.lean
lemma preimage_val_sUnion : A ↓∩ (⋃₀ S) = ⋃₀ { (A ↓∩ B) | B ∈ S }

Proof state:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃₀ S = ⋃ a ∈ S, A ↓∩ a

Tactic:
simp_rw [sUnion_eq_biUnion, preimage_iUnion]

Result:
no goals

Proof state:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃₀ S = ⋃₀ {x | ∃ B ∈ S, A ↓∩ B = x}

Tactic:
rw [← Set.image, sUnion_image]

Result:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃₀ S = ⋃ a ∈ S, A ↓∩ a
-- Mathlib/Topology/PartialHomeomorph.lean
theorem continuousAt_iff_continuousAt_comp_left {f : Z → X} {x : Z} (h : f ⁻¹' e.source ∈ 𝓝 x) :
    ContinuousAt f x ↔ ContinuousAt (e ∘ f) x

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Tactic:
have h' : f ⁻¹' e.source ∈ 𝓝[univ] x := by rwa [nhdsWithin_univ]

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Tactic:
rw [← continuousWithinAt_univ, ← continuousWithinAt_univ,
  e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Tactic:
have hx : f x ∈ e.source := (mem_of_mem_nhds h :)

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ f ⁻¹' e.source ∈ 𝓝[univ] x

Tactic:
rwa [nhdsWithin_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_insertEntryIfNew_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} : containsKey k (insertEntryIfNew k v l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ containsKey k (insertEntryIfNew k v l) = true

Tactic:
rw [containsKey_insertEntryIfNew, BEq.refl, Bool.true_or]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
/-- See also `yonedaEquiv_naturality'` for a more general version. -/
lemma yonedaEquiv_naturality {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F)
    (g : Y ⟶ X) : F.map g.op (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ ((yoneda.obj X).map g.op ≫ f.app (op Y)) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)

Tactic:
dsimp

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ f.app (op Y) (g ≫ 𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ F.map g.op (yonedaEquiv f) = yonedaEquiv (yoneda.map g ≫ f)

Tactic:
change (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)

Tactic:
rw [← f.naturality]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ ((yoneda.obj X).map g.op ≫ f.app (op Y)) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ f.app (op Y) (g ≫ 𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem exists_open_nhds_one_mul_subset {U : Set M} (hU : U ∈ 𝓝 (1 : M)) :
    ∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ V * V ⊆ U

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
U : Set M
hU : U ∈ 𝓝 1
⊢ ∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U

Tactic:
simpa only [mul_subset_iff] using exists_open_nhds_one_split hU

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem eq_bot_of_card_le_two (h2 : card α ≤ 2) : alternatingGroup α = ⊥

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : card α ≤ 2
a✝ : Nontrivial α
hα' : card α = 2
⊢ alternatingGroup α = ⊥

Tactic:
rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by norm_num),
  Nat.card_eq_fintype_card, two_mul_card_alternatingGroup, mul_one, card_perm, hα',
  Nat.factorial_two]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : card α ≤ 2
⊢ alternatingGroup α = ⊥

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : card α ≤ 2
a✝ : Nontrivial α
⊢ alternatingGroup α = ⊥

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : card α ≤ 2
a✝ : Nontrivial α
⊢ card α = 2

Tactic:
exact h2.antisymm Fintype.one_lt_card

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : card α ≤ 2
a✝ : Nontrivial α
⊢ alternatingGroup α = ⊥

Tactic:
suffices hα' : card α = 2 by
  rw [Subgroup.eq_bot_iff_card, ← Nat.mul_right_inj (a := 2) (by norm_num),
    Nat.card_eq_fintype_card, two_mul_card_alternatingGroup, mul_one, card_perm, hα',
    Nat.factorial_two]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : card α ≤ 2
a✝ : Nontrivial α
⊢ card α = 2

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : card α ≤ 2
a✝ : Nontrivial α
hα' : card α = 2
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b

Proof state:
α : Type u_1
a b : α
l : List α
⊢ (some b).getD a = b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a b : α
l : List α
⊢ (l ++ [b]).getLastD a = b

Tactic:
rw [getLastD_eq_getLast?, getLast?_concat]

Result:
α : Type u_1
a b : α
l : List α
⊢ (some b).getD a = b
-- Mathlib/Computability/Primrec.lean
theorem listLookup [DecidableEq α] : Primrec₂ (List.lookup : α → List (α × β) → Option β) :=
  (to₂ <| list_rec snd (const none) <|
    to₂ <|
      cond (Primrec.beq.comp (fst.comp fst) (fst.comp <| fst.comp snd))
        (option_some.comp <| snd.comp <| fst.comp snd)
        (snd.comp <| snd.comp snd)).of_eq
  fun a ps => by
  induction' ps with p ps ih <;> simp [List.lookup, *]
  cases ha : a == p.1 <;> simp [ha]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
ps : List (α × β)
⊢ (List.recOn (a, ps).2 none fun b l IH =>
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps

Tactic:
induction' ps with p ps ih <;> simp [List.lookup, *]

Result:
case cons
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH =>
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (a, ps).2 none fun b l IH =>
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match a == p.1 with
    | true => some p.2
    | false => List.lookup a ps

Tactic:
cases ha : a == p.1 <;> simp [ha]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem eq_emptyOn_or_nonempty (M : Matroid α) : M = emptyOn α ∨ Matroid.Nonempty M

Proof state:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ ∨ M.Nonempty

Tactic:
exact M.E.eq_empty_or_nonempty.elim Or.inl (fun h ↦ Or.inr ⟨h⟩)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ M = emptyOn α ∨ M.Nonempty

Tactic:
rw [← ground_eq_empty_iff]

Result:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ ∨ M.Nonempty
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
@[simp] lemma natTrailingDegree_eq_zero : natTrailingDegree p = 0 ↔ p = 0 ∨ coeff p 0 ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0

Tactic:
simp [natTrailingDegree, or_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem set_smul_mem_nhds_zero_iff {s : Set α} {c : G₀} (hc : c ≠ 0) :
    c • s ∈ 𝓝 (0 : α) ↔ s ∈ 𝓝 (0 : α)

Proof state:
α : Type u_2
G₀ : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ s ∈ 𝓝 0

Tactic:
refine Iff.trans ?_ (smul_mem_nhds_smul_iff₀ hc)

Result:
α : Type u_2
G₀ : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 (c • 0)

Proof state:
α : Type u_2
G₀ : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 (c • 0)

Tactic:
rw [smul_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_Icc : Neg.neg '' Icc a b = Icc (-b) (-a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ Neg.neg '' Icc a b = Icc (-b) (-a)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_eq_succ_iff_cons :
    #s = n + 1 ↔ ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n :=
  ⟨cons_induction_on s (by simp) fun a s _ _ _ => ⟨a, s, by simp_all⟩,
   fun ⟨a, t, _, hs, _⟩ => by simpa [← hs]⟩

Proof state:
α : Type u_1
s✝ : Finset α
n : ℕ
a : α
s : Finset α
x✝² : a ∉ s
x✝¹ : #s = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
x✝ : #(cons a s x✝²) = n + 1
⊢ ∃ (h : a ∉ s), cons a s h = cons a s x✝² ∧ #s = n

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
n : ℕ
x✝ : ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
a : α
t : Finset α
w✝ : a ∉ t
hs : cons a t w✝ = s
right✝ : #t = n
⊢ #s = n + 1

Tactic:
simpa [← hs]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
n : ℕ
⊢ #∅ = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = ∅ ∧ #t = n

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem IsPiSystem.insert_empty {S : Set (Set α)} (h_pi : IsPiSystem S) :
    IsPiSystem (insert ∅ S)

Proof state:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert ∅ S)

Tactic:
intro s hs t ht hst

Result:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert ∅ S

Proof state:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

Tactic:
simp [hs]

Result:
no goals

Proof state:
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
rcases ht with ht | ht

Result:
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S

case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S

Proof state:
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S

Tactic:
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)

Result:
no goals

Proof state:
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert ∅ S

Tactic:
rcases hs with hs | hs

Result:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S

Proof state:
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : (s ∩ t).Nonempty
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S

Tactic:
simp [ht]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem get?_ofSeq (s : Seq α) (n) : get? (ofSeq s) n = Computation.pure (Seq.get? s n)

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).head = Computation.pure (s.get? n)

Tactic:
rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]

Result:
no goals

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ (↑s).get? n = Computation.pure (s.get? n)

Tactic:
dsimp [get?]

Result:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).head = Computation.pure (s.get? n)
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem zero_opow {a : Ordinal} (a0 : a ≠ 0) : (0 : Ordinal) ^ a = 0

Proof state:
a : Ordinal.{u_1}
a0 : a ≠ 0
⊢ 0 ^ a = 0

Tactic:
rwa [zero_opow', Ordinal.sub_eq_zero_iff_le, one_le_iff_ne_zero]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem map_lcm [CommGroupWithZero R] {f : ArithmeticFunction R}
    (hf : f.IsMultiplicative) {x y : ℕ} (hf_gcd : f (x.gcd y) ≠ 0) :
    f (x.lcm y) = f x * f y / f (x.gcd y)

Proof state:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
x y : ℕ
hf_gcd : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f x * f y / f (x.gcd y)

Tactic:
rw [←hf.lcm_apply_mul_gcd_apply, mul_div_cancel_right₀ _ hf_gcd]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
@[simp] lemma vadd_set_vsub_vadd_set (v : G) (s t : Set P) : (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t

Proof state:
case h
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v : G
s t : Set P
x✝ : G
⊢ x✝ ∈ (v +ᵥ s) -ᵥ (v +ᵥ t) ↔ x✝ ∈ s -ᵥ t

Tactic:
simp [mem_vsub, mem_vadd_set]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v : G
s t : Set P
⊢ (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t

Tactic:
ext

Result:
case h
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v : G
s t : Set P
x✝ : G
⊢ x✝ ∈ (v +ᵥ s) -ᵥ (v +ᵥ t) ↔ x✝ ∈ s -ᵥ t
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem div (dvd : p ∣ b) : padicValNat p (b / p) = padicValNat p b - 1

Proof state:
p b : ℕ
hp : Fact (Nat.Prime p)
dvd : p ∣ b
⊢ padicValNat p (b / p) = padicValNat p b - 1

Tactic:
rw [padicValNat.div_of_dvd dvd, padicValNat_self]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
/-- If a family of sets `𝒜` is measure-dense in `X`, then any measurable set with finite measure
can be approximated by sets in `𝒜` with finite measure. -/
lemma Measure.MeasureDense.fin_meas_approx (h𝒜 : μ.MeasureDense 𝒜) {s : Set X}
    (ms : MeasurableSet s) (hμs : μ s ≠ ∞) (ε : ℝ) (ε_pos : 0 < ε) :
    ∃ t ∈ 𝒜, μ t ≠ ∞ ∧ μ (s ∆ t) < ENNReal.ofReal ε

Proof state:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
ht : μ (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, μ t ≠ ⊤ ∧ μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
exact ⟨t, t_mem, (measure_ne_top_iff_of_symmDiff <| ne_top_of_lt ht).1 hμs, ht⟩

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ 𝒜, μ t ≠ ⊤ ∧ μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases h𝒜.approx s ms hμs ε ε_pos with ⟨t, t_mem, ht⟩

Result:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
ht : μ (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, μ t ≠ ⊤ ∧ μ (s ∆ t) < ENNReal.ofReal ε
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
theorem eigenvalues_eq (i : n) :
    (hA.eigenvalues i) = RCLike.re (dotProduct (star ⇑(hA.eigenvectorBasis i))
    (A *ᵥ ⇑(hA.eigenvectorBasis i)))

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
i : n
⊢ hA.eigenvalues i =
    RCLike.re
      (star ((WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis i)) ⬝ᵥ
        A *ᵥ (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis i))

Tactic:
simp only [mulVec_eigenvectorBasis, dotProduct_smul,← EuclideanSpace.inner_eq_star_dotProduct,
  inner_self_eq_norm_sq_to_K, RCLike.smul_re, hA.eigenvectorBasis.orthonormal.1 i,
  mul_one, algebraMap.coe_one, one_pow, RCLike.one_re]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem divisors_subset_properDivisors {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :
    divisors m ⊆ properDivisors n

Proof state:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ ∀ ⦃x : ℕ⦄, x ∈ m.divisors → x ∈ n.properDivisors

Tactic:
intro x hx

Result:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
hx : x ∈ m.divisors
⊢ x ∈ n.properDivisors

Proof state:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
hx : x ∈ m.divisors
⊢ x ∈ n.properDivisors

Tactic:
exact
  Nat.mem_properDivisors.2
    ⟨(Nat.mem_divisors.1 hx).1.trans h,
      lt_of_le_of_lt (divisor_le hx)
        (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩

Result:
no goals

Proof state:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ m.divisors ⊆ n.properDivisors

Tactic:
apply Finset.subset_iff.2

Result:
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ ∀ ⦃x : ℕ⦄, x ∈ m.divisors → x ∈ n.properDivisors
-- Mathlib/CategoryTheory/Products/Bifunctor.lean
theorem diagonal (F : C × D ⥤ E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') :
    F.map ((𝟙 X, g) : (X, Y) ⟶ (X, Y')) ≫ F.map ((f, 𝟙 Y') : (X, Y') ⟶ (X', Y')) =
      F.map ((f, g) : (X, Y) ⟶ (X', Y'))

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (𝟙 X, g) ≫ F.map (f, 𝟙 Y') = F.map (f, g)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₂_of_isCharNeTwoNF : W.b₂ = 4 * W.a₂

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₂ = 4 * W.a₂

Tactic:
rw [b₂, a₁_of_isCharNeTwoNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₂ = 4 * W.a₂

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₂ = 4 * W.a₂

Tactic:
ring1

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem lintegral_deterministic {f : β → ℝ≥0∞} {g : α → β} {a : α} (hg : Measurable g)
    [MeasurableSingletonClass β] : ∫⁻ x, f x ∂deterministic g hg a = f (g a)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝ : MeasurableSingletonClass β
⊢ ∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)

Tactic:
rw [deterministic_apply, lintegral_dirac (g a) f]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsion_iff_isTorsion_nat [AddCommMonoid M] :
    AddMonoid.IsTorsion M ↔ Module.IsTorsion ℕ M

Proof state:
case refine_1
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion M
x : M
⊢ ∃ a, a • x = 0

Tactic:
obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero

Result:
case refine_1.intro.intro
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ a, a • x = 0

Proof state:
M : Type u_2
inst✝ : AddCommMonoid M
⊢ IsTorsion M ↔ Module.IsTorsion ℕ M

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩

Result:
case refine_1
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion M
x : M
⊢ ∃ a, a • x = 0

case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ IsOfFinAddOrder x

Proof state:
case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0

Tactic:
obtain ⟨n, hn⟩ := @h x

Result:
case refine_2.intro
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
n : ↥ℕ⁰
hn : n • x = 0
⊢ ∃ n, 0 < n ∧ n • x = 0

Proof state:
case refine_1.intro.intro
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion M
x : M
n : ℕ
h0 : 0 < n
hn : n • x = 0
⊢ ∃ a, a • x = 0

Tactic:
exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩

Result:
no goals

Proof state:
case refine_2.intro
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
n : ↥ℕ⁰
hn : n • x = 0
⊢ ∃ n, 0 < n ∧ n • x = 0

Tactic:
exact ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩

Result:
no goals

Proof state:
case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ IsOfFinAddOrder x

Tactic:
rw [isOfFinAddOrder_iff_nsmul_eq_zero]

Result:
case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : Module.IsTorsion ℕ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0
-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
lemma rootForm_pos_of_ne_zero {x : M} (hx : x ∈ P.rootSpan) (h : x ≠ 0) :
    0 < P.RootForm x x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
h : x ≠ 0
⊢ 0 < (P.RootForm x) x

Tactic:
apply (P.zero_le_rootForm x).lt_of_ne

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
h : x ≠ 0
⊢ 0 ≠ (P.RootForm x) x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
h : 0 = (P.RootForm x) x
⊢ x = 0

Tactic:
exact P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero hx h.symm

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
h : x ≠ 0
⊢ 0 ≠ (P.RootForm x) x

Tactic:
contrapose! h

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : LinearOrderedCommRing R
inst✝¹ : Module R M
inst✝ : Module R N
P : RootPairing ι R M N
x : M
hx : x ∈ P.rootSpan
h : 0 = (P.RootForm x) x
⊢ x = 0