harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_subset_uIcc (x y : E) : [x -[𝕜] y] ⊆ uIcc x y

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ Icc x y

Tactic:
exact segment_subset_Icc h

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : y ≤ x
⊢ [y-[𝕜]x] ⊆ Icc y x

Tactic:
exact segment_subset_Icc h

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : y ≤ x
⊢ [x-[𝕜]y] ⊆ uIcc x y

Tactic:
rw [uIcc_of_ge h, segment_symm]

Result:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : y ≤ x
⊢ [y-[𝕜]x] ⊆ Icc y x

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ uIcc x y

Tactic:
rw [uIcc_of_le h]

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ Icc x y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
⊢ [x-[𝕜]y] ⊆ uIcc x y

Tactic:
rcases le_total x y with h | h

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : x ≤ y
⊢ [x-[𝕜]y] ⊆ uIcc x y

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : LinearOrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
x y : E
h : y ≤ x
⊢ [x-[𝕜]y] ⊆ uIcc x y
-- Mathlib/Order/Lattice.lean
theorem inf_eq_minDefault [SemilatticeInf α] [DecidableRel ((· ≤ ·) : α → α → Prop)]
    [IsTotal α (· ≤ ·)] :
    (· ⊓ ·) = (minDefault : α → α → α)

Proof state:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
⊢ (fun x1 x2 => x1 ⊓ x2) = minDefault

Tactic:
ext x y

Result:
case h.h
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊓ y = minDefault x y

Proof state:
case h.h
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊓ y = if x ≤ y then x else y

Tactic:
split_ifs with h'

Result:
case pos
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
h' : x ≤ y
⊢ x ⊓ y = x

case neg
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
h' : ¬x ≤ y
⊢ x ⊓ y = y

Proof state:
case h.h
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊓ y = minDefault x y

Tactic:
unfold minDefault

Result:
case h.h
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : IsTotal α fun x1 x2 => x1 ≤ x2
x y : α
⊢ x ⊓ y = if x ≤ y then x else y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forM_append [Monad m] [LawfulMonad m] (l₁ l₂ : Array α) (f : α → m PUnit) :
    forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₁ l₂ : Array α
f : α → m PUnit
⊢ forM (l₁ ++ l₂) f = do
    forM l₁ f
    forM l₂ f

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₂ : Array α
f : α → m PUnit
l₁ : List α
⊢ forM ({ toList := l₁ } ++ l₂) f = do
    forM { toList := l₁ } f
    forM l₂ f

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₂ : Array α
f : α → m PUnit
l₁ : List α
⊢ forM ({ toList := l₁ } ++ l₂) f = do
    forM { toList := l₁ } f
    forM l₂ f

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m PUnit
l₁ l₂ : List α
⊢ forM ({ toList := l₁ } ++ { toList := l₂ }) f = do
    forM { toList := l₁ } f
    forM { toList := l₂ } f

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m PUnit
l₁ l₂ : List α
⊢ forM ({ toList := l₁ } ++ { toList := l₂ }) f = do
    forM { toList := l₁ } f
    forM { toList := l₂ } f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem of_card_le_one (hA : A.Nonempty) (hB : B.Nonempty) (hA1 : #A ≤ 1) (hB1 : #B ≤ 1) :
    ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Proof state:
case intro.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
b : G
hb : b ∈ B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
exact ⟨a, ha, b, hb, fun _ _ ha' hb' _ ↦ ⟨hA1 ha' ha, hB1 hb' hb⟩⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨a, ha⟩ := hA

Result:
case intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : #A ≤ 1
hB1 : #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
rw [Finset.card_le_one_iff] at hA1 hB1

Result:
G : Type u_1
inst✝ : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Proof state:
case intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
hB : B.Nonempty
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
obtain ⟨b, hb⟩ := hB

Result:
case intro.intro
G : Type u_1
inst✝ : Mul G
A B : Finset G
hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b
hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b
a : G
ha : a ∈ A
b : G
hb : b ∈ B
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isCompact_isOpen_iff {s : Set (PrimeSpectrum R)} :
    IsCompact s ∧ IsOpen s ↔ ∃ t : Finset R, (zeroLocus t)ᶜ = s

Proof state:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ s, s.Finite ∧ s✝ = (zeroLocus s)ᶜ
s : Set R
hs : s.Finite
e : s✝ = (zeroLocus s)ᶜ
⊢ (zeroLocus ↑hs.toFinset)ᶜ = s✝

Tactic:
simpa using e.symm

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ s_1, s_1.Finite ∧ s = ⋃ i ∈ s_1, ↑(basicOpen i)) ↔ ∃ t, (zeroLocus ↑t)ᶜ = s

Tactic:
simp only [basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂, ← zeroLocus_iUnion₂,
  Set.biUnion_of_singleton]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ s_1, s_1.Finite ∧ s = (zeroLocus s_1)ᶜ) ↔ ∃ t, (zeroLocus ↑t)ᶜ = s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ s_1, s_1.Finite ∧ s = (zeroLocus s_1)ᶜ) ↔ ∃ t, (zeroLocus ↑t)ᶜ = s

