harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem quasiSeparated_eq_diagonal_is_quasiCompact :
    @QuasiSeparated = MorphismProperty.diagonal @QuasiCompact

Proof state:
⊢ @QuasiSeparated = MorphismProperty.diagonal @QuasiCompact

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ QuasiSeparated x✝ ↔ MorphismProperty.diagonal (@QuasiCompact) x✝

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ QuasiSeparated x✝ ↔ MorphismProperty.diagonal (@QuasiCompact) x✝

Tactic:
exact quasiSeparated_iff _

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem transAssocReparamAux_mem_I (t : I) : transAssocReparamAux t ∈ I

Proof state:
t : ↑I
⊢ transAssocReparamAux t ∈ I

Tactic:
unfold transAssocReparamAux

Result:
t : ↑I
⊢ (if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I

Proof state:
t : ↑I
⊢ (if ↑t ≤ 1 / 4 then 2 * ↑t else if ↑t ≤ 1 / 2 then ↑t + 1 / 4 else 1 / 2 * (↑t + 1)) ∈ I

Tactic:
split_ifs <;> constructor <;> linarith [unitInterval.le_one t, unitInterval.nonneg t]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem join_zero : (0 : Measure (Measure α)).join = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
⊢ join 0 = 0

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (join 0) s = 0 s

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (join 0) s = 0 s

Tactic:
simp only [hs, join_apply, lintegral_zero_measure, coe_zero, Pi.zero_apply]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem exists_of_mem_map {f} {b : β} : ∀ {s : WSeq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b
  | ⟨g, al⟩, h => by
    let ⟨o, om, oe⟩ := Seq.exists_of_mem_map h
    rcases o with - | a
    · injection oe
    injection oe with h'
    exact ⟨a, om, h'⟩

Proof state:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
o : Option α
om : o ∈ ⟨g, al⟩
oe : Option.map f o = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
rcases o with - | a

Result:
case none
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
om : none ∈ ⟨g, al⟩
oe : Option.map f none = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Proof state:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
let ⟨o, om, oe⟩ := Seq.exists_of_mem_map h

Result:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
o : Option α
om : o ∈ ⟨g, al⟩
oe : Option.map f o = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Proof state:
case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
h' : f a = b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
exact ⟨a, om, h'⟩

Result:
no goals

Proof state:
case none
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
om : none ∈ ⟨g, al⟩
oe : Option.map f none = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
injection oe

Result:
no goals

Proof state:
case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
injection oe with h'

Result:
case some
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ ⟨g, al⟩
h' : f a = b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b
-- Mathlib/Order/OrderIsoNat.lean
theorem wellFoundedGT_iff_monotone_chain_condition' [Preorder α] :
    WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m

Proof state:
case refine_1.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
n : ℕ
H : ∀ x ∈ Set.range ⇑a, ¬x > a n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ WellFoundedGT α

Tactic:
rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_no_descending_seq]

Result:
case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ IsEmpty ((fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2)

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

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

Result:
case refine_1
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ WellFoundedGT α

Proof state:
case refine_2.intro
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a.swap.toRelHom.toOrderHom n < a.swap.toRelHom.toOrderHom m
⊢ False

Tactic:
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ False

Tactic:
obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom

Result:
case refine_2.intro
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → ¬a.swap.toRelHom.toOrderHom n < a.swap.toRelHom.toOrderHom m
⊢ False

Proof state:
case refine_1
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Tactic:
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)

Result:
case refine_1.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
h : WellFoundedGT α
a : ℕ →o α
n : ℕ
H : ∀ x ∈ Set.range ⇑a, ¬x > a n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m

Proof state:
case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
⊢ IsEmpty ((fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2)

Tactic:
refine ⟨fun a => ?_⟩

Result:
case refine_2
α : Type u_1
inst✝ : Preorder α
h : ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m
a : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 > x2
⊢ False
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem suppPreservation_iff_uniform : q.SuppPreservation ↔ q.IsUniform

Proof state:
case mpr
F : Type u → Type u
q : QPF F
⊢ IsUniform → SuppPreservation

Tactic:
rintro h α ⟨a, f⟩

Result:
case mpr.mk
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Proof state:
case mpr.mk
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Tactic:
rwa [supp_eq_of_isUniform, PFunctor.supp_eq]

Result:
no goals

Proof state:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ f '' univ = f' '' univ

Tactic:
rw [← PFunctor.supp_eq, ← PFunctor.supp_eq, ← h, h', h]

Result:
no goals

Proof state:
case mp
F : Type u → Type u
q : QPF F
⊢ SuppPreservation → IsUniform

Tactic:
intro h α a a' f f' h'

Result:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ f '' univ = f' '' univ

Proof state:
F : Type u → Type u
q : QPF F
⊢ SuppPreservation ↔ IsUniform

Tactic:
constructor

Result:
case mp
F : Type u → Type u
q : QPF F
⊢ SuppPreservation → IsUniform

case mpr
F : Type u → Type u
q : QPF F
⊢ IsUniform → SuppPreservation
-- Mathlib/Data/List/Cycle.lean
theorem pmap_next_eq_rotate_one (h : Nodup l) : (l.pmap l.next fun _ h => h) = l.rotate 1

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.next l ⋯).length) (h₂ : i < (l.rotate 1).length), (pmap l.next l ⋯)[i] = (l.rotate 1)[i]

Tactic:
intros

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
i✝ : ℕ
h₁✝ : i✝ < (pmap l.next l ⋯).length
h₂✝ : i✝ < (l.rotate 1).length
⊢ (pmap l.next l ⋯)[i✝] = (l.rotate 1)[i✝]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ pmap l.next l ⋯ = l.rotate 1

Tactic:
apply List.ext_getElem

Result:
case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.next l ⋯).length = (l.rotate 1).length

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ ∀ (i : ℕ) (h₁ : i < (pmap l.next l ⋯).length) (h₂ : i < (l.rotate 1).length), (pmap l.next l ⋯)[i] = (l.rotate 1)[i]

