harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Side.lean
theorem sSameSide_smul_vsub_vadd_left {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s)
    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R} (ht : 0 < t) : s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
⊢ s.SSameSide (t • (x -ᵥ p₁) +ᵥ p₂) x

Tactic:
refine ⟨wSameSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
⊢ x ∈ s

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p₁ p₂ : P
hx : x ∉ s
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
t : R
ht : 0 < t
h : t • (x -ᵥ p₁) +ᵥ p₂ ∈ s
⊢ x ∈ s

Tactic:
rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne.symm,
  vsub_right_mem_direction_iff_mem hp₁] at h

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_insert_congr_right (h : M.closure X = M.closure Y) :
    M.closure (insert e X) = M.closure (insert e Y)

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
e : α
h : M.closure X = M.closure Y
⊢ M.closure (insert e X) = M.closure (insert e Y)

Tactic:
simp [← union_singleton, closure_union_congr_left h]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem tendsto_nhds_top_iff_real {α : Type*} {m : α → EReal} {f : Filter α} :
    Tendsto m f (𝓝 ⊤) ↔ ∀ x : ℝ, ∀ᶠ a in f, ↑x < m a :=
  nhds_top_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Ioi]

Proof state:
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Ioi ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, ↑x < m a

Tactic:
simp only [true_implies, mem_Ioi]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem mem_factors'_iff_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    Subtype.mk (Associates.mk p) (irreducible_mk.2 hp) ∈ factors' a ↔ p ∣ a

Proof state:
case mp.hz
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ a ≠ 0

Tactic:
apply ha0

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → ⟨Associates.mk p, ⋯⟩ ∈ factors' a

Tactic:
apply mem_factors'_of_dvd ha0 hp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a ↔ p ∣ a

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → p ∣ a

case mpr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ p ∣ a → ⟨Associates.mk p, ⋯⟩ ∈ factors' a

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → p ∣ a

Tactic:
rw [← mk_dvd_mk]

Result:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → Associates.mk p ∣ Associates.mk a

Proof state:
case mp
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ ⟨Associates.mk p, ⋯⟩ ∈ factors' a → Associates.mk p ∣ Associates.mk a

Tactic:
apply dvd_of_mem_factors'

Result:
case mp.hz
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
⊢ a ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem get!_val [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α} [Inhabited (β a)] :
    m.val.get! a = m.get! a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
m : Raw₀ α β
a : α
inst✝ : Inhabited (β a)
⊢ m.val.get! a = m.get! a

Tactic:
simp [Raw.get!, m.2]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsClique.finsetMap {f : α ↪ β} {s : Finset α} (h : G.IsClique s) :
    (G.map f).IsClique (s.map f)

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
s : Finset α
h : G.IsClique ↑s
⊢ (SimpleGraph.map f G).IsClique ↑(map f s)

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Simple.lean
theorem Biprod.isIso_inl_iff_isZero (X Y : C) : IsIso (biprod.inl : X ⟶ X ⊞ Y) ↔ IsZero Y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y

Tactic:
constructor

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : (biprod.snd ≫ biprod.inr) ≫ biprod.snd = 0 ≫ biprod.snd
⊢ IsZero Y

