harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/IndepAxioms.lean
theorem _root_.Matroid.existsMaximalSubsetProperty_of_bdd {P : Set α → Prop}
    (hP : ∃ (n : ℕ), ∀ Y, P Y → Y.encard ≤ n) (X : Set α) : ExistsMaximalSubsetProperty P X

Proof state:
case intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K => P K ∧ K ⊆ X) J

Tactic:
obtain ⟨Y, ⟨hY, hIY, hYX⟩, hY'⟩ :=
  Finite.exists_maximal_wrt' ncard _ hfin ⟨I, hI, rfl.subset, hIX⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ a' ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}, Y.ncard ≤ a'.ncard → Y.ncard = a'.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K => P K ∧ K ⊆ X) J
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_basis_of_ne (hij : i ≠ j) (hj : j ∈ s) : (Lagrange.basis s v i).eval (v j) = 0

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0

Tactic:
exact ⟨j, ⟨mem_erase.mpr ⟨hij.symm, hj⟩, eval_basisDivisor_right⟩⟩

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ eval (v j) (Lagrange.basis s v i) = 0

Tactic:
simp_rw [Lagrange.basis, eval_prod, prod_eq_zero_iff]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hij : i ≠ j
hj : j ∈ s
⊢ ∃ a ∈ s.erase i, eval (v j) (basisDivisor (v i) (v a)) = 0
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem IsPRadical.trans [IsPRadical i p] [IsPRadical f p] :
    IsPRadical (f.comp i) p where
  pow_mem' x

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : i x ∈ RingHom.ker f
⊢ x ∈ pNilradical K p

Tactic:
simpa only [← Ideal.mem_comap, comap_pNilradical] using ker_le f p h

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
m : ℕ
z : K
hz : i z = y ^ p ^ m
⊢ (f.comp i) z = x ^ p ^ (n + m)

Tactic:
rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Tactic:
obtain ⟨m, z, hz⟩ := pow_mem i p y

Result:
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
m : ℕ
z : K
hz : i z = y ^ p ^ m
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Proof state:
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
m : ℕ
z : K
hz : i z = y ^ p ^ m
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Tactic:
exact ⟨n + m, z, by rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]⟩

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Tactic:
obtain ⟨n, y, hy⟩ := pow_mem f p x

Result:
case intro.intro
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : M
n : ℕ
y : L
hy : f y = x ^ p ^ n
⊢ ∃ n y, (f.comp i) y = x ^ p ^ n

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : x ∈ RingHom.ker (f.comp i)
⊢ x ∈ pNilradical K p

Tactic:
rw [RingHom.mem_ker, RingHom.comp_apply, ← RingHom.mem_ker] at h

Result:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst✝¹ : IsPRadical i p
inst✝ : IsPRadical f p
x : K
h : i x ∈ RingHom.ker f
⊢ x ∈ pNilradical K p
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem map_measurableSpace_eq_borel [SecondCountableTopology Y] {f : X → Y} (hf : Measurable f)
    (hsurj : Surjective f) : MeasurableSpace.map f ‹MeasurableSpace X› = borel Y

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
letI := borel Y

Result:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this : MeasurableSpace Y := borel Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
have d := hf.mono le_rfl OpensMeasurableSpace.borel_le

Result:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this✝ : MeasurableSpace Y := borel Y
this : BorelSpace Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
exact d.map_measurableSpace_eq hsurj

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this : MeasurableSpace Y := borel Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
haveI : BorelSpace Y := ⟨rfl⟩

Result:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this✝ : MeasurableSpace Y := borel Y
this : BorelSpace Y
⊢ MeasurableSpace.map f inst✝⁶ = borel Y
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_lintegral_enorm_sub_div {f : α → E} (hf : LocallyIntegrable f μ) :
    ∀ᵐ x ∂μ, Tendsto (fun a => (∫⁻ y in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
⊢ ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
intro n

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)

Tactic:
filter_upwards [ae_all_iff.2 this] with x hx

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → E
hf : LocallyIntegrable f μ
u : ℕ → Set α
u_open : ∀ (n : ℕ), IsOpen (u n)
u_univ : ⋃ n, u n = univ
hu : ∀ (n : ℕ), IntegrableOn f (u n) μ
this :
  ∀ (n : ℕ),
    ∀ᵐ (x : α) ∂μ,
      Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u n).indicator f y - (u n).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
