harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_map (p : R[X]) (f : R →+* S) :
    sumIDeriv (p.map f) = (sumIDeriv p).map f

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := (map f p).natDegree ⊔ p.natDegree
⊢ ∑ i ∈ range ((map f p).natDegree ⊔ p.natDegree + 1), (⇑derivative)^[i] (map f p) = map f (sumIDeriv p)

Tactic:
rw [sumIDeriv_apply_of_le (le_max_right _ _ : _ ≤ n)]

Result:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := (map f p).natDegree ⊔ p.natDegree
⊢ ∑ i ∈ range ((map f p).natDegree ⊔ p.natDegree + 1), (⇑derivative)^[i] (map f p) =
    map f (∑ i ∈ range ((map f p).natDegree ⊔ p.natDegree + 1), (⇑derivative)^[i] p)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := (map f p).natDegree ⊔ p.natDegree
⊢ sumIDeriv (map f p) = map f (sumIDeriv p)

Tactic:
rw [sumIDeriv_apply_of_le (le_max_left _ _ : _ ≤ n)]

Result:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := (map f p).natDegree ⊔ p.natDegree
⊢ ∑ i ∈ range ((map f p).natDegree ⊔ p.natDegree + 1), (⇑derivative)^[i] (map f p) = map f (sumIDeriv p)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := (map f p).natDegree ⊔ p.natDegree
⊢ ∑ i ∈ range ((map f p).natDegree ⊔ p.natDegree + 1), (⇑derivative)^[i] (map f p) =
    map f (∑ i ∈ range ((map f p).natDegree ⊔ p.natDegree + 1), (⇑derivative)^[i] p)

Tactic:
simp_rw [Polynomial.map_sum, iterate_derivative_map p f]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ sumIDeriv (map f p) = map f (sumIDeriv p)

Tactic:
let n := max (p.map f).natDegree p.natDegree

Result:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
n : ℕ := (map f p).natDegree ⊔ p.natDegree
⊢ sumIDeriv (map f p) = map f (sumIDeriv p)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_some_iff_findIdx_eq {xs : Array α} {p : α → Bool} {i : Nat} :
    xs.findIdx? p = some i ↔ i < xs.size ∧ xs.findIdx p = i

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
i : Nat
⊢ findIdx? p xs = some i ↔ i < xs.size ∧ findIdx p xs = i

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
i : Nat
xs : List α
⊢ findIdx? p { toList := xs } = some i ↔ i < { toList := xs }.size ∧ findIdx p { toList := xs } = i

Proof state:
case mk
α : Type u_1
p : α → Bool
i : Nat
xs : List α
⊢ findIdx? p { toList := xs } = some i ↔ i < { toList := xs }.size ∧ findIdx p { toList := xs } = i

Tactic:
simp [List.findIdx?_eq_some_iff_findIdx_eq]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem one_lt_tprod (hsum : Multipliable g) (hg : ∀ i, 1 ≤ g i) (i : ι) (hi : 1 < g i) :
    1 < ∏' i, g i

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
g : ι → α
hsum : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏' (x : ?m.46545), 1 < ∏' (i : ι), g i

ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
g : ι → α
hsum : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ Type ?u.46542

Tactic:
exact tprod_lt_tprod hg hi multipliable_one hsum

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
g : ι → α
hsum : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ 1 < ∏' (i : ι), g i

Tactic:
rw [← tprod_one]

Result:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
g : ι → α
hsum : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏' (x : ?m.46545), 1 < ∏' (i : ι), g i

ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
inst✝ : OrderClosedTopology α
g : ι → α
hsum : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ Type ?u.46542
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getKey? k = if k ∈ m then some k else none

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey? k = if k ∈ m then some k else none

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey? k = if m.contains k = true then some k else none

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey? k = if m.contains k = true then some k else none

Tactic:
simp_to_raw using Raw₀.getKey?_modify_self

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_image (hΦ : Isometry Φ) : infDist (Φ x) (Φ '' t) = infDist x t

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
t : Set α
x : α
Φ : α → β
hΦ : Isometry Φ
⊢ infDist (Φ x) (Φ '' t) = infDist x t

