harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Lists.lean
theorem of_toList : ∀ l : Lists' α true, ofList (toList l) = l :=
  suffices
    ∀ (b) (h : true = b) (l : Lists' α b),
      let l' : Lists' α true

Proof state:
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := ⋯.mpr b;
    ofList l'.toList = l'
IH :
  ∀ (h : true = true),
    let l' := ⋯.mpr a;
    ofList l'.toList = l'
h : true = true
⊢ let l' := ⋯.mpr (b.cons' a);
  ofList l'.toList = l'

Tactic:
simpa [cons] using IH rfl

Result:
no goals

Proof state:
case atom
α : Type u_1
b : Bool
a✝ : α
h : true = false
⊢ let l' := ⋯.mpr (atom a✝);
  ofList l'.toList = l'

Tactic:
cases h

Result:
no goals

Proof state:
case nil
α : Type u_1
b : Bool
h : true = true
⊢ let l' := ⋯.mpr nil;
  ofList l'.toList = l'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := ⋯.mpr l;
  ofList l'.toList = l'

Tactic:
induction l with
| atom => cases h
| nil => simp
| cons' b a _ IH => simpa [cons] using IH rfl

Result:
no goals

Proof state:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α b

Tactic:
exact l

Result:
no goals

Proof state:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α true

Tactic:
rw [h]

Result:
α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ Lists' α b
-- Mathlib/Data/BitVec.lean
@[simp] lemma ofFin_natCast (n : ℕ) : ofFin (n : Fin (2^w)) = n

Proof state:
w n : ℕ
⊢ { toFin := ↑n } = ↑n

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem inverse_domain : (inverse f).domain = LinearMap.range f.toFun

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ Submodule.map (LinearMap.fst R F E) (Submodule.map (LinearEquiv.prodComm R E F) f.graph) =
    Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ f.inverse.domain = LinearMap.range f.toFun

Tactic:
rw [inverse, Submodule.toLinearPMap_domain, ← graph_map_snd_eq_range,
  ← LinearEquiv.fst_comp_prodComm, Submodule.map_comp]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ Submodule.map (LinearMap.fst R F E) (Submodule.map (LinearEquiv.prodComm R E F) f.graph) =
    Submodule.map (LinearMap.fst R F E) (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph)