x : α
hx :
  ∀ (i : ℕ),
    Tendsto (fun a => (∫⁻ (y : α) in a, ‖(u i).indicator f y - (u i).indicator f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
⊢ Tendsto (fun a => (∫⁻ (y : α) in a, ‖f y - f x‖ₑ ∂μ) / μ a) (v.filterAt x) (𝓝 0)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).toList = List.ofFn f

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_add (p q : SkewMonoidAlgebra k G) (a : G) :
    coeff (p + q) a = coeff p a + coeff q a

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p q : SkewMonoidAlgebra k G
a : G
⊢ (p + q).coeff a = p.coeff a + q.coeff a

Tactic:
rcases p

Result:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
q : SkewMonoidAlgebra k G
a : G
toFinsupp✝ : G →₀ k
⊢ ({ toFinsupp := toFinsupp✝ } + q).coeff a = { toFinsupp := toFinsupp✝ }.coeff a + q.coeff a

Proof state:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
toFinsupp✝¹ toFinsupp✝ : G →₀ k
⊢ (toFinsupp✝¹ + toFinsupp✝) a = toFinsupp✝¹ a + toFinsupp✝ a

Tactic:
exact Finsupp.add_apply _ _ _

Result:
no goals

Proof state:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
q : SkewMonoidAlgebra k G
a : G
toFinsupp✝ : G →₀ k
⊢ ({ toFinsupp := toFinsupp✝ } + q).coeff a = { toFinsupp := toFinsupp✝ }.coeff a + q.coeff a

Tactic:
rcases q

Result:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
toFinsupp✝¹ toFinsupp✝ : G →₀ k
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).coeff a =
    { toFinsupp := toFinsupp✝¹ }.coeff a + { toFinsupp := toFinsupp✝ }.coeff a

Proof state:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
toFinsupp✝¹ toFinsupp✝ : G →₀ k
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).coeff a =
    { toFinsupp := toFinsupp✝¹ }.coeff a + { toFinsupp := toFinsupp✝ }.coeff a

Tactic:
simp_rw [← ofFinsupp_add, coeff]

Result:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
toFinsupp✝¹ toFinsupp✝ : G →₀ k
⊢ (toFinsupp✝¹ + toFinsupp✝) a = toFinsupp✝¹ a + toFinsupp✝ a
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_left_Ioo (a b c : α) : (Ioo a b).image (c + ·) = Ioo (c + a) (c + b)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
rw [← map_add_left_Ioo, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < (k + 1) * n) : m / n = k :=
have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
  rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
Nat.le_antisymm
  (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi))
  ((Nat.le_div_iff_mul_le npos).2 lo)

Proof state:
k n m : Nat
lo : k * n ≤ m
hi : m < (k + 1) * n
hn : n = 0
⊢ False

Tactic:
rw [hn, Nat.mul_zero] at hi lo

Result:
k n m : Nat
lo : 0 ≤ m
hi : m < 0
hn : n = 0
⊢ False

Proof state:
k n m : Nat
lo : 0 ≤ m
hi : m < 0
hn : n = 0
⊢ False

Tactic:
exact absurd lo (Nat.not_le_of_gt hi)

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem finrank_le_card [Fintype G] : finrank (subfield G F) F ≤ Fintype.card G

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
⊢ finrank (↥(subfield G F)) F ≤ Fintype.card G

Tactic:
rw [← @Nat.cast_le Cardinal, finrank_eq_rank]

Result:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
⊢ Module.rank (↥(subfield G F)) F ≤ ↑(Fintype.card G)

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
⊢ Module.rank (↥(subfield G F)) F ≤ ↑(Fintype.card G)

Tactic:
apply rank_le_card

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Basic.lean
theorem repr_algebraMap {ι : Type*} [DecidableEq ι] {B : Basis ι R S} {i : ι} (hBi : B i = 1)
    (r : R) : B.repr ((algebraMap R S) r) = fun j : ι ↦ if i = j then r else 0

