harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem mem_map_indicator_ae_iff_of_zero_nmem [Zero β] {t : Set β} (ht : (0 : β) ∉ t) :
    t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Tactic:
change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun x => 0) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun x => 0) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Tactic:
simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Tactic:
classical
rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]
change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
simp only [ht, if_false, Set.compl_empty, Set.empty_diff, Set.inter_univ, Set.preimage_const]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0

Tactic:
rw [mem_map, mem_ae_iff, Set.indicator_preimage, Set.ite, Set.compl_union, Set.compl_inter]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∉ t
⊢ μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
/-- If there is any isomorphism `⊥ ⟶ G.obj ⊥`, then `G` preserves initial objects. -/
lemma preservesInitial_of_isIso (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : IsIso f] :
    PreservesColimit (Functor.empty.{0} C) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
f : ⊥_ D ⟶ G.obj (⊥_ C)
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
exact PreservesInitial.of_iso_comparison G

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
f : ⊥_ D ⟶ G.obj (⊥_ C)
i : IsIso f
⊢ PreservesColimit (Functor.empty C) G

Tactic:
rw [Subsingleton.elim f (initialComparison G)] at i

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
f : ⊥_ D ⟶ G.obj (⊥_ C)
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem g_apply_fromCoset (x : B) (y : X) :
    g x (fromCoset y) = fromCoset ⟨x • ↑y,
      by obtain ⟨z, hz⟩ := y.2; exact ⟨x * z, by simp [← hz, smul_smul]⟩⟩ := rfl

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
y : ↑X
z : ↑B
hz : (fun x => x • ↑(Hom.hom f).range) z = ↑y
⊢ (fun x => x • ↑(Hom.hom f).range) (x * z) = x • ↑y

Tactic:
simp [← hz, smul_smul]

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
y : ↑X
⊢ x • ↑y ∈ X

Tactic:
obtain ⟨z, hz⟩ := y.2

Result:
case intro
A B : Grp
f : A ⟶ B
x : ↑B
y : ↑X
z : ↑B
hz : (fun x => x • ↑(Hom.hom f).range) z = ↑y
⊢ x • ↑y ∈ X

Proof state:
case intro
A B : Grp
f : A ⟶ B
x : ↑B
y : ↑X
z : ↑B
hz : (fun x => x • ↑(Hom.hom f).range) z = ↑y
⊢ x • ↑y ∈ X

Tactic:
exact ⟨x * z, by simp [← hz, smul_smul]⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_push [Monad m] [LawfulMonad m] (l : Array α) (a : α) (f : β → α → m β) (b) :
    (l.push a).foldlM f b = l.foldlM f b >>= fun b => f b a

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
a : α
f : β → α → m β
b : β
⊢ foldlM f b (l.push a) = do
    let b ← foldlM f b l
    f b a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem flatMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Array β)) :
    l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a)

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (Array β)
acc : List (List β)
⊢ List.foldlM (fun x y => HAppend.hAppend x <$> f y) acc.reverse.flatten.toArray [] =
    toArray <$> flatMapM.loop (fun a => Array.toList <$> f a) [] acc

Tactic:
simp only [foldlM_nil, flatMapM.loop, map_pure]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_mul_add_lt_opow_succ {b u v w : Ordinal} (hvb : v < b) (hw : w < b ^ u) :
    b ^ u * v + w < b ^ succ u

Proof state:
case h.e'_4
b u v w : Ordinal.{u_1}
hvb : v < b
hw : w < b ^ u
⊢ b ^ succ u = b ^ u * b

Tactic:
exact opow_succ b u

Result:
no goals

Proof state:
b u v w : Ordinal.{u_1}
hvb : v < b
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ succ u