-- Mathlib/Logic/Function/Basic.lean
/-- A relation `r : α → β → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some function `f`. -/
lemma forall_existsUnique_iff {r : α → β → Prop} :
    (∀ a, ∃! b, r a b) ↔ ∃ f : α → β, ∀ {a b}, r a b ↔ f a = b

Proof state:
case refine_2.intro
α : Sort u_1
β : Sort u_2
r : α → β → Prop
f : α → β
hf : ∀ {a : α} {b : β}, r a b ↔ f a = b
⊢ ∀ (a : α), ∃! b, r a b

Tactic:
simp [hf]

Result:
no goals

Proof state:
case refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩

Result:
case refine_1.refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
hr : r a✝ b✝
⊢ (fun a => Exists.choose ⋯) a✝ = b✝

case refine_1.refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
h' : (fun a => Exists.choose ⋯) a✝ = b✝
⊢ r a✝ ((fun a => Exists.choose ⋯) a✝)

Proof state:
case refine_1.refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
hr : r a✝ b✝
⊢ (fun a => Exists.choose ⋯) a✝ = b✝

case refine_1.refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
a✝ : α
b✝ : β
h' : (fun a => Exists.choose ⋯) a✝ = b✝
⊢ r a✝ ((fun a => Exists.choose ⋯) a✝)

Tactic:
exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

case refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b, r a b

Proof state:
case refine_2
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b) → ∀ (a : α), ∃! b, r a b

Tactic:
rintro ⟨f, hf⟩

Result:
case refine_2.intro
α : Sort u_1
β : Sort u_2
r : α → β → Prop
f : α → β
hf : ∀ {a : α} {b : β}, r a b ↔ f a = b
⊢ ∀ (a : α), ∃! b, r a b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_replicate {n : Nat} {a : α} :
    (replicate n a).any f = if n = 0 then false else f a

Proof state:
α : Type u_1
f : α → Bool
n : Nat
a : α
⊢ (replicate n a).any f = if n = 0 then false else f a

Tactic:
cases n <;> simp [replicate_succ]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_mul_eq_prod_mul_of_exists {s : Finset α} {f : α → β} {b₁ b₂ : β}
    (a : α) (ha : a ∈ s) (h : f a * b₁ = f a * b₂) :
    (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
b₁ b₂ : β
a : α
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂

Tactic:
simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
b₁ b₂ : β
a : α
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
b₁ b₂ : β
a : α
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Tactic:
classical
rw [← insert_erase ha]
simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
b₁ b₂ : β
a : α
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (f a * ∏ a ∈ s.erase a, f a) * b₁ = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
b₁ b₂ : β
a : α
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Tactic:
rw [← insert_erase ha]

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
b₁ b₂ : β
a : α
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ insert a (s.erase a), f a) * b₁ = (∏ a ∈ insert a (s.erase a), f a) * b₂
-- Mathlib/Analysis/Convex/Deriv.lean
lemma slope_le_of_hasDerivWithinAt_Ioi (hfc : ConcaveOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Ioi x) x) :
    slope f x y ≤ f'

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Ioi x) x
⊢ slope f x y ≤ f'

Tactic:
simpa only [Pi.neg_def, slope_neg, neg_neg] using
  neg_le_neg (hfc.neg.le_slope_of_hasDerivWithinAt_Ioi hx hy hxy hf'.neg)

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem modEq_iff_toIocMod_eq_right : a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ a ≡ b [PMOD p] ↔ toIocMod hp a b = a + p

Tactic:
refine modEq_iff_eq_add_zsmul.trans ⟨?_, fun h => ⟨toIocDiv hp a b + 1, ?_⟩⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ z, b = a + z • p) → toIocMod hp a b = a + p

case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b = a + (toIocDiv hp a b + 1) • p

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b = a + (toIocDiv hp a b + 1) • p

Tactic:
rwa [add_one_zsmul, add_left_comm, ← sub_eq_iff_eq_add']

Result:
no goals

Proof state:
case refine_1.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ toIocMod hp a (a + z • p) = a + p

Tactic:
rw [toIocMod_add_zsmul, toIocMod_apply_left]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ z, b = a + z • p) → toIocMod hp a b = a + p

Tactic:
rintro ⟨z, rfl⟩

Result:
case refine_1.intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
z : ℤ
⊢ toIocMod hp a (a + z • p) = a + p
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_eq_iInf (s : Set α) : m.trim s = ⨅ (t) (_ : s ⊆ t) (_ : MeasurableSet t), m t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t

Tactic:
simp (config := { singlePass := true }) only [iInf_comm]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), m t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : MeasurableSet t), ⨅ (_ : s ⊆ t), m t

Tactic:
exact
  inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => measure_iUnion_le f)
    (fun _ _ _ _ h => measure_mono h) s

Result:
no goals
-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem restrictDvd_def [Decidable (q = 0)] (hpq : p ∣ q) :
    restrictDvd hpq =
      if hq : q = 0 then 1
      else
        @restrict F _ p _ _ _
          ⟨splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q)
              hpq⟩

Proof state:
F : Type u_1
inst✝¹ : Field F
p q : F[X]
inst✝ : Decidable (q = 0)
hpq : p ∣ q
⊢ (if hq : q = 0 then 1 else restrict p q.SplittingField) = if hq : q = 0 then 1 else restrict p q.SplittingField

Tactic:
congr

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
p q : F[X]
inst✝ : Decidable (q = 0)
hpq : p ∣ q
⊢ restrictDvd hpq = if hq : q = 0 then 1 else restrict p q.SplittingField

Tactic:
unfold restrictDvd

Result:
F : Type u_1
inst✝¹ : Field F
p q : F[X]
inst✝ : Decidable (q = 0)
hpq : p ∣ q
⊢ (if hq : q = 0 then 1 else restrict p q.SplittingField) = if hq : q = 0 then 1 else restrict p q.SplittingField
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_bool (f : Bool → α) : ∏' i : Bool, f i = f false * f true

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : Bool → α
⊢ ∏' (i : Bool), f i = f false * f true

Tactic:
rw [tprod_fintype, Fintype.prod_bool, mul_comm]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem preimage_symm_proj_baseSet :
    e.toPartialEquiv.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ x.1 ∈ e.baseSet

Tactic:
exact e.mem_target.mp hx

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
⊢ ↑e.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target

Tactic:
refine inter_eq_right.mpr fun x hx => ?_

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ x ∈ ↑e.symm ⁻¹' (proj ⁻¹' e.baseSet)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ x ∈ ↑e.symm ⁻¹' (proj ⁻¹' e.baseSet)

Tactic:
simp only [mem_preimage, PartialEquiv.invFun_as_coe, e.proj_symm_apply hx]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : B × F
hx : x ∈ e.target
⊢ x.1 ∈ e.baseSet
-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : Fact p.Prime] (hq0 : (q : ZMod p) ≠ 0) :
    ∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q =
    p / 2 * (q / 2)

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
⊢ False

Tactic:
have : (x.1 : ZMod p) = 0 := by
  simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : ↑x.1 = 0
⊢ False

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : ↑x.1 = 0
⊢ False

Tactic:
apply_fun ZMod.val at this

Result:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
this : (↑x.1).val = val 0
⊢ False

Proof state:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #(filter (fun x => x.2 * q ≤ x.1 * p) (Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ)) =
    #(filter (fun x => x.1 * q ≤ x.2 * p) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
hxp : x.1 < p
⊢ ↑x.1 = 0

Tactic:
simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)

Result:
no goals
-- Mathlib/Order/RelSeries.lean
lemma Rel.finiteDimensional_or_infiniteDimensional [Nonempty α] :
    r.FiniteDimensional ∨ r.InfiniteDimensional

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ r.FiniteDimensional ∨ ¬r.FiniteDimensional

Tactic:
exact em r.FiniteDimensional

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ r.FiniteDimensional ∨ r.InfiniteDimensional

Tactic:
rw [← not_finiteDimensional_iff]

Result:
α : Type u_1
r : Rel α α
inst✝ : Nonempty α
⊢ r.FiniteDimensional ∨ ¬r.FiniteDimensional
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Stream.next?_toList {s : RBNode.Stream α} :
    (s.next?.map fun (a, b) => (a, b.toList)) = s.toList.next?

Proof state:
α : Type u_1
s : RBNode.Stream α
⊢ Option.map
      (fun x =>
        match x with
        | (a, b) => (a, b.toList))
      s.next? =
    s.toList.next?

Tactic:
cases s <;> simp [next?, toStream_toList']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem neg_zero (n:Nat) : -BitVec.ofNat n 0 = BitVec.ofNat n 0

Proof state:
case a
n : Nat
⊢ (-0#n).toNat = (0#n).toNat

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
⊢ -0#n = 0#n

Tactic:
apply eq_of_toNat_eq

Result:
case a
n : Nat
⊢ (-0#n).toNat = (0#n).toNat
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma interior_range_modelWithCornersEuclideanHalfSpace (n : ℕ) [NeZero n] :
    interior (range (𝓡∂ n)) = { y | 0 < y 0 }

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ interior (range ↑(𝓡∂ n)) = {y | 0 < y 0}

Tactic:
calc interior (range (𝓡∂ n))
  _ = interior ({ y | 0 ≤ y 0}) := by
    congr!
    apply range_euclideanHalfSpace
  _ = { y | 0 < y 0 } := interior_halfSpace _ _ _

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ interior (range ↑(𝓡∂ n)) = interior {y | 0 ≤ y 0}

Tactic:
congr!

Result:
case h.e'_3
n : ℕ
inst✝ : NeZero n
⊢ range ↑(𝓡∂ n) = {y | 0 ≤ y 0}

Proof state:
case h.e'_3
n : ℕ
inst✝ : NeZero n
⊢ range ↑(𝓡∂ n) = {y | 0 ≤ y 0}

Tactic:
apply range_euclideanHalfSpace

Result:
no goals
-- Mathlib/Data/Real/Sign.lean
theorem inv_sign (r : ℝ) : (sign r)⁻¹ = sign r

Proof state:
case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hp]

Result:
case inr.inr
r : ℝ
hp : r.sign = 1
⊢ 1⁻¹ = 1

Proof state:
case inl
r : ℝ
hn : r.sign = -1
⊢ (-1)⁻¹ = -1

Tactic:
norm_num

Result:
no goals

Proof state:
case inr.inl
r : ℝ
hz : r.sign = 0
⊢ 0⁻¹ = 0

Tactic:
exact inv_zero

Result:
no goals

Proof state:
case inl
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hn]

Result:
case inl
r : ℝ
hn : r.sign = -1
⊢ (-1)⁻¹ = -1

Proof state:
case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

Tactic:
rw [hz]

Result:
case inr.inl
r : ℝ
hz : r.sign = 0
⊢ 0⁻¹ = 0

Proof state:
r : ℝ
⊢ r.sign⁻¹ = r.sign

Tactic:
obtain hn | hz | hp := sign_apply_eq r

Result:
case inl
r : ℝ
hn : r.sign = -1
⊢ r.sign⁻¹ = r.sign

case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Proof state:
case inr.inr
r : ℝ
hp : r.sign = 1
⊢ 1⁻¹ = 1

Tactic:
exact inv_one

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem toMatrix_toPEquiv_mul [Fintype m] [DecidableEq m]
    [Semiring α] (f : l ≃ m) (M : Matrix m n α) :
    f.toPEquiv.toMatrix * M = M.submatrix f id

Proof state:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
⊢ (f.toPEquiv.toMatrix * M) i j = M.submatrix (⇑f) id i j

Tactic:
rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]

Result:
no goals

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃ m
M : Matrix m n α
⊢ f.toPEquiv.toMatrix * M = M.submatrix (⇑f) id

Tactic:
ext i j

Result:
case a
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃ m
M : Matrix m n α
i : l
j : n
⊢ (f.toPEquiv.toMatrix * M) i j = M.submatrix (⇑f) id i j
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
`f` is a monotone function. -/
lemma monotone_of_hasDerivAt_nonneg {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x)
    (hf' : 0 ≤ f') : Monotone f :=
  monotone_of_deriv_nonneg (fun _ ↦ (hf _).differentiableAt) fun x ↦ by
    rw [(hf _).deriv]; exact hf' _

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x

Tactic:
exact hf' _

Result:
no goals

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ deriv f x

Tactic:
rw [(hf _).deriv]

Result:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma mul_comm_iff {f : S → R} {a b : A} :
    QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁷ : Semifield R
inst✝⁶ : Field S
inst✝⁵ : NonUnitalRing A
inst✝⁴ : Module R A
inst✝³ : Module S A
inst✝² : Algebra R S
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass S A A
f : S → R
a b : A
⊢ QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f

Tactic:
simp only [quasispectrumRestricts_iff, quasispectrum.mul_comm]

Result:
no goals
-- Mathlib/Tactic/NormNum/NatFib.lean
theorem isFibAux_two_mul {n a b n' a' b' : ℕ} (H : IsFibAux n a b)
    (hn : 2 * n = n') (h1 : a * (2 * b - a) = a') (h2 : a * a + b * b = b') :
    IsFibAux n' a' b' :=
  ⟨by rw [← hn, fib_two_mul, H.1, H.2, ← h1],
   by rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]⟩

Proof state:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib (n' + 1) = b'

Tactic:
rw [← hn, fib_two_mul_add_one, H.1, H.2, pow_two, pow_two, add_comm, h2]

Result:
no goals

Proof state:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib n' = a'

Tactic:
rw [← hn, fib_two_mul, H.1, H.2, ← h1]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem prod_eq_zero {ι} (f : ι → Cardinal.{u}) : prod f = 0 ↔ ∃ i, f i = 0

Proof state:
ι : Type u_1
f : ι → Cardinal.{u}
⊢ prod f = 0 ↔ ∃ i, f i = 0

Tactic:
lift f to ι → Type u using fun _ => trivial

Result:
case intro
ι : Type u_1
f : ι → Type u
⊢ (prod fun i => #(f i)) = 0 ↔ ∃ i, (fun i => #(f i)) i = 0

Proof state:
case intro
ι : Type u_1
f : ι → Type u
⊢ (prod fun i => #(f i)) = 0 ↔ ∃ i, (fun i => #(f i)) i = 0

Tactic:
simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem gradient_eq_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : ∇ f x = 0

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
h : ¬DifferentiableAt 𝕜 f x
⊢ ∇ f x = 0

Tactic:
rw [gradient, fderiv_zero_of_not_differentiableAt h, map_zero]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
    (f * ζ) x = ∑ i ∈ divisors x, f i

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ f i.1 * ↑ζ i.2 = f i.1

Tactic:
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩

Result:
case intro
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ f i.1 * ↑ζ i.2 = f i.1

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, f x.1 * ↑ζ x.2 = ∑ i ∈ x.divisors, f i

Tactic:
trans ∑ i ∈ divisorsAntidiagonal x, f i.1

Result:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, f x.1 * ↑ζ x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.1

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.1 = ∑ i ∈ x.divisors, f i

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.1 = ∑ i ∈ x.divisors, f i

Tactic:
rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ (f * ↑ζ) x = ∑ i ∈ x.divisors, f i

Tactic:
rw [mul_apply]

Result:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, f x.1 * ↑ζ x.2 = ∑ i ∈ x.divisors, f i

Proof state:
case intro
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ f i.1 * ↑ζ i.2 = f i.1

Tactic:
rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, f x.1 * ↑ζ x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.1

Tactic:
refine sum_congr rfl fun i hi => ?_

Result:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ f i.1 * ↑ζ i.2 = f i.1