Tactic:
simpa [← IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsIso biprod.inl ↔ IsZero Y

Tactic:
rw [biprod.isIso_inl_iff_id_eq_fst_comp_inl, ← biprod.total, add_right_eq_self]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y

Tactic:
intro h

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd ≫ biprod.inr = 0
⊢ IsZero Y

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : IsZero Y
⊢ biprod.snd ≫ biprod.inr = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : IsZero Y
⊢ biprod.snd ≫ biprod.inr = 0

Tactic:
rw [IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] at h

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ biprod.snd ≫ biprod.inr = 0

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ biprod.snd ≫ biprod.inr = 0

Tactic:
rw [h, zero_comp]

Result:
no goals

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd ≫ biprod.inr = 0
⊢ IsZero Y

Tactic:
replace h := h =≫ biprod.snd

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : (biprod.snd ≫ biprod.inr) ≫ biprod.snd = 0 ≫ biprod.snd
⊢ IsZero Y
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_coe_nat (n : ℕ) : Real.toNNReal n = n :=
  NNReal.eq <| by simp [Real.coe_toNNReal]

Proof state:
n : ℕ
⊢ ↑(↑n).toNNReal = ↑↑n

Tactic:
simp [Real.coe_toNNReal]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem smul_ofFunction {c : ℝ≥0∞} (hc : c ≠ ∞) : c • OuterMeasure.ofFunction m m_empty =
    OuterMeasure.ofFunction (c • m) (by simp [m_empty])

Proof state:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ (c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s

Tactic:
haveI : Nonempty { t : ℕ → Set α // s ⊆ ⋃ i, t i } := ⟨⟨fun _ => s, subset_iUnion (fun _ => s) 0⟩⟩

Result:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ (c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ (c • m) ∅ = 0

Tactic:
simp [m_empty]

Result:
no goals

Proof state:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ (c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s

Tactic:
simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul,
iInf_subtype']

Result:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ c * ⨅ x, ∑' (n : ℕ), m (↑x n) = ⨅ x, c * ∑' (i : ℕ), m (↑x i)

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c • OuterMeasure.ofFunction m m_empty = OuterMeasure.ofFunction (c • m) ⋯

Tactic:
ext1 s

Result:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
⊢ (c • OuterMeasure.ofFunction m m_empty) s = (OuterMeasure.ofFunction (c • m) ⋯) s

Proof state:
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ⊤
s : Set α
this : Nonempty { t // s ⊆ ⋃ i, t i }
⊢ c * ⨅ x, ∑' (n : ℕ), m (↑x n) = ⨅ x, c * ∑' (i : ℕ), m (↑x i)

Tactic:
rw [ENNReal.mul_iInf fun h => (hc h).elim]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.exists_nat_integrableOn [SecondCountableTopology X]
    (hf : LocallyIntegrable f μ) : ∃ u : ℕ → Set X,
    (∀ n, IsOpen (u n)) ∧ ((⋃ n, u n) = univ) ∧ (∀ n, IntegrableOn f (u n) μ)

Proof state:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ ∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
rcases (hf.locallyIntegrableOn univ).exists_nat_integrableOn with ⟨u, u_open, u_union, hu⟩

Result:
case intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
⊢ ∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Proof state:
case intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
⊢ ∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
refine ⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ ?_⟩

Result:
case intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
n : ℕ
⊢ IntegrableOn f (u n) μ

Proof state:
case intro.intro.intro
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
u : ℕ → Set X
u_open : ∀ (n : ℕ), IsOpen (u n)
u_union : univ ⊆ ⋃ n, u n
hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ
n : ℕ
⊢ IntegrableOn f (u n) μ

Tactic:
simpa only [inter_univ] using hu n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pred_inj :
    ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
  | ⟨0, _⟩, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
  | ⟨i + 1, _⟩, ⟨0, _⟩, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [Fin.ext_iff, Nat.succ.injEq]

Proof state:
n i : Nat
isLt✝¹ : i + 1 < n + 1
isLt✝ : 0 < n + 1
x✝ : ⟨i + 1, isLt✝¹⟩ ≠ 0
hb : ⟨0, isLt✝⟩ ≠ 0
⊢ ⟨i + 1, isLt✝¹⟩.pred x✝ = ⟨0, isLt✝⟩.pred hb ↔ ⟨i + 1, isLt✝¹⟩ = ⟨0, isLt✝⟩

Tactic:
simp only [mk_zero, ne_eq, not_true] at hb

Result:
no goals

Proof state:
n : Nat
isLt✝ : 0 < n + 1
x✝¹ : Fin (n + 1)
ha : ⟨0, isLt✝⟩ ≠ 0
x✝ : x✝¹ ≠ 0
⊢ ⟨0, isLt✝⟩.pred ha = x✝¹.pred x✝ ↔ ⟨0, isLt✝⟩ = x✝¹

Tactic:
simp only [mk_zero, ne_eq, not_true] at ha

Result:
no goals

Proof state:
n i : Nat
hi : i + 1 < n + 1
j : Nat
hj : j + 1 < n + 1
ha : ⟨i + 1, hi⟩ ≠ 0
hb : ⟨j + 1, hj⟩ ≠ 0
⊢ ⟨i + 1, hi⟩.pred ha = ⟨j + 1, hj⟩.pred hb ↔ ⟨i + 1, hi⟩ = ⟨j + 1, hj⟩

Tactic:
simp [Fin.ext_iff, Nat.succ.injEq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_iff_right_iff_imp : ∀ {a b : Bool}, ((a && b) = b) ↔ (b → a)

Proof state:
⊢ ∀ {a b : Bool}, (a && b) = b ↔ b = true → a = true

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_ofList [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k : α} :
    (ofList l).contains k = (l.map Prod.fst).contains k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
⊢ (ofList l).contains k = (List.map Prod.fst l).contains k

Tactic:
simp_to_raw using Raw₀.Const.contains_insertMany_empty_list

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_empty_of_size_eq_zero (xs : Vector α n) (h : n = 0) : xs = #v[].cast h.symm

Proof state:
case mk
α : Type u_1
xs : Array α
h✝ : xs.size = 0
h : xs = #[]
⊢ { toArray := xs, size_toArray := ⋯ }.toArray = (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }).toArray

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
h : n = 0
⊢ xs = Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
xs : Array α
h : xs.size = 0
⊢ { toArray := xs, size_toArray := ⋯ } = Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
xs : Array α
h : xs.size = 0
⊢ { toArray := xs, size_toArray := ⋯ } = Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }

Tactic:
apply toArray_inj.1

Result:
case mk
α : Type u_1
xs : Array α
h : xs.size = 0
⊢ { toArray := xs, size_toArray := ⋯ }.toArray = (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }).toArray

Proof state:
case mk
α : Type u_1
xs : Array α
h : xs.size = 0
⊢ { toArray := xs, size_toArray := ⋯ }.toArray = (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }).toArray

Tactic:
simp only [List.length_eq_zero, Array.toList_eq_nil_iff] at h

Result:
case mk
α : Type u_1
xs : Array α
h✝ : xs.size = 0
h : xs = #[]
⊢ { toArray := xs, size_toArray := ⋯ }.toArray = (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }).toArray
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean
lemma univ_map_map :
    (univ R n).map (MvPolynomial.map f) = univ S n

Proof state:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
⊢ (of (Function.curry MvPolynomial.X)).charpoly = univ S n

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
⊢ Polynomial.map (MvPolynomial.map f) (univ R n) = univ S n

Tactic:
rw [MvPolynomial.map, univ_map_eval₂Hom]

Result:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
⊢ (of (Function.curry MvPolynomial.X)).charpoly = univ S n
-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem denseRange_zpow_iff_pow {x : G} :
    DenseRange (x ^ · : ℤ → G) ↔ DenseRange (x ^ · : ℕ → G)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ (DenseRange fun x_1 => x ^ x_1) ↔ DenseRange fun x_1 => x ^ x_1

Tactic:
simp only [DenseRange, dense_iff_closure_eq, closure_range_zpow_eq_pow]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_inj {a b : Ordinal} : lift.{u, v} a = lift.{u, v} b ↔ a = b

Proof state:
a b : Ordinal.{v}
⊢ lift.{u, v} a = lift.{u, v} b ↔ a = b

Tactic:
simp_rw [le_antisymm_iff, lift_le]

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_eq_intro {n m k l : ℕ} (h : n + m = k + l) : dist n k = dist l m :=
  calc
    dist n k = dist (n + m) (k + m)

Proof state:
n m k l : ℕ
h : n + m = k + l
⊢ n.dist k = (n + m).dist (k + m)

Tactic:
rw [dist_add_add_right]

Result:
no goals

Proof state:
n m k l : ℕ
h : n + m = k + l
⊢ (n + m).dist (k + m) = (k + l).dist (k + m)

Tactic:
rw [h]

Result:
no goals

Proof state:
n m k l : ℕ
h : n + m = k + l
⊢ (k + l).dist (k + m) = l.dist m

Tactic:
rw [dist_add_add_left]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem Infinitesimal.mul {x y : ℝ*} (hx : Infinitesimal x) (hy : Infinitesimal y) :
    Infinitesimal (x * y)

Proof state:
x y : ℝ*
hx : x.Infinitesimal
hy : y.Infinitesimal
⊢ (x * y).Infinitesimal

Tactic:
simpa only [mul_zero] using hx.mul hy

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem drop_add_one_eq_tail_drop (l : List α) : l.drop (i + 1) = (l.drop i).tail

Proof state:
α : Type u_1
i : Nat
l : List α
⊢ drop (i + 1) l = (drop i l).tail

Tactic:
rw [← drop_drop, drop_one]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toMeasureOfLEZero_apply (hi : s ≤[i] 0) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) :
    s.toMeasureOfLEZero i hi₁ hi j = ((↑) : ℝ≥0 → ℝ≥0∞) ⟨-s (i ∩ j), neg_apply s (i ∩ j) ▸
      nonneg_of_zero_le_restrict _ (zero_le_restrict_subset _ hi₁ Set.inter_subset_left
      (@neg_zero (VectorMeasure α ℝ) _ ▸ neg_le_neg _ _ hi₁ hi))⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑⟨↑(-s) (i ∩ j), ⋯⟩ = ↑⟨-↑s (i ∩ j), ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfLEZero i hi₁ hi) j = ↑⟨-↑s (i ∩ j), ⋯⟩