Proof state:
R : Type u
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type u_3
inst✝ : DecidableEq ι
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
⊢ ⇑(B.repr ((algebraMap R S) r)) = fun j => if i = j then r else 0

Tactic:
ext j

Result:
case h
R : Type u
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type u_3
inst✝ : DecidableEq ι
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
j : ι
⊢ (B.repr ((algebraMap R S) r)) j = if i = j then r else 0

Proof state:
case h
R : Type u
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type u_3
inst✝ : DecidableEq ι
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
j : ι
⊢ (r • if i = j then 1 else 0) = if i = j then r else 0

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type u_3
inst✝ : DecidableEq ι
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
j : ι
⊢ (B.repr ((algebraMap R S) r)) j = if i = j then r else 0

Tactic:
rw [Algebra.algebraMap_eq_smul_one, map_smul, ← hBi, Finsupp.smul_apply, B.repr_self_apply]

Result:
case h
R : Type u
S : Type u_2
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
ι : Type u_3
inst✝ : DecidableEq ι
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
j : ι
⊢ (r • if i = j then 1 else 0) = if i = j then r else 0
-- Mathlib/Analysis/Convex/Slope.lean
theorem convexOn_of_slope_mono_adjacent (hs : Convex 𝕜 s)
    (hf :
      ∀ {x y z : 𝕜},
        x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)) :
    ConvexOn 𝕜 s f :=
  LinearOrder.convexOn_of_lt hs fun x hx z hz hxz a b ha hb hab => by
    let y := a * x + b * z
    have hxy : x < y

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (a * x + b * z - x) / (z - x) = b

Tactic:
simp_rw [div_eq_iff hxz.ne', ← hab]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) ≤ (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (1 - b) * x + b * z - x = b * (z - x)
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem length (h : Red L₁ L₂) : ∃ n, L₁.length = L₂.length + 2 * n

Proof state:
case tail
α : Type u
L₁ L₂✝ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
ih : ∃ n, L₁.length = L₂.length + 2 * n
⊢ ∃ n, L₁.length = L₃.length + 2 * n

Tactic:
rcases ih with ⟨n, eq⟩

Result:
case tail.intro
α : Type u
L₁ L₂✝ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : L₁.length = L₂.length + 2 * n
⊢ ∃ n, L₁.length = L₃.length + 2 * n

Proof state:
case refl
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∃ n, L₁.length = L₁.length + 2 * n

Tactic:
exact ⟨0, rfl⟩

Result:
no goals

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ n, L₁.length = L₂.length + 2 * n

Tactic:
induction' h with L₂ L₃ _h₁₂ h₂₃ ih

Result:
case refl
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∃ n, L₁.length = L₁.length + 2 * n

case tail
α : Type u
L₁ L₂✝ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
ih : ∃ n, L₁.length = L₂.length + 2 * n
⊢ ∃ n, L₁.length = L₃.length + 2 * n

Proof state:
case tail.intro
α : Type u
L₁ L₂✝ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : L₁.length = L₂.length + 2 * n
⊢ L₁.length = L₃.length + 2 * (1 + n)

Tactic:
simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]

Result:
no goals

Proof state:
case tail.intro
α : Type u
L₁ L₂✝ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : L₁.length = L₂.length + 2 * n
⊢ ∃ n, L₁.length = L₃.length + 2 * n

Tactic:
exists 1 + n

Result:
case tail.intro
α : Type u
L₁ L₂✝ L₂ L₃ : List (α × Bool)
_h₁₂ : ReflTransGen Step L₁ L₂
h₂₃ : Step L₂ L₃
n : ℕ
eq : L₁.length = L₂.length + 2 * n
⊢ L₁.length = L₃.length + 2 * (1 + n)
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime {n x y : ℕ} (h : n = x ^ 2 + y ^ 2)
    (hc : x.Coprime y) : IsSquare (-1 : ZMod n)

Proof state:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hc : x.Coprime y
⊢ IsSquare (-1)

Tactic:
zify at h

Result:
n x y : ℕ
hc : x.Coprime y
h : ↑n = ↑x ^ 2 + ↑y ^ 2
⊢ IsSquare (-1)