Tactic:
convert (opow_mul_add_lt_opow_mul_succ v hw).trans_le
  (mul_le_mul_left' (succ_le_of_lt hvb) _) using 1

Result:
case h.e'_4
b u v w : Ordinal.{u_1}
hvb : v < b
hw : w < b ^ u
⊢ b ^ succ u = b ^ u * b
-- Mathlib/Data/List/Chain.lean
theorem chain_pmap_of_chain {S : β → β → Prop} {p : α → Prop} {f : ∀ a, p a → β}
    (H : ∀ a b ha hb, R a b → S (f a ha) (f b hb)) {a : α} {l : List α} (hl₁ : Chain R a l)
    (ha : p a) (hl₂ : ∀ a ∈ l, p a) : Chain S (f a ha) (List.pmap f l hl₂)

Proof state:
case nil
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a : α
hl₁ : Chain R a []
ha : p a
hl₂ : ∀ (a : α), a ∈ [] → p a
⊢ Chain S (f a ha) (pmap f [] hl₂)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
lh : α
lt : List α
l_ih : ∀ {a : α}, Chain R a lt → ∀ (ha : p a) (hl₂ : ∀ (a : α), a ∈ lt → p a), Chain S (f a ha) (pmap f lt hl₂)
a : α
hl₁ : Chain R a (lh :: lt)
ha : p a
hl₂ : ∀ (a : α), a ∈ lh :: lt → p a
⊢ Chain S (f a ha) (pmap f (lh :: lt) hl₂)

Tactic:
simp [H _ _ _ _ (rel_of_chain_cons hl₁), l_ih (chain_of_chain_cons hl₁)]

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a : α
l : List α
hl₁ : Chain R a l
ha : p a
hl₂ : ∀ (a : α), a ∈ l → p a
⊢ Chain S (f a ha) (pmap f l hl₂)

Tactic:
induction' l with lh lt l_ih generalizing a

Result:
case nil
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
a : α
hl₁ : Chain R a []
ha : p a
hl₂ : ∀ (a : α), a ∈ [] → p a
⊢ Chain S (f a ha) (pmap f [] hl₂)

case cons
α : Type u
β : Type v
R : α → α → Prop
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb)
lh : α
lt : List α
l_ih : ∀ {a : α}, Chain R a lt → ∀ (ha : p a) (hl₂ : ∀ (a : α), a ∈ lt → p a), Chain S (f a ha) (pmap f lt hl₂)
a : α
hl₁ : Chain R a (lh :: lt)
ha : p a
hl₂ : ∀ (a : α), a ∈ lh :: lt → p a
⊢ Chain S (f a ha) (pmap f (lh :: lt) hl₂)
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_conj {σ τ : Perm α} : (τ * σ * τ⁻¹).cycleType = σ.cycleType

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ : Perm α
hσ : σ.IsCycle
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType

Tactic:
rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]

Result:
no goals

Proof state:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
⊢ (τ * 1 * τ⁻¹).cycleType = cycleType 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ (τ * σ * τ⁻¹).cycleType = σ.cycleType

Tactic:
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, hσ.conj.cycleType, card_support_conj]
| induction_disjoint σ π hd _ hσ hπ =>
  rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]

Result:
no goals

Proof state:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ σ π : Perm α
hd : σ.Disjoint π
a✝ : σ.IsCycle
hσ : (τ * σ * τ⁻¹).cycleType = σ.cycleType
hπ : (τ * π * τ⁻¹).cycleType = π.cycleType
⊢ (τ * (σ * π) * τ⁻¹).cycleType = (σ * π).cycleType

Tactic:
rw [← conj_mul, hd.cycleType, (hd.conj _).cycleType, hσ, hπ]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem mul_dvd_mul_left (a : α) (h : b ∣ c) : a * b ∣ a * c

Proof state:
case h
α : Type u_1
inst✝ : Monoid α
b a d : α
⊢ a * (b * d) = a * b * d

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : Monoid α
b a d : α
⊢ a * b ∣ a * (b * d)

Tactic:
use d

Result:
case h
α : Type u_1
inst✝ : Monoid α
b a d : α
⊢ a * (b * d) = a * b * d

Proof state:
α : Type u_1
inst✝ : Monoid α
b c a : α
h : b ∣ c
⊢ a * b ∣ a * c

Tactic:
obtain ⟨d, rfl⟩ := h