Tactic:
erw [toMeasureOfZeroLE_apply]

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ ↑⟨↑(-s) (i ∩ j), ⋯⟩ = ↑⟨-↑s (i ∩ j), ⋯⟩

case hj₁
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ MeasurableSet j

Proof state:
case hj₁
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ MeasurableSet j

Tactic:
assumption

Result:
no goals
-- Mathlib/Order/GaloisConnection/Defs.lean
theorem u_eq {z : α} {y : β} : u y = z ↔ ∀ x, x ≤ z ↔ l x ≤ y

Proof state:
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y

Tactic:
constructor

Result:
case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y

case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z

Proof state:
case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y

Tactic:
exact (gc x y).symm

Result:
no goals

Proof state:
case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ (∀ (x : α), x ≤ z ↔ l x ≤ y) → u y = z

Tactic:
intro H

Result:
case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z

Proof state:
case mpr
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
H : ∀ (x : α), x ≤ z ↔ l x ≤ y
⊢ u y = z

Tactic:
exact ((H <| u y).mpr (gc.l_u_le y)).antisymm ((gc _ _).mp <| (H z).mp le_rfl)

Result:
no goals

Proof state:
case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
z : α
y : β
⊢ u y = z → ∀ (x : α), x ≤ z ↔ l x ≤ y