Proof state:
n x y : ℕ
hc : x.Coprime y
h : ↑n = ↑x ^ 2 + ↑y ^ 2
⊢ IsSquare (-1)

Tactic:
exact ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem det_eq_sign_charpoly_coeff (M : Matrix n n R) :
    M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0

Tactic:
rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.det = (-1 • eval ((scalar n) 0) (X - C M)).det

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.det = (-1 • eval ((scalar n) 0) (X - C M)).det

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_empty {c} : (empty c : Raw₀ α β).1.isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c : Nat
⊢ (empty c).val.isEmpty = true

Tactic:
rw [Raw.isEmpty_eq_isEmpty wfImp_empty, toListModel_buckets_empty, List.isEmpty_nil]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/Bounds.lean
theorem log_le_harmonic_floor (y : ℝ) (hy : 0 ≤ y) :
    Real.log y ≤ harmonic ⌊y⌋₊

Proof state:
case neg.hxy
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ ↑⌈y⌉₊ ≤ ↑(⌊y⌋₊ + 1)

Tactic:
norm_cast

Result:
case neg.hxy
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ ⌈y⌉₊ ≤ ⌊y⌋₊ + 1

Proof state:
case neg
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ Real.log ↑(⌊y⌋₊ + 1)

Tactic:
gcongr

Result:
case neg.hxy
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ y ≤ ↑(⌊y⌋₊ + 1)

Proof state:
case neg
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ ↑(harmonic ⌊y⌋₊)

Tactic:
calc
  _ ≤ Real.log ↑(Nat.floor y + 1) := ?_
  _ ≤ _ := log_add_one_le_harmonic _

Result:
case neg
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ Real.log ↑(⌊y⌋₊ + 1)

Proof state:
case neg.hxy
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ ⌈y⌉₊ ≤ ⌊y⌋₊ + 1

Tactic:
exact Nat.ceil_le_floor_add_one y

Result:
no goals

Proof state:
case neg.hxy
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ y ≤ ↑(⌊y⌋₊ + 1)

Tactic:
apply (Nat.le_ceil y).trans

Result:
case neg.hxy
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ ↑⌈y⌉₊ ≤ ↑(⌊y⌋₊ + 1)

Proof state:
case pos
y : ℝ
hy : 0 ≤ y
h0 : y = 0
⊢ Real.log y ≤ ↑(harmonic ⌊y⌋₊)

Tactic:
simp [h0]

Result:
no goals

Proof state:
y : ℝ
hy : 0 ≤ y
⊢ Real.log y ≤ ↑(harmonic ⌊y⌋₊)

Tactic:
by_cases h0 : y = 0

Result:
case pos
y : ℝ
hy : 0 ≤ y
h0 : y = 0
⊢ Real.log y ≤ ↑(harmonic ⌊y⌋₊)

case neg
y : ℝ
hy : 0 ≤ y
h0 : ¬y = 0
⊢ Real.log y ≤ ↑(harmonic ⌊y⌋₊)
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem not_bddAbove_fp_family [Small.{u} ι] (H : ∀ i, IsNormal (f i)) :
    ¬ BddAbove (⋂ i, Function.fixedPoints (f i))

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ¬BddAbove (⋂ i, fixedPoints (f i))

Tactic:
rw [not_bddAbove_iff]

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (x : Ordinal.{u}), ∃ y ∈ ⋂ i, fixedPoints (f i), x < y

Proof state:
case intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
i : ι
⊢ nfpFamily f (succ a) ∈ (fun i => fixedPoints (f i)) i

Tactic:
exact nfpFamily_fp (H i) _

Result:
no goals

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
⊢ nfpFamily f (succ a) ∈ ⋂ i, fixedPoints (f i)

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case intro
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
i : ι
⊢ nfpFamily f (succ a) ∈ (fun i => fixedPoints (f i)) i

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ∀ (x : Ordinal.{u}), ∃ y ∈ ⋂ i, fixedPoints (f i), x < y

Tactic:
refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
⊢ nfpFamily f (succ a) ∈ ⋂ i, fixedPoints (f i)