Proof state:
case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.next l ⋯).length = (l.rotate 1).length

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
i✝ : ℕ
h₁✝ : i✝ < (pmap l.next l ⋯).length
h₂✝ : i✝ < (l.rotate 1).length
⊢ (pmap l.next l ⋯)[i✝] = (l.rotate 1)[i✝]

Tactic:
rw [getElem_pmap, getElem_rotate, next_getElem _ h]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
lemma filter_attach' (s : Multiset α) (p : {a // a ∈ s} → Prop) [DecidableEq α]
    [DecidablePred p] :
    s.attach.filter p =
      (s.filter fun x ↦ ∃ h, p ⟨x, h⟩).attach.map (Subtype.map id fun _ ↦ mem_of_mem_filter)

Proof state:
α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ filter p s.attach = map (Subtype.map id ⋯) (filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach

Tactic:
classical
refine Multiset.map_injective Subtype.val_injective ?_
rw [map_filter' _ Subtype.val_injective]
simp only [Function.comp, Subtype.exists, coe_mk, Subtype.map,
  exists_and_right, exists_eq_right, attach_map_val, map_map, map_coe, id]

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ map val (filter p s.attach) = map val (map (Subtype.map id ⋯) (filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach)

Tactic:
rw [map_filter' _ Subtype.val_injective]

Result:
α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ filter (fun b => ∃ a, p a ∧ ↑a = b) (map val s.attach) =
    map val (map (Subtype.map id ⋯) (filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach)

Proof state:
α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ filter (fun b => ∃ a, p a ∧ ↑a = b) (map val s.attach) =
    map val (map (Subtype.map id ⋯) (filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach)

Tactic:
simp only [Function.comp, Subtype.exists, coe_mk, Subtype.map,
  exists_and_right, exists_eq_right, attach_map_val, map_map, map_coe, id]

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ filter p s.attach = map (Subtype.map id ⋯) (filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach

Tactic:
refine Multiset.map_injective Subtype.val_injective ?_

Result:
α : Type u_1
s : Multiset α
p : { a // a ∈ s } → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
⊢ map val (filter p s.attach) = map val (map (Subtype.map id ⋯) (filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach)
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem List.norm_prod_le' : ∀ {l : List α}, l ≠ [] → ‖l.prod‖ ≤ (l.map norm).prod
  | [], h => (h rfl).elim
  | [a], _ => by simp
  | a::b::l, _ => by
    rw [List.map_cons, List.prod_cons, List.prod_cons (a := ‖a‖)]
    refine le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))
    exact List.norm_prod_le' (List.cons_ne_nil b l)

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod

Tactic:
refine le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))

Result:
α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a : α
x✝ : [a] ≠ []
⊢ ‖[a].prod‖ ≤ (map norm [a]).prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖(a :: b :: l).prod‖ ≤ (map norm (a :: b :: l)).prod

Tactic:
rw [List.map_cons, List.prod_cons, List.prod_cons (a := ‖a‖)]

Result:
α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * (b :: l).prod‖ ≤ ‖a‖ * (map norm (b :: l)).prod

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod

Tactic:
exact List.norm_prod_le' (List.cons_ne_nil b l)

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_and_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
    (∃ᶠ x in f, p ∧ q x) ↔ p ∧ ∃ᶠ x in f, q x

Proof state:
α : Type u
f : Filter α
p : Prop
q : α → Prop
⊢ (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x

Tactic:
simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem val_eq_iff_norm_eq {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0) :
    f.valuation = g.valuation ↔ f.norm = g.norm

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ f.valuation = g.valuation ↔ f.norm = g.norm

Tactic:
rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀]

Result:
case ha₀
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ 0 < ↑p

case ha₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ↑p ≠ 1

Proof state:
case ha₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ↑p ≠ 1

Tactic:
exact mod_cast (Fact.out : p.Prime).ne_one

Result:
no goals

Proof state:
case ha₀
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ 0 < ↑p

Tactic:
exact mod_cast (Fact.out : p.Prime).pos

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem opNorm_add_le (f g : ContinuousMultilinearMap 𝕜 E G) : ‖f + g‖ ≤ ‖f‖ + ‖g‖ :=
  opNorm_le_bound (add_nonneg (opNorm_nonneg f) (opNorm_nonneg g)) fun x => by
    rw [add_mul]
    exact norm_add_le_of_le (le_opNorm _ _) (le_opNorm _ _)

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f g : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖(f + g) x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖ + ‖g‖ * ∏ i : ι, ‖x i‖

Tactic:
exact norm_add_le_of_le (le_opNorm _ _) (le_opNorm _ _)

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f g : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖(f + g) x‖ ≤ (‖f‖ + ‖g‖) * ∏ i : ι, ‖x i‖

Tactic:
rw [add_mul]

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f g : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖(f + g) x‖ ≤ ‖f‖ * ∏ i : ι, ‖x i‖ + ‖g‖ * ∏ i : ι, ‖x i‖
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean
theorem go_eq_carry (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig) (origCin : Ref aig)
    (lhs rhs : RefVec aig w) (lhsExpr rhsExpr : BitVec w) (assign : α → Bool)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsbD idx)
    (hcin : ⟦aig, cin, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦aig, origCin, assign⟧) :
    ⟦go aig lhs rhs curr cin, assign⟧
      =
    BitVec.carry w lhsExpr rhsExpr ⟦aig, origCin, assign⟧

Proof state:
case isTrue.hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin origCin : aig.Ref
lhs rhs : aig.RefVec w
lhsExpr rhsExpr : BitVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := lhs.get idx hidx }⟧ = lhsExpr.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := rhs.get idx hidx }⟧ = rhsExpr.getLsbD idx
hcin : ⟦assign, { aig := aig, ref := cin }⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦assign, { aig := aig, ref := origCin }⟧
h✝ : curr < w
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := aig, ref := { gate := ((lhs.cast ⋯).get idx✝ hidx✝).gate, hgate := ?isTrue.hleft } }⟧ =
    lhsExpr.getLsbD idx✝

Tactic:
simp [hleft]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem rootMultiplicity_le_one_of_separable [Nontrivial R] {p : R[X]} (hsep : Separable p)
    (x : R) : rootMultiplicity x p ≤ 1

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ emultiplicity (X - C x) p ≤ 1

Tactic:
apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1

Tactic:
simp [hp]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1

Tactic:
rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
  Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]