Tactic:
rintro rfl x

Result:
case mp
α : Type u
β : Type v
inst✝¹ : PartialOrder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
y : β
x : α
⊢ x ≤ u y ↔ l x ≤ y
-- Mathlib/Analysis/Seminorm.lean
theorem smul_closedBall_preimage (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜) (ha : a ≠ 0) :
    (a • ·) ⁻¹' p.closedBall y r = p.closedBall (a⁻¹ • y) (r / ‖a‖) :=
  Set.ext fun _ => by
    rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ x✝ ∈ (fun x => a • x) ⁻¹' p.closedBall y r ↔ x✝ ∈ p.closedBall (a⁻¹ • y) (r / ‖a‖)

Tactic:
rw [mem_preimage, mem_closedBall, mem_closedBall, le_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
  map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem inf_ae_iff : μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : μ (t ∩ u) < ⊤
⊢ μ t ≤ μ (t ∩ u)

Tactic:
exact measure_mono_ae (mem_of_superset hu fun x hu ht => ⟨ht, hu⟩)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
⊢ μ.FiniteAtFilter (f ⊓ ae μ) → μ.FiniteAtFilter f

Tactic:
rintro ⟨s, ⟨t, ht, u, hu, rfl⟩, hμ⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : μ (t ∩ u) < ⊤
⊢ μ.FiniteAtFilter f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
⊢ μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f

Tactic:
refine ⟨?_, fun h => h.filter_mono inf_le_left⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
⊢ μ.FiniteAtFilter (f ⊓ ae μ) → μ.FiniteAtFilter f

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : μ (t ∩ u) < ⊤
⊢ μ.FiniteAtFilter f

Tactic:
suffices μ t ≤ μ (t ∩ u) from ⟨t, ht, this.trans_lt hμ⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : μ (t ∩ u) < ⊤
⊢ μ t ≤ μ (t ∩ u)