harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Function.lean
lemma SurjOn.of_comp (h : SurjOn (g ∘ f) s p) (hr : MapsTo f s t) : SurjOn g t p

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
x : α
hx : x ∈ s
hz : (g ∘ f) x ∈ p
⊢ (g ∘ f) x ∈ g '' t

Tactic:
exact ⟨f x, hr hx, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
⊢ SurjOn g t p

Tactic:
intro z hz

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
z : γ
hz : z ∈ p
⊢ z ∈ g '' t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
z : γ
hz : z ∈ p
⊢ z ∈ g '' t

Tactic:
obtain ⟨x, hx, rfl⟩ := h hz

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
x : α
hx : x ∈ s
hz : (g ∘ f) x ∈ p
⊢ (g ∘ f) x ∈ g '' t
-- Mathlib/GroupTheory/Torsion.lean
theorem IsTorsion.module_of_torsion [Semiring R] [Module R M] (tR : IsTorsion R) : IsTorsion M :=
  fun f =>
  isOfFinAddOrder_iff_nsmul_eq_zero.mpr <| by
    obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero
    exact ⟨n, npos, by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]⟩

Proof state:
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
⊢ ∃ n, 0 < n ∧ n • f = 0

Tactic:
obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero

Result:
case intro.intro
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0

Proof state:
case intro.intro
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ ∃ n, 0 < n ∧ n • f = 0

Tactic:
exact ⟨n, npos, by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]⟩

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
tR : IsTorsion R
f : M
n : ℕ
npos : 0 < n
hn : n • 1 = 0
⊢ n • f = 0

Tactic:
simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]

Result:
no goals
-- Mathlib/Analysis/Analytic/Order.lean
/-- Helper lemma for `AnalyticAt.order_mul` -/
lemma order_mul_of_order_eq_top {f g : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀)
    (hg : AnalyticAt 𝕜 g z₀) (h'f : hf.order = ⊤) :
    (hf.mul hg).order = ⊤

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h'f : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f * g) y = 0) ∧ IsOpen t ∧ z₀ ∈ t

Tactic:
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h'f

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = 0
h₂t : IsOpen t
h₃t : z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f * g) y = 0) ∧ IsOpen t ∧ z₀ ∈ t

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = 0
h₂t : IsOpen t
h₃t : z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f * g) y = 0) ∧ IsOpen t ∧ z₀ ∈ t

Tactic:
exact ⟨t, fun y hy ↦ (by simp [h₁t y hy]), h₂t, h₃t⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
t : Set 𝕜
h₁t : ∀ y ∈ t, f y = 0
h₂t : IsOpen t
h₃t : z₀ ∈ t
y : 𝕜
hy : y ∈ t
⊢ (f * g) y = 0

Tactic:
simp [h₁t y hy]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h'f : hf.order = ⊤
⊢ ⋯.order = ⊤

Tactic:
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at *

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
z₀ : 𝕜
f g : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
h'f : ∃ t, (∀ y ∈ t, f y = 0) ∧ IsOpen t ∧ z₀ ∈ t
⊢ ∃ t, (∀ y ∈ t, (f * g) y = 0) ∧ IsOpen t ∧ z₀ ∈ t
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iInf_iff {f : ι → UpperSet α} : (a ∈ ⨅ i, f i) ↔ ∃ i, a ∈ f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⨅ i, f i ↔ ∃ i, a ∈ f i

Tactic:
rw [← SetLike.mem_coe, coe_iInf]

Result:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i

Tactic:
exact mem_iUnion

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_neg_left (xs ys : IntList) : (-xs).dot ys = -(xs.dot ys)

Proof state:
xs ys : IntList
⊢ (-xs).dot ys = -xs.dot ys

Tactic:
simp [dot, mul_neg_left]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atBot ↔ r < 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atBot ↔ r < 0

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_sub_one' (hx : 0 ≤ x) (h : y - 1 ≠ 0) : x ^ (y - 1) = x ^ y / x