Result:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ emultiplicity (X - C x) p ≤ 1

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : p = 0
⊢ rootMultiplicity x p ≤ 1

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1
-- Mathlib/RingTheory/DedekindDomain/PID.lean
theorem IsPrincipalIdealRing.of_finite_primes [IsDedekindDomain R]
    (h : {I : Ideal R | I.IsPrime}.Finite) : IsPrincipalIdealRing R :=
  ⟨fun I => by
    obtain rfl | hI := eq_or_ne I ⊥
    · exact bot_isPrincipal
    apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit
    · apply h.subset; exact @Ideal.IsMaximal.isPrime _ _
    · exact isUnit_of_mul_eq_one _ _ (FractionalIdeal.coe_ideal_mul_inv I hI)⟩

Proof state:
case inr.hI
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit ↑I

Tactic:
exact isUnit_of_mul_eq_one _ _ (FractionalIdeal.coe_ideal_mul_inv I hI)

Result:
no goals

Proof state:
case inr.hf
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ {I | I.IsMaximal}.Finite

Tactic:
apply h.subset

Result:
case inr.hf
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ {I | I.IsMaximal} ⊆ {I | I.IsPrime}

Proof state:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
⊢ Submodule.IsPrincipal ⊥

Tactic:
exact bot_isPrincipal

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
⊢ Submodule.IsPrincipal I