Result:
case intro
α : Type u_1
inst✝ : Monoid α
b a d : α
⊢ a * b ∣ a * (b * d)
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive (attr := simp)] lemma MulEquiv.mulDissociated_preimage (e : β ≃* α) :
    MulDissociated (e ⁻¹' s) ↔ MulDissociated s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommGroup α
inst✝ : CommGroup β
s : Set α
e : β ≃* α
⊢ MulDissociated (⇑e ⁻¹' s) ↔ MulDissociated s

Tactic:
simp [MulDissociated, InjOn, ← e.finsetCongr.forall_congr_right, ← e.apply_eq_iff_eq,
  (Finset.map_injective _).eq_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_eq_some {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w, l[n] = a

Proof state:
w n : Nat
a : Bool
l : BitVec w
⊢ l[n]? = some a ↔ ∃ h, l[n] = a

Tactic:
simp only [getElem?_def]

Result:
w n : Nat
a : Bool
l : BitVec w
⊢ (if h : n < w then some l[n] else none) = some a ↔ ∃ h, l[n] = a

Proof state:
case isFalse
w n : Nat
a : Bool
l : BitVec w
h✝ : ¬n < w
⊢ ∀ (x : n < w), ¬l[n] = a

Tactic:
omega

Result:
no goals

Proof state:
w n : Nat
a : Bool
l : BitVec w
⊢ (if h : n < w then some l[n] else none) = some a ↔ ∃ h, l[n] = a

Tactic:
split

Result:
case isTrue
w n : Nat
a : Bool
l : BitVec w
h✝ : n < w
⊢ some l[n] = some a ↔ ∃ h, l[n] = a

case isFalse
w n : Nat
a : Bool
l : BitVec w
h✝ : ¬n < w
⊢ none = some a ↔ ∃ h, l[n] = a

Proof state:
case isTrue
w n : Nat
a : Bool
l : BitVec w
h✝ : n < w
⊢ some l[n] = some a ↔ ∃ h, l[n] = a

Tactic:
simp_all

Result:
no goals

Proof state:
case isFalse
w n : Nat
a : Bool
l : BitVec w
h✝ : ¬n < w
⊢ none = some a ↔ ∃ h, l[n] = a

Tactic:
simp

Result:
case isFalse
w n : Nat
a : Bool
l : BitVec w
h✝ : ¬n < w
⊢ ∀ (x : n < w), ¬l[n] = a
-- Mathlib/Algebra/Small/Group.lean
@[to_additive (attr := simp)]
lemma equivShrink_symm_mul [Mul α] [Small α] (x y : Shrink α) :
    (equivShrink α).symm (x * y) = (equivShrink α).symm x * (equivShrink α).symm y

Proof state:
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x * (equivShrink α).symm y)) =
    (equivShrink α).symm x * (equivShrink α).symm y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm (x * y) = (equivShrink α).symm x * (equivShrink α).symm y

Tactic:
rw [Equiv.mul_def]

Result:
α : Type u_1
inst✝¹ : Mul α
inst✝ : Small.{u_2, u_1} α
x y : Shrink.{u_2, u_1} α
⊢ (equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x * (equivShrink α).symm y)) =
    (equivShrink α).symm x * (equivShrink α).symm y
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_node4L {P l x m y r} :
    @All α P (node4L l x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
cases m <;> simp [node4L, all_node', All, all_node3L, and_assoc]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem le_card_nonuniformWitness (h : ¬G.IsUniform ε s t) :
    #s * ε ≤ #(G.nonuniformWitness ε s t)

Proof state:
case neg
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : ¬WellOrderingRel s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε t s).2)

Tactic:
exact G.right_nonuniformWitnesses_card fun i => h i.symm

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitness ε s t))

Tactic:
unfold nonuniformWitness

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2))

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#s) * ε ≤ ↑(#(if WellOrderingRel s t then (G.nonuniformWitnesses ε s t).1 else (G.nonuniformWitnesses ε t s).2))

Tactic:
split_ifs

Result:
case pos
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : WellOrderingRel s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).1)

case neg
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : ¬WellOrderingRel s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε t s).2)

Proof state:
case pos
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : WellOrderingRel s t
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).1)

Tactic:
exact G.left_nonuniformWitnesses_card h

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem continuous_map_iff [TopologicalSpace Y] {f : X → Y} :
    Continuous (OnePoint.map f) ↔
      Continuous f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x => ↑(f x)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧ Continuous fun x => ↑(f x)) ↔
    Continuous (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)

Tactic:
exact and_comm

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous (OnePoint.map f) ↔ Continuous f ∧ Tendsto f (coclosedCompact X) (coclosedCompact Y)

Tactic:
simp_rw [continuous_iff, map_some, ← comap_coe_nhds_infty, tendsto_comap_iff, map_infty,
  isOpenEmbedding_coe.isInducing.continuous_iff (Y := Y)]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Tendsto (fun x => ↑(f x)) (comap some (𝓝 ∞)) (𝓝 ∞) ∧ Continuous fun x => ↑(f x)) ↔
    Continuous (some ∘ f) ∧ Tendsto (some ∘ f) (comap some (𝓝 ∞)) (𝓝 ∞)
-- Mathlib/Algebra/Lie/TraceForm.lean
lemma lowerCentralSeries_one_inf_center_le_ker_traceForm [Module.Free R M] [Module.Finite R M] :
    lowerCentralSeries R L L 1 ⊓ LieAlgebra.center R L ≤ LinearMap.ker (traceForm R L M)

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hz : z ∈ lowerCentralSeries R L L 1
hzc : z ∈ LieAlgebra.center R L
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
⊢ 1 ⊗ₜ[R] z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1