Tactic:
simp [infDist, infEdist_image hΦ]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiableAt.mfderiv (h : MDifferentiableAt I I' f x) :
    mfderiv I I' f x =
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f :) (range I) ((extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
h : MDifferentiableAt I I' f x
⊢ mfderiv I I' f x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)

Tactic:
simp only [mfderiv, h, if_pos]

Result:
no goals
-- Mathlib/Data/Int/SuccPred.lean
theorem natCast_covBy {a b : ℕ} : (a : ℤ) ⋖ b ↔ a ⋖ b

Proof state:
a b : ℕ
⊢ ↑a ⋖ ↑b ↔ a ⋖ b

Tactic:
rw [Order.covBy_iff_add_one_eq, Order.covBy_iff_add_one_eq]

Result:
a b : ℕ
⊢ ↑a + 1 = ↑b ↔ a + 1 = b

Proof state:
a b : ℕ
⊢ ↑a + 1 = ↑b ↔ a + 1 = b

Tactic:
exact Int.natCast_inj

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_eq_linear_combination (s : Finset ι) (p : ι → V) (w : ι → k)
    (hw : ∑ i ∈ s, w i = 1) : s.affineCombination k p w = ∑ i ∈ s, w i • p i

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
p : ι → V
w : ι → k
hw : ∑ i ∈ s, w i = 1
⊢ (affineCombination k s p) w = ∑ i ∈ s, w i • p i

Tactic:
simp [s.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w p hw 0]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_append {p : α → Prop} {l₁ l₂ : Vector { x // p x } n} :
    (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach

Proof state:
case mk.mk
α : Type u_1
n : Nat
p : α → Prop
toArray✝¹ : Array { x // p x }
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array { x // p x }
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }).unattach =
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.unattach ++
      { toArray := toArray✝, size_toArray := size_toArray✝ }.unattach

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Prop
l₂ : Vector { x // p x } n
toArray✝ : Array { x // p x }
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂).unattach =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.unattach ++ l₂.unattach

Tactic:
rcases l₂

Result:
case mk.mk
α : Type u_1
n : Nat
p : α → Prop
toArray✝¹ : Array { x // p x }
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array { x // p x }
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }).unattach =
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.unattach ++
      { toArray := toArray✝, size_toArray := size_toArray✝ }.unattach

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l₁ l₂ : Vector { x // p x } n
⊢ (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach

Tactic:
rcases l₁

Result:
case mk
α : Type u_1
n : Nat
p : α → Prop
l₂ : Vector { x // p x } n
toArray✝ : Array { x // p x }
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂).unattach =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.unattach ++ l₂.unattach
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_iInter {f : ι → Set α} : (⋂ i, f i).Nonempty ↔ ∃ x, ∀ i, x ∈ f i

Proof state:
α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ (⋂ i, f i).Nonempty ↔ ∃ x, ∀ (i : ι), x ∈ f i

Tactic:
simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem not_bddAbove_coe : ¬ (BddAbove <| range (fun (x : ℚ) ↦ (x : ℝ)))

Proof state:
⊢ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x} = ∅

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x} ↔ x✝ ∈ ∅

Proof state:
case h
x✝ : ℝ
⊢ x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x} ↔ x✝ ∈ ∅

Tactic:
simpa using exists_rat_gt _

Result:
no goals

Proof state:
⊢ ¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x}.Nonempty

Tactic:
rw [Set.not_nonempty_iff_eq_empty]

Result:
⊢ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x} = ∅

Proof state:
⊢ ¬BddAbove (range fun x => ↑x)

Tactic:
dsimp only [BddAbove, upperBounds]

Result:
⊢ ¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → a ≤ x}.Nonempty
-- Mathlib/Data/ENat/Basic.lean
theorem coe_toNat_eq_self : ENat.toNat n = n ↔ n ≠ ⊤ :=
  ENat.recTopCoe (by decide) (fun _ => by simp [toNat_coe]) n

Proof state:
n : ℕ∞
x✝ : ℕ
⊢ ↑(↑x✝).toNat = ↑x✝ ↔ ↑x✝ ≠ ⊤

Tactic:
simp [toNat_coe]

Result:
no goals

Proof state:
n : ℕ∞
⊢ ↑⊤.toNat = ⊤ ↔ ⊤ ≠ ⊤

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean
lemma one_le_prod {s : Multiset R} (h : ∀ a ∈ s, 1 ≤ a) : 1 ≤ s.prod

Proof state:
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : Multiset R
h : ∀ a ∈ s, 1 ≤ a
⊢ 1 ≤ s.prod

Tactic:
cases s using Quotient.ind

Result:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ ⟦a✝⟧, 1 ≤ a
⊢ 1 ≤ prod ⟦a✝⟧

Proof state:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ a✝, 1 ≤ a
⊢ 1 ≤ a✝.prod

Tactic:
apply List.one_le_prod h

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ ⟦a✝⟧, 1 ≤ a
⊢ 1 ≤ prod ⟦a✝⟧

Tactic:
simp only [quot_mk_to_coe, mem_coe, prod_coe] at *

Result:
case a
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
a✝ : List R
h : ∀ a ∈ a✝, 1 ≤ a
⊢ 1 ≤ a✝.prod
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_eq_one : a * b = 1 ↔ a = 1 ∧ b = 1 :=
  ⟨fun h => ⟨LeftCancelMonoid.eq_one_of_mul_right h, LeftCancelMonoid.eq_one_of_mul_left h⟩, by
    rintro ⟨rfl, rfl⟩
    exact mul_one _⟩

Proof state:
case intro
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1

Tactic:
exact mul_one _

Result:
no goals

Proof state:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
⊢ 1 * 1 = 1
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_apply_of_not_and {f : R → R} (a : A) (ha : ¬ (p a ∧ ContinuousOn f (spectrum R a))) :
    cfc f a = 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : ¬(p a ∧ ContinuousOn f (spectrum R a))
⊢ cfc f a = 0

Tactic:
rw [cfc_def, dif_neg ha]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem map_le_iff_le_comap (f : V ↪ W) (G : SimpleGraph V) (G' : SimpleGraph W) :
    G.map f ≤ G' ↔ G ≤ G'.comap f :=
  ⟨fun h _ _ ha => h ⟨_, _, ha, rfl, rfl⟩, by
    rintro h _ _ ⟨u, v, ha, rfl, rfl⟩
    exact h ha⟩

Proof state:
case intro.intro.intro.intro
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
h : G ≤ SimpleGraph.comap (⇑f) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj (f u) (f v)

Tactic:
exact h ha

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
⊢ G ≤ SimpleGraph.comap (⇑f) G' → SimpleGraph.map f G ≤ G'

Tactic:
rintro h _ _ ⟨u, v, ha, rfl, rfl⟩

Result:
case intro.intro.intro.intro
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
h : G ≤ SimpleGraph.comap (⇑f) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj (f u) (f v)
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem nonneg_of_zero_le_restrict (hi₂ : 0 ≤[i] v) : 0 ≤ v i

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ ↑v i

Tactic:
rw [v.not_measurable hi₁]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : MeasurableSet i
⊢ 0 ≤ ↑v i

Tactic:
exact (restrict_le_restrict_iff _ _ hi₁).1 hi₂ hi₁ Set.Subset.rfl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
⊢ 0 ≤ ↑v i

Tactic:
by_cases hi₁ : MeasurableSet i

Result:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : MeasurableSet i
⊢ 0 ≤ ↑v i

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
v : VectorMeasure α M
i : Set α
hi₂ : 0 ≤[i] v
hi₁ : ¬MeasurableSet i
⊢ 0 ≤ ↑v i
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_rel₂ {R : L.Relations 2} {t₁ t₂ : L.Term _} :
    (R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![t₁.realize v, t₂.realize v]

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]

Tactic:
rw [Relations.formula₂, realize_rel, iff_eq_eq]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (RelMap R fun i => Term.realize v (![t₁, t₂] i)) = RelMap R ![Term.realize v t₁, Term.realize v t₂]

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (RelMap R fun i => Term.realize v (![t₁, t₂] i)) = RelMap R ![Term.realize v t₁, Term.realize v t₂]

Tactic:
refine congr rfl (funext (Fin.cases ?_ ?_))

Result:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v t₂] 0

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ ∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v t₂] i.succ

Proof state:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ ∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v t₂] i.succ

Tactic:
simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Result:
no goals

Proof state:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v t₂] 0