Proof state:
x y : ℝ
hx : 0 ≤ x
h : y - 1 ≠ 0
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
rw [rpow_sub' hx h, rpow_one]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem IsFiltered.of_exists_of_isFiltered_of_fullyFaithful [IsFiltered D] [F.Full] [F.Faithful]
    (h : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) : IsFiltered C :=
  { IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h with
    nonempty

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : Nonempty D
⊢ Nonempty C

Tactic:
obtain ⟨c, -⟩ := h (Classical.arbitrary D)

Result:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : Nonempty D
c : C
⊢ Nonempty C

Proof state:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
exact ⟨c⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
⊢ Nonempty C

Tactic:
have : Nonempty D := IsFiltered.nonempty

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFiltered D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
this : Nonempty D
⊢ Nonempty C
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setIntegral_condKernel {s : Set β} (hs : MeasurableSet s)
    {t : Set Ω} (ht : MeasurableSet t) (hf : IntegrableOn f (s ×ˢ t) ρ) :
    ∫ b in s, ∫ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x in s ×ˢ t, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [setIntegral_compProd hs ht hf]

Result:
no goals

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [← ρ.disintegrate ρ.condKernel] at hf

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)
⊢ ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_biInf_principal {s : β → Set α} {S : Set β} (h : DirectedOn (s ⁻¹'o (· ≥ ·)) S)
    (ne : S.Nonempty) : (⨅ i ∈ S, 𝓟 (s i)).HasBasis (fun i => i ∈ S) s :=
  ⟨fun t => by
    refine mem_biInf_of_directed ?_ ne
    rw [directedOn_iff_directed, ← directed_comp] at h ⊢
    refine h.mono_comp _ ?_
    exact fun _ _ => principal_mono.2⟩

Proof state:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 => x1 ≥ x2) S
ne : S.Nonempty
t : Set α
⊢ DirectedOn ((fun i => 𝓟 (s i)) ⁻¹'o fun x1 x2 => x1 ≥ x2) S

Tactic:
rw [directedOn_iff_directed, ← directed_comp] at h ⊢

Result:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 => x1 ≥ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ Directed (fun x1 x2 => x1 ≥ x2) ((fun i => 𝓟 (s i)) ∘ Subtype.val)

Proof state:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 => x1 ≥ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ Directed (fun x1 x2 => x1 ≥ x2) ((fun i => 𝓟 (s i)) ∘ Subtype.val)

Tactic:
refine h.mono_comp _ ?_

Result:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 => x1 ≥ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y

Proof state:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 => x1 ≥ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ≥ y → 𝓟 x ≥ 𝓟 y

Tactic:
exact fun _ _ => principal_mono.2

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 => x1 ≥ x2) S
ne : S.Nonempty
t : Set α
⊢ t ∈ ⨅ i ∈ S, 𝓟 (s i) ↔ ∃ i ∈ S, s i ⊆ t

Tactic:
refine mem_biInf_of_directed ?_ ne

Result:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 => x1 ≥ x2) S
ne : S.Nonempty
t : Set α
⊢ DirectedOn ((fun i => 𝓟 (s i)) ⁻¹'o fun x1 x2 => x1 ≥ x2) S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lex_eq_true_iff_exists [BEq α] (lt : α → α → Bool) {l₁ l₂ : Vector α n} :
    lex l₁ l₂ lt = true ↔
      (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] == l₂[j]) ∧ lt l₁[i] l₂[i])

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : Vector α n
⊢ l₁.lex l₂ lt = true ↔ ∃ i h, (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true

Tactic:
rcases l₁ with ⟨l₁, n₁⟩

Result:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₂ : Vector α n
l₁ : Array α
n₁ : l₁.size = n
⊢ { toArray := l₁, size_toArray := n₁ }.lex l₂ lt = true ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i), ({ toArray := l₁, size_toArray := n₁ }[j] == l₂[j]) = true) ∧
        lt { toArray := l₁, size_toArray := n₁ }[i] l₂[i] = true

Proof state:
case mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ : Array α
n₁ : l₁.size = n
l₂ : Array α
n₂ : l₂.size = n
⊢ { toArray := l₁, size_toArray := n₁ }.lex { toArray := l₂, size_toArray := n₂ } lt = true ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i),
          ({ toArray := l₁, size_toArray := n₁ }[j] == { toArray := l₂, size_toArray := n₂ }[j]) = true) ∧
        lt { toArray := l₁, size_toArray := n₁ }[i] { toArray := l₂, size_toArray := n₂ }[i] = true

Tactic:
simp [Array.lex_eq_true_iff_exists, n₁, n₂]

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₂ : Vector α n
l₁ : Array α
n₁ : l₁.size = n
⊢ { toArray := l₁, size_toArray := n₁ }.lex l₂ lt = true ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i), ({ toArray := l₁, size_toArray := n₁ }[j] == l₂[j]) = true) ∧
        lt { toArray := l₁, size_toArray := n₁ }[i] l₂[i] = true

Tactic:
rcases l₂ with ⟨l₂, n₂⟩

Result:
case mk.mk
α : Type u_1
n : Nat
inst✝ : BEq α
lt : α → α → Bool
l₁ : Array α
n₁ : l₁.size = n
l₂ : Array α
n₂ : l₂.size = n
⊢ { toArray := l₁, size_toArray := n₁ }.lex { toArray := l₂, size_toArray := n₂ } lt = true ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i),
          ({ toArray := l₁, size_toArray := n₁ }[j] == { toArray := l₂, size_toArray := n₂ }[j]) = true) ∧
        lt { toArray := l₁, size_toArray := n₁ }[i] { toArray := l₂, size_toArray := n₂ }[i] = true
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma dual_mul_self (hI : I ≠ 0) :
    dual A K I * I = dual A K 1

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ dual A K I * I = dual A K 1