Tactic:
simp only [lowerCentralSeries_succ, lowerCentralSeries_zero] at hz ⊢

Result:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hzc : z ∈ LieAlgebra.center R L
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : z ∈ ⁅⊤, ⊤⁆
⊢ 1 ⊗ₜ[R] z ∈ ⁅⊤, ⊤⁆

Proof state:
R : Type u_1
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : LieRing.IsNilpotent L
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
z : L
hzc : z ∈ LieAlgebra.center R L
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : z ∈ ⁅⊤, ⊤⁆
⊢ 1 ⊗ₜ[R] z ∈ LieSubmodule.baseChange A ⁅⊤, ⊤⁆

Tactic:
exact Submodule.tmul_mem_baseChange_of_mem 1 hz

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
/-- A commutative square involving the morphisms `mor₂` of two distinguished triangles
can be extended as morphism of triangles -/
lemma complete_distinguished_triangle_morphism₁ (T₁ T₂ : Triangle C)
    (hT₁ : T₁ ∈ distTriang C) (hT₂ : T₂ ∈ distTriang C) (b : T₁.obj₂ ⟶ T₂.obj₂)
    (c : T₁.obj₃ ⟶ T₂.obj₃) (comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂) :
    ∃ (a : T₁.obj₁ ⟶ T₂.obj₁), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧
      T₁.mor₃ ≫ a⟦(1 : ℤ)⟧' = c ≫ T₂.mor₃

Proof state:
case intro.intro.refine_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)

Tactic:
dsimp at ha₂

Result:
case intro.intro.refine_1.a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : (-(shiftFunctor C 1).map T₁.mor₁) ≫ (shiftFunctor C 1).map b = a ≫ (-(shiftFunctor C 1).map T₂.mor₁)
⊢ (shiftFunctor C 1).map (T₁.mor₁ ≫ b) = (shiftFunctor C 1).map ((shiftFunctor C 1).preimage a ≫ T₂.mor₁)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.Inv_atomToCNF (heq : aig.decls[upper] = .atom a) :
    State.Inv (aig := aig) (Decl.atomToCNF (.inr ⟨upper, h⟩) (.inl a))

Proof state:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
a : Nat
heq : aig.decls[upper] = Decl.atom a
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig assign1) (Decl.atomToCNF (Sum.inr ⟨upper, h⟩) (Sum.inl a))

Tactic:
simp [CNF.sat_def, denote_idx_atom heq]

Result:
no goals

Proof state:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
a : Nat
heq : aig.decls[upper] = Decl.atom a
⊢ Inv (Decl.atomToCNF (Sum.inr ⟨upper, h⟩) (Sum.inl a))

Tactic:
intro assign1

Result:
upper : Nat
aig : AIG Nat
h : upper < aig.decls.size
a : Nat
heq : aig.decls[upper] = Decl.atom a
assign1 : Nat → Bool
⊢ CNF.Sat (cnfSatAssignment aig assign1) (Decl.atomToCNF (Sum.inr ⟨upper, h⟩) (Sum.inl a))
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
/-- The **Cauchy-Schwarz inequality** for positive semidefinite forms. -/
lemma apply_mul_apply_le_of_forall_zero_le (hs : ∀ x, 0 ≤ B x x) (x y : M) :
    (B x y) * (B y x) ≤ (B x x) * (B y y)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x✝ y✝ x y : M
⊢ 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)

Tactic:
rw [← apply_smul_sub_smul_sub_eq B x y]

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x✝ y✝ x y : M
⊢ 0 ≤ (B ((B x) y • x - (B x) x • y)) ((B x) y • x - (B x) x • y)

Proof state:
case inl
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : 0 < (B x) x
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux x y) hx

Result:
no goals

Proof state:
case inr.inl
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : 0 < (B y) y
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
rw [mul_comm (B x y), mul_comm (B x x)]

Result:
case inr.inl
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : 0 < (B y) y
⊢ (B y) x * (B x) y ≤ (B y) y * (B x) x

Proof state:
case inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
replace hx : B x x = 0 := le_antisymm hx (hs x)

Result:
case inr
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Proof state:
case inr.inl
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : 0 < (B y) y
⊢ (B y) x * (B x) y ≤ (B y) y * (B x) x

Tactic:
exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux y x) hy

Result:
no goals