Tactic:
exact ⟨fun ⟨s, hs, e⟩ ↦ ⟨hs.toFinset, by simpa using e.symm⟩,
  fun ⟨s, e⟩ ↦ ⟨s, s.finite_toSet, by simpa using e.symm⟩⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ t, (zeroLocus ↑t)ᶜ = s✝
s : Finset R
e : (zeroLocus ↑s)ᶜ = s✝
⊢ s✝ = (zeroLocus ↑s)ᶜ

Tactic:
simpa using e.symm

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ IsCompact s ∧ IsOpen s ↔ ∃ t, (zeroLocus ↑t)ᶜ = s

Tactic:
rw [isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _
  isTopologicalBasis_basic_opens isCompact_basicOpen]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (∃ s_1, s_1.Finite ∧ s = ⋃ i ∈ s_1, ↑(basicOpen i)) ↔ ∃ t, (zeroLocus ↑t)ᶜ = s
-- Mathlib/Order/RelSeries.lean
lemma smash_natAdd {p q : RelSeries r} (h : p.last = q.head) (i : Fin q.length) :
    smash p q h (Fin.castSucc <| i.natAdd p.length) = q (Fin.castSucc i)

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ ¬↑(Fin.natAdd p.length i).castSucc < p.length

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ ↑(Fin.natAdd p.length i).castSucc - p.length = ↑i

Tactic:
exact Nat.add_sub_self_left _ _

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ (p.smash q h).toFun (Fin.natAdd p.length i).castSucc = q.toFun i.castSucc

Tactic:
rw [smash_toFun, dif_neg (by simp)]

Result:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ q.toFun ⟨↑(Fin.natAdd p.length i).castSucc - p.length, ⋯⟩ = q.toFun i.castSucc

Proof state:
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ q.toFun ⟨↑(Fin.natAdd p.length i).castSucc - p.length, ⋯⟩ = q.toFun i.castSucc

Tactic:
congr

Result:
case e_a.e_val
α : Type u_1
r : Rel α α
p q : RelSeries r
h : p.last = q.head
i : Fin q.length
⊢ ↑(Fin.natAdd p.length i).castSucc - p.length = ↑i
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.ext_iff {u₁ u₂ : UniformSpace α} :
    u₁ = u₂ ↔ ∀ s, s ∈ 𝓤[u₁] ↔ s ∈ 𝓤[u₂] :=
  ⟨fun h _ => h ▸ Iff.rfl, fun h => by ext; exact h _⟩

Proof state:
α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
⊢ u₁ = u₂

Tactic:
ext

Result:
case h.h
α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
s✝ : Set (α × α)
⊢ s✝ ∈ 𝓤 α ↔ s✝ ∈ 𝓤 α

Proof state:
case h.h
α : Type ua
u₁ u₂ : UniformSpace α
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
s✝ : Set (α × α)
⊢ s✝ ∈ 𝓤 α ↔ s✝ ∈ 𝓤 α

Tactic:
exact h _

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem lim_conj (f : CauSeq ℂ (‖·‖)) : lim (cauSeqConj f) = conj (lim f) :=
  Complex.ext (by simp [cauSeqConj, (lim_re _).symm, cauSeqRe])
    (by simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]; rfl)

Proof state:
f : CauSeq ℂ fun x => ‖x‖
⊢ CauSeq.lim ⟨fun n => -(↑f n).im, ⋯⟩ = (-⟨fun n => (↑f n).im, ⋯⟩).lim

Tactic:
rfl

Result:
no goals

Proof state:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqConj f).lim.im = ((starRingEnd ℂ) f.lim).im

Tactic:
simp [cauSeqConj, (lim_im _).symm, cauSeqIm, (lim_neg _).symm]

Result:
f : CauSeq ℂ fun x => ‖x‖
⊢ CauSeq.lim ⟨fun n => -(↑f n).im, ⋯⟩ = (-⟨fun n => (↑f n).im, ⋯⟩).lim

Proof state:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqConj f).lim.re = ((starRingEnd ℂ) f.lim).re