Tactic:
obtain rfl | hI := eq_or_ne I ⊥

Result:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
⊢ Submodule.IsPrincipal ⊥

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ Submodule.IsPrincipal I

Proof state:
case inr.hf
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ {I | I.IsMaximal} ⊆ {I | I.IsPrime}

Tactic:
exact @Ideal.IsMaximal.isPrime _ _

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ Submodule.IsPrincipal I

Tactic:
apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit

Result:
case inr.hf
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ {I | I.IsMaximal}.Finite

case inr.hI
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
h : {I | I.IsPrime}.Finite
I : Ideal R
hI : I ≠ ⊥
⊢ IsUnit ↑I
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem vadd_mem_fundamentalDomain [Fintype ι] (y : span ℤ (Set.range b)) (x : E) :
    y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : ↥(span ℤ (Set.range ⇑b))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x

Tactic:
rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
  ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
  fract_eq_self]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Icc_pi {a b : ι → ℝ} : volume (Icc a b) = ∏ i, ENNReal.ofReal (b i - a i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i : ι, volume (Icc (a i) (b i)) = ∏ i : ι, ofReal (b i - a i)

Tactic:
simp only [Real.volume_Icc]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ volume (Icc a b) = ∏ i : ι, ofReal (b i - a i)

Tactic:
rw [← pi_univ_Icc, volume_pi_pi]

Result:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
⊢ ∏ i : ι, volume (Icc (a i) (b i)) = ∏ i : ι, ofReal (b i - a i)
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem parallelepiped_comp_equiv (v : ι → E) (e : ι' ≃ ι) :
    parallelepiped (v ∘ e) = parallelepiped v

Proof state:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
⊢ Icc 0 1 = ⇑K '' Icc 0 1

Tactic:
rw [← Equiv.preimage_eq_iff_eq_image]

Result:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
⊢ ⇑K ⁻¹' Icc 0 1 = Icc 0 1

Proof state:
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝³ : Fintype ι
inst✝² : Fintype ι'
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
this✝ : Icc 0 1 = ⇑K '' Icc 0 1
x : E
this : ∀ (z : ι' → ℝ), ∑ x : ι, z (e.symm x) • v x = ∑ i : ι', z i • v (e i)
⊢ x ∈ (fun t => ∑ i : ι', t i • (v ∘ ⇑e) i) '' Icc 0 1 ↔ x ∈ (fun t => ∑ i : ι, t i • v i) ∘ ⇑K '' Icc 0 1

Tactic:
simp_rw [Function.comp_apply, mem_image, mem_Icc, K, Equiv.piCongrLeft'_apply, this]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
protected lemma div_ne_zero : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ⊤

Proof state:
a b : ℝ≥0∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ⊤

Tactic:
rw [← pos_iff_ne_zero, div_pos_iff]

Result:
no goals