Tactic:
rw [dual_eq_mul_inv, mul_assoc, inv_mul_cancel₀ hI, mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_finset_biUnion {ι : Type*} (t : Finset ι) {s : ι → Set X}
    (hs : ∀ i ∈ t, MeasurableSet (s i)) (h's : Set.Pairwise (↑t) (Disjoint on s))
    (hf : ∀ i ∈ t, IntegrableOn f (s i) μ) :
    ∫ x in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ x in s i, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ Disjoint (s a) (⋃ i ∈ t, s i)

Tactic:
simp only [disjoint_iUnion_right]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ ∀ i ∈ t, Disjoint (s a) (s i)

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
s : ι → Set X
a : ι
t : Finset ι
hat : a ∉ t
IH :
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Disjoint on s) →
      (∀ i ∈ t, IntegrableOn f (s i) μ) → ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
hs : MeasurableSet (s a) ∧ ∀ x ∈ t, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ t, IntegrableOn f (s x) μ
h's : (↑t).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑t, a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ MeasurableSet (⋃ i ∈ t, s i)

Tactic:
exact Finset.measurableSet_biUnion _ hs.2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.iff_not_comm [Decidable a] [Decidable b] : (a ↔ ¬b) ↔ (b ↔ ¬a)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → ¬b) ∧ (¬b → a) ↔ (b → ¬a) ∧ (¬a → b)

Tactic:
exact and_congr imp_not_comm not_imp_comm

Result:
no goals

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a ↔ ¬b) ↔ (b ↔ ¬a)

Tactic:
rw [@iff_def a, @iff_def b]

Result:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → ¬b) ∧ (¬b → a) ↔ (b → ¬a) ∧ (¬a → b)
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_le_one_div (h1 : 0 < a) (h2 : a ≤ 1) : 1 ≤ 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h1 : 0 < a
h2 : a ≤ 1
⊢ 1 ≤ 1 / a

Tactic:
rwa [le_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_le_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b ≤ c + d) = (a ≤ c + (d - b))

Proof state:
a c b d : Nat
h : b ≤ d
⊢ (a + b ≤ c + d) = (a ≤ c + (d - b))

Tactic:
rw [← Nat.add_sub_assoc h, Nat.le_sub_iff_add_le]

Result:
a c b d : Nat
h : b ≤ d
⊢ b ≤ c + d

Proof state:
a c b d : Nat
h : b ≤ d
⊢ b ≤ c + d

Tactic:
exact Nat.le_trans h (le_add_left d c)

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem interpolate_eq_of_values_eq_on (hrr' : ∀ i ∈ s, r i = r' i) :
    interpolate s v r = interpolate s v r' :=
  sum_congr rfl fun i hi => by rw [hrr' _ hi]

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r r' : ι → F
hrr' : ∀ i ∈ s, r i = r' i
i : ι
hi : i ∈ s
⊢ C (r i) * Lagrange.basis s v i = C (r' i) * Lagrange.basis s v i

Tactic:
rw [hrr' _ hi]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem modEq_iff_dvd' (h : a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a

Proof state:
n a b : ℕ
h : a ≤ b
⊢ a ≡ b [MOD n] ↔ n ∣ b - a

Tactic:
rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_mul (a b : α) : |a * b| = |a| * |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a * b| = |a| * |b|

Tactic:
rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]

Result:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)

Tactic:
rcases le_total a 0 with ha | ha <;> rcases le_total b 0 with hb | hb <;>
  simp only [abs_of_nonpos, abs_of_nonneg, true_or, or_true, eq_self_iff_true, neg_mul,
    mul_neg, neg_neg, *]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem zero_cpow {x : ℂ} (h : x ≠ 0) : (0 : ℂ) ^ x = 0

Proof state:
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0

Tactic:
simp [cpow_def, *]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem outerMeasure_pos_of_is_mul_left_invariant [Group G] [IsTopologicalGroup G]
    (h3 : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (K : Compacts G)
    (hK : μ K ≠ 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) : 0 < μ.outerMeasure U

Proof state:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Set G
h1U : IsOpen U
h2U : U.Nonempty
⊢ 0 < μ.outerMeasure U

Tactic:
convert μ.innerContent_pos_of_is_mul_left_invariant h3 K hK ⟨U, h1U⟩ h2U

Result:
case h.e'_4
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Set G
h1U : IsOpen U
h2U : U.Nonempty
⊢ μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := h1U }

Proof state:
case h.e'_4
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Set G
h1U : IsOpen U
h2U : U.Nonempty
⊢ μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := h1U }

Tactic:
exact μ.outerMeasure_opens ⟨U, h1U⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
    DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝[s] x
⊢ DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter' ht]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem zero : padicNorm p 0 = 0

Proof state:
p : ℕ
⊢ padicNorm p 0 = 0

Tactic:
simp [padicNorm]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem supDegree_sub_le {f g : R'[A]} :
    (f - g).supDegree D ≤ f.supDegree D ⊔ g.supDegree D

Proof state:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)

Tactic:
apply supDegree_add_le

Result:
no goals

Proof state:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g

Tactic:
rw [sub_eq_add_neg, ← supDegree_neg (f := g)]

Result:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_one' : a / b < 1 ↔ a < b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a / b < 1 ↔ a < b

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem one_mem_nthRootsFinset (hn : 0 < n) : 1 ∈ nthRootsFinset n R

Proof state:
R : Type u
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : 0 < n
⊢ 1 ∈ nthRootsFinset n R

Tactic:
rw [mem_nthRootsFinset hn, one_pow]

Result:
no goals