Tactic:
simp [cauSeqConj, (lim_re _).symm, cauSeqRe]

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem HasLines.pointCount_le_lineCount [HasLines P L] {p : P} {l : L} (h : p ∉ l)
    [Finite { l : L // p ∈ l }] : pointCount P l ≤ lineCount L p

Proof state:
case pos
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
exact (le_of_eq Nat.card_eq_zero_of_infinite).trans (zero_le (lineCount L p))

Result:
no goals

Proof state:
case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
cases nonempty_fintype { l : L // p ∈ l }

Result:
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Proof state:
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
by_cases hf : Infinite { p : P // p ∈ l }

Result:
case pos
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Proof state:
case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
haveI := fintypeOfNotInfinite hf

Result:
case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Proof state:
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
rw [lineCount, pointCount, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]

Result:
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ Fintype.card { p // p ∈ l } ≤ Fintype.card { l // p ∈ l }
-- Mathlib/Analysis/Convolution.lean
theorem Integrable.convolution_integrand (hf : Integrable f ν) (hg : Integrable g μ) :
    Integrable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν)

Proof state:
case refine_2
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ ν : Measure G
inst✝⁵ : AddGroup G
inst✝⁴ : MeasurableAdd₂ G
inst✝³ : MeasurableNeg G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddRightInvariant
inst✝ : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν
t : G
⊢ ‖∫ (x : G), ‖(L (f t)) (g (x - t))‖ ∂μ‖ ≤ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ

Tactic:
simp_rw [← integral_mul_left]

Result:
case refine_2
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ ν : Measure G
inst✝⁵ : AddGroup G
inst✝⁴ : MeasurableAdd₂ G
inst✝³ : MeasurableNeg G
inst✝² : SFinite μ
inst✝¹ : μ.IsAddRightInvariant
inst✝ : SFinite ν
hf : Integrable f ν
hg : Integrable g μ
h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)
h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν
t : G
⊢ ‖∫ (x : G), ‖(L (f t)) (g (x - t))‖ ∂μ‖ ≤ ∫ (a : G), ‖L‖ * ‖f t‖ * ‖g (a - t)‖ ∂μ
-- Mathlib/RingTheory/Finiteness/Cardinality.lean
lemma _root_.Set.Finite.submoduleSpan [Finite R] {s : Set M} (hs : s.Finite) :
    (Submodule.span R s : Set M).Finite

Proof state:
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Set M
hs : s.Finite
⊢ (↑(span R s)).Finite

Tactic:
lift s to Finset M using hs

Result:
case intro
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ (↑(span R ↑s)).Finite

Proof state:
case intro
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↑↑(span R ↑s)

Tactic:
dsimp

Result:
case intro
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↥(span R ↑s)

Proof state:
case intro
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ (↑(span R ↑s)).Finite

Tactic:
rw [Set.Finite, ← Module.finite_iff_finite (R := R)]

Result:
case intro
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↑↑(span R ↑s)

Proof state:
case intro
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite R
s : Finset M
⊢ Module.Finite R ↥(span R ↑s)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem hom.congr_left {f g : Arrow T} {φ₁ φ₂ : f ⟶ g} (h : φ₁ = φ₂) : φ₁.left = φ₂.left

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ φ₁.left = φ₂.left

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_tan_oangle_add_left_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖x‖ / Real.Angle.tan (o.oangle (x + y) y) = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (x + y)).tan = ‖y‖

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (y + x)).tan = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (y + x)).tan = ‖y‖

Tactic:
exact (-o).norm_div_tan_oangle_add_right_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖x‖ / (o.oangle (x + y) y).tan = ‖y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (x + y)).tan = ‖y‖
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem absolutelyContinuous_map_mul_right (g : G) : μ ≪ map (· * g) μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ s = 0

Tactic:
exact id

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun x => x * g) μ

Tactic:
refine AbsolutelyContinuous.mk fun s hs => ?_

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ (map (fun x => x * g) μ) s = 0 → μ s = 0

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ (map (fun x => x * g) μ) s = 0 → μ s = 0

Tactic:
rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ s = 0
-- Mathlib/Algebra/Quandle.lean
lemma act_self_act_eq (x y : S) : x ◃ (x ◃ y) = x ◃ y

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = x ◃ y

Tactic:
have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw [act_one]

Result:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
⊢ x ◃ x ◃ y = x ◃ y

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
h : x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y
⊢ x ◃ x ◃ y = x ◃ y

Tactic:
rw [h, ← Shelf.self_distrib, one_act]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x y : S
⊢ x ◃ x ◃ y = (x ◃ 1) ◃ x ◃ y

Tactic:
rw [act_one]

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem isLUB_of_tendsto_atTop [TopologicalSpace α] [Preorder α] [OrderClosedTopology α]
    [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} (hf : Monotone f)
    (ha : Tendsto f atTop (𝓝 a)) : IsLUB (Set.range f) a

Proof state:
case right
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Tactic:
exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ IsLUB (range f) a

Tactic:
constructor

Result:
case left
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)

case right
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Proof state:
case left.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a

Tactic:
exact hf.ge_of_tendsto ha b

Result:
no goals

Proof state:
case left
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)

Tactic:
rintro _ ⟨b, rfl⟩

Result:
case left.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a
-- Mathlib/Topology/Instances/AddCircle.lean
theorem coe_image_Ico_eq : ((↑) : 𝕜 → AddCircle p) '' Ico a (a + p) = univ

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ QuotientAddGroup.mk '' Ico a (a + p) = univ

Tactic:
rw [image_eq_range]

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ (range fun x => ↑↑x) = univ

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ (range fun x => ↑↑x) = univ

Tactic:
exact (equivIco p a).symm.range_eq_univ

Result:
no goals