Tactic:
simp only [Matrix.cons_val_zero]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem not_mem_iff {r : R} {a : A} : r ∉ σ a ↔ IsUnit (↑ₐ r - a)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ r ∉ σ a ↔ IsUnit (↑ₐ r - a)

Tactic:
apply not_iff_not.mp

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬r ∉ σ a ↔ ¬IsUnit (↑ₐ r - a)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : A
⊢ ¬r ∉ σ a ↔ ¬IsUnit (↑ₐ r - a)

Tactic:
simp [Set.not_not_mem, mem_iff]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblen_pos : 0 < veblen o a :=
  veblenWith_pos (isNormal_opow one_lt_omega0) (by simp)

Proof state:
o a : Ordinal.{u}
⊢ 0 < ω ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompNotation.lean
@[simp]
lemma id_comp : Kernel.id ∘ₘ μ = μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ⇑Kernel.id ∘ₘ μ = μ

Tactic:
rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem mem_range'_1 : m ∈ range' s n ↔ s ≤ m ∧ m < s + n

Proof state:
s n m : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n

Tactic:
exact ⟨
fun ⟨i, h, e⟩ => e ▸ ⟨Nat.le_add_right .., Nat.add_lt_add_left h _⟩,
fun ⟨h₁, h₂⟩ => ⟨m - s, Nat.sub_lt_left_of_lt_add h₁ h₂, (Nat.add_sub_cancel' h₁).symm⟩⟩

Result:
no goals

Proof state:
s n m : Nat
⊢ m ∈ range' s n ↔ s ≤ m ∧ m < s + n

Tactic:
simp [mem_range']

Result:
s n m : Nat
⊢ (∃ i, i < n ∧ m = s + i) ↔ s ≤ m ∧ m < s + n
-- Mathlib/Data/Part.lean
theorem div_mem_div [Div α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma / mb ∈ a / b

Proof state:
α : Type u_1
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 / a = ma / mb

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma / mb ∈ a / b

Tactic:
simp [div_def]

Result:
α : Type u_1
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 / a = ma / mb
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_C_mul : (C r * p).smeval x = r • p.smeval x

Proof state:
case h_add
R : Type u_1
inst✝³ : Semiring R
r : R
p✝ : R[X]
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Module R S
inst✝ : Pow S ℕ
x : S
p q : R[X]
ph : (C r * p).smeval x = r • p.smeval x
qh : (C r * q).smeval x = r • q.smeval x
⊢ (C r * (p + q)).smeval x = r • (p + q).smeval x

Tactic:
simp only [mul_add, smeval_add, ph, qh, smul_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Module R S
inst✝ : Pow S ℕ
x : S
⊢ (C r * p).smeval x = r • p.smeval x

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp only [mul_add, smeval_add, ph, qh, smul_add]
| h_monomial n b =>
  simp only [C_mul_monomial, smeval_monomial, mul_smul]

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
inst✝³ : Semiring R
r : R
p : R[X]
S : Type u_2
inst✝² : NonAssocSemiring S
inst✝¹ : Module R S
inst✝ : Pow S ℕ
x : S
n : ℕ
b : R
⊢ (C r * (monomial n) b).smeval x = r • ((monomial n) b).smeval x

Tactic:
simp only [C_mul_monomial, smeval_monomial, mul_smul]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.swap_mul {α : Type*} [DecidableEq α] {f : Perm α} (hf : IsCycle f) {x : α}
    (hx : f x ≠ x) (hffx : f (f x) ≠ x) : IsCycle (swap x (f x) * f) :=
  ⟨f x, by simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, if_neg hx, hx],
    fun y hy =>
    let ⟨i, hi⟩ := hf.exists_zpow_eq hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1
    have hi : (f ^ (i - 1)) (f x) = y :=
      calc
        (f ^ (i - 1) : Perm α) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ) : Perm α) x

Proof state:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
hffx : f (f x) ≠ x
⊢ (swap x (f x) * f) (f x) ≠ f x

Tactic:
simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, if_neg hx, hx]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
hffx : f (f x) ≠ x
y : α
hy : (swap x (f x) * f) y ≠ y
i : ℤ
hi : (f ^ i) x = y
⊢ (f ^ (i - 1) * f ^ 1) x = y

Tactic:
rwa [← zpow_add, sub_add_cancel]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
hffx : f (f x) ≠ x
y : α
hy : (swap x (f x) * f) y ≠ y
i : ℤ
hi : (f ^ i) x = y
⊢ (f ^ (i - 1)) (f x) = (f ^ (i - 1) * f ^ 1) x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) :
    ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Proof state:
case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p

Tactic:
rw [← ofReal_add (sub_nonneg_of_le h) hq, sub_add_cancel]

Result:
no goals

Proof state:
case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
rw [ofReal_of_nonpos (sub_nonpos_of_le h), tsub_eq_zero_of_le (ofReal_le_ofReal h)]

Result:
no goals

Proof state:
case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
refine ENNReal.eq_sub_of_add_eq ofReal_ne_top ?_

Result:
case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p

Proof state:
p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
obtain h | h := le_total p q

Result:
case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q