harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_of_degrees_lt_of_eval_finset_eq (degree_f_lt : f.degree < #s)
    (degree_g_lt : g.degree < #s) (eval_fg : ∀ x ∈ s, f.eval x = g.eval x) : f = g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ (f - g).degree < ↑(#s)

Tactic:
rw [← mem_degreeLT]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g ∈ degreeLT R #s

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f.degree < ↑(#s)
degree_g_lt : g.degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
rw [← mem_degreeLT] at degree_f_lt degree_g_lt

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g ∈ degreeLT R #s

Tactic:
exact Submodule.sub_mem _ degree_f_lt degree_g_lt

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
refine eq_of_degree_sub_lt_of_eval_finset_eq _ ?_ eval_fg

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_f_lt : f ∈ degreeLT R #s
degree_g_lt : g ∈ degreeLT R #s
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ (f - g).degree < ↑(#s)
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
lemma tensor_map_id_left_eq_map :
    (AlgebraTensorModule.map LinearMap.id f) =
      (ofTensorProductEquivOfFiniteNoetherian I N).symm.toLinearMap ∘ₗ
      map I f ∘ₗ
      (ofTensorProductEquivOfFiniteNoetherian I M).toLinearMap

Proof state:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ map I f ∘ₗ ↑(ofTensorProductEquivOfFiniteNoetherian I M)

Tactic:
erw [ofTensorProduct_naturality I f]

Result:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f

Proof state:
case a.h.h
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
x : M
⊢ ((AlgebraTensorModule.curry (AlgebraTensorModule.map LinearMap.id f)) 1) x =
    ((AlgebraTensorModule.curry
          (↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ
            ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f))
        1)
      x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ AlgebraTensorModule.map LinearMap.id f =
    ↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f

Tactic:
ext x

Result:
case a.h.h
R : Type u
inst✝⁷ : CommRing R
I : Ideal R
inst✝⁶ : IsNoetherianRing R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
f : M →ₗ[R] N
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
x : M
⊢ ((AlgebraTensorModule.curry (AlgebraTensorModule.map LinearMap.id f)) 1) x =
    ((AlgebraTensorModule.curry
          (↑(ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ
            ofTensorProduct I N ∘ₗ AlgebraTensorModule.map LinearMap.id f))
        1)
      x
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_sub {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) :
    ∫ a, f a - g a ∂μ = ∫ a, f a ∂μ - ∫ a, g a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => f a - g a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a - g a) hf) else 0
    else 0) =
    (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0) -
      if h : True then
        if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
      else 0

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => f a - g a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a - g a) hf) else 0
    else 0) =
    (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0) -
      if h : True then
        if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
      else 0

Tactic:
exact setToFun_sub (dominatedFinMeasAdditive_weightedSMul μ) hf hg

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a - g a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ

Tactic:
simp [integral, hG]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version with absolute values) -/
lemma hasSum_nat_hurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ (SignType.sign (n + a) / (↑|n + a| : ℂ) ^ s
      - SignType.sign (n + 1 - a) / (↑|n + 1 - a| : ℂ) ^ s) / 2) (hurwitzZetaOdd a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑n + 1) + a)) / ↑|-(↑n + 1) + a| ^ s / 2

Tactic:
have : -(n + 1) + a = -(n + 1 - a) := by ring_nf

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑n + 1) + a)) / ↑|-(↑n + 1) + a| ^ s / 2

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ -(↑n + 1) + a = -(↑n + 1 - a)

Tactic:
ring_nf

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2 =
    ↑(SignType.sign (↑↑n + a)) / ↑|↑↑n + a| ^ s / 2 + ↑(SignType.sign (↑(-(↑n + 1)) + a)) / ↑|↑(-(↑n + 1)) + a| ^ s / 2

Tactic:
rw [Int.cast_neg, Int.cast_add, Int.cast_one, sub_div, sub_eq_add_neg, Int.cast_natCast]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑n + 1) + a)) / ↑|-(↑n + 1) + a| ^ s / 2

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑n + 1) + a)) / ↑|-(↑n + 1) + a| ^ s / 2

Tactic:
rw [this, Left.sign_neg, abs_neg, SignType.coe_neg, neg_div, neg_div]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2)
    (hurwitzZetaOdd (↑a) s)

Tactic:
refine (hasSum_int_hurwitzZetaOdd a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2 =
    ↑(SignType.sign (↑↑n + a)) / ↑|↑↑n + a| ^ s / 2 + ↑(SignType.sign (↑(-(↑n + 1)) + a)) / ↑|↑(-(↑n + 1)) + a| ^ s / 2
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem ofPrime_idealOfLE (R S : ValuationSubring K) (h : R ≤ S) :
    ofPrime R (idealOfLE R S h) = S

Proof state:
case h.mp.intro.intro.intro.a.ha
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a r : ↥R
hr : r ∈ (R.idealOfLE S h).primeCompl
⊢ 0 < S.valuation ((algebraMap (↥R) K) r)

Tactic:
simpa [Valuation.pos_iff] using fun hr₀ ↦ hr₀ ▸ hr <| Ideal.zero_mem (R.idealOfLE S h)

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioo_succ_right_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ioo a (succ b) = Ioc a b :=
  coe_injective <| by simpa using Set.Ioo_succ_right_eq_Ioc_of_not_isMax hb _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ioo a (succ b)) = ↑(Ioc a b)

Tactic:
simpa using Set.Ioo_succ_right_eq_Ioc_of_not_isMax hb _

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean
theorem ContinuousLinearEquiv.homothety_inverse (a : ℝ) (ha : 0 < a) (f : E ≃ₛₗ[σ] F) :
    (∀ x : E, ‖f x‖ = a * ‖x‖) → ∀ y : F, ‖f.symm y‖ = a⁻¹ * ‖y‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
⊢ (∀ (x : E), ‖f x‖ = a * ‖x‖) → ∀ (y : F), ‖f.symm y‖ = a⁻¹ * ‖y‖

Tactic:
intro hf y

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ ‖f.symm y‖ = a⁻¹ * ‖y‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ ‖f.symm y‖ = a⁻¹ * ‖y‖

Tactic:
calc
  ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖) := by
    rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]
  _ = a⁻¹ * ‖f (f.symm y)‖ := by rw [hf]
  _ = a⁻¹ * ‖y‖ := by simp

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖)

Tactic:
rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ a⁻¹ * (a * ‖f.symm y‖) = a⁻¹ * ‖f (f.symm y)‖

Tactic:
rw [hf]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ a⁻¹ * ‖f (f.symm y)‖ = a⁻¹ * ‖y‖

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
/-- For every element `e` of an independent set `I`,
there is a cocircuit whose intersection with `I` is `{e}`. -/
lemma Indep.exists_isCocircuit_inter_eq_mem (hI : M.Indep I) (heI : e ∈ I) :
    ∃ K, M.IsCocircuit K ∧ K ∩ I = {e}

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ ∃ K, M.IsCocircuit K ∧ K ∩ I = {e}

Tactic:
refine ⟨M.fundCocircuit e B, fundCocircuit_isCocircuit (hIB heI) hB, ?_⟩

Result:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I = {e}

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I = {e}

Tactic:
rw [subset_antisymm_iff, subset_inter_iff, singleton_subset_iff, and_iff_right
  (mem_fundCocircuit _ _ _), singleton_subset_iff, and_iff_left heI,
  ← M.fundCocircuit_inter_eq (hIB heI)]

Result:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B

Proof state:
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
⊢ ∃ K, M.IsCocircuit K ∧ K ∩ I = {e}

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Result:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ ∃ K, M.IsCocircuit K ∧ K ∩ I = {e}

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
heI : e ∈ I
B : Set α
hB : M.IsBase B
hIB : I ⊆ B
⊢ M.fundCocircuit e B ∩ I ⊆ M.fundCocircuit e B ∩ B

Tactic:
exact inter_subset_inter_right _ hIB

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem pow_length_le_mul_ofDigits {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : l.getLast hl ≠ 0) :
    (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Proof state:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ 0 < l.getLast hl

Tactic:
rwa [pos_iff_ne_zero]

Result:
no goals

Proof state:
case h
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
convert Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1

Result:
case h.e'_3
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0

Proof state:
case h.e'_3
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0

Tactic:
rw [Nat.mul_one]

Result:
no goals

Proof state:
case h
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
refine le_trans ?_ (Nat.le_add_left _ _)

Result:
case h
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Proof state:
case h
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]

Result:
case h
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Proof state:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [l.getLast hl])

Tactic:
simp only [List.length_append, List.length, zero_add, List.length_dropLast, ofDigits_append,
  List.length_dropLast, ofDigits_singleton, add_comm (l.length - 1), pow_add, pow_one]

Result:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) * (b + 2) ^ (l.length - 1) ≤ (b + 2) * (ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl)

Proof state:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Tactic:
rw [← List.dropLast_append_getLast hl]

Result:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [l.getLast hl])

Proof state:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) * (b + 2) ^ (l.length - 1) ≤ (b + 2) * (ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl)

Tactic:
apply Nat.mul_le_mul_left

Result:
case h
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl
-- Mathlib/Data/PNat/Basic.lean
theorem le_of_dvd {m n : ℕ+} : m ∣ n → m ≤ n

Proof state:
m n : ℕ+
h : n.mod m = m
⊢ m ≤ n

Tactic:
rw [← h]

Result:
m n : ℕ+
h : n.mod m = m
⊢ n.mod m ≤ n

Proof state:
m n : ℕ+
⊢ n.mod m = m → m ≤ n

Tactic:
intro h

Result:
m n : ℕ+
h : n.mod m = m
⊢ m ≤ n

Proof state:
m n : ℕ+
h : n.mod m = m
⊢ n.mod m ≤ n

Tactic:
apply (mod_le n m).left

Result:
no goals

Proof state:
m n : ℕ+
⊢ m ∣ n → m ≤ n

Tactic:
rw [dvd_iff']

Result:
m n : ℕ+
⊢ n.mod m = m → m ≤ n
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem MeasureTheory.volume_sum_rpow_lt [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) :
    volume {x : ι → ℝ | (∑ i, |x i| ^ p) ^ (1 / p) < r} = (.ofReal r) ^ card ι *
      .ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (card ι / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
⊢ {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ∅

Tactic:
ext x

Result:
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℝ
⊢ x ∈ {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} ↔ x ∈ ∅

Proof state:
case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p
h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)
hr : r ≤ 0
x : ι → ℝ
hx : x ∈ {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r}
⊢ x ∈ ∅

Tactic:
exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_flatten (xs : List (List α)) (p : α → Bool) :
    xs.flatten.find? p = xs.findSome? (·.find? p)

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ find? p [].flatten = findSome? (fun x => find? p x) []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List (List α)
p : α → Bool
⊢ find? p xs.flatten = findSome? (fun x => find? p x) xs

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp only [flatten_cons, find?_append, findSome?_cons, ih]
  split <;> simp [*]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : List α
xs : List (List α)
ih : find? p xs.flatten = findSome? (fun x => find? p x) xs
⊢ (find? p x).or (findSome? (fun x => find? p x) xs) =
    match find? p x with
    | some b => some b
    | none => findSome? (fun x => find? p x) xs

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : List α
xs : List (List α)
ih : find? p xs.flatten = findSome? (fun x => find? p x) xs
⊢ find? p (x :: xs).flatten = findSome? (fun x => find? p x) (x :: xs)

Tactic:
simp only [flatten_cons, find?_append, findSome?_cons, ih]

Result:
case cons
α : Type u_1
p : α → Bool
x : List α
xs : List (List α)
ih : find? p xs.flatten = findSome? (fun x => find? p x) xs
⊢ (find? p x).or (findSome? (fun x => find? p x) xs) =
    match find? p x with
    | some b => some b
    | none => findSome? (fun x => find? p x) xs
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_X_pow (n : ℕ) : eraseLead (X ^ n : R[X]) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).eraseLead = 0

Tactic:
rw [X_pow_eq_monomial, eraseLead_monomial]

Result:
no goals
-- Mathlib/Data/ZMod/Defs.lean
theorem left_distrib_aux (n : ℕ) : ∀ a b c : Fin n, a * (b + c) = a * b + a * c :=
  fun ⟨a, _⟩ ⟨b, _⟩ ⟨c, _⟩ =>
  Fin.eq_of_val_eq <|
    calc
      a * ((b + c) % n) ≡ a * (b + c) [MOD n] := (Nat.mod_modEq _ _).mul_left _
      _ ≡ a * b + a * c [MOD n]

Proof state:
n : ℕ
x✝² x✝¹ x✝ : Fin n
a : ℕ
isLt✝² : a < n
b : ℕ
isLt✝¹ : b < n
c : ℕ
isLt✝ : c < n
⊢ a * (b + c) ≡ a * b + a * c [MOD n]

Tactic:
rw [mul_add]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toNNReal_toReal_eq (z : ℝ≥0∞) : z.toReal.toNNReal = z.toNNReal

Proof state:
z : ℝ≥0∞
⊢ z.toReal.toNNReal = z.toNNReal

Tactic:
ext

Result:
case a
z : ℝ≥0∞
⊢ ↑z.toReal.toNNReal = ↑z.toNNReal

Proof state:
case a
z : ℝ≥0∞
⊢ ↑z.toReal.toNNReal = ↑z.toNNReal

Tactic:
simp [coe_toNNReal_eq_toReal]

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_sub_goldConj : φ - ψ = √5

Proof state:
⊢ φ - ψ = √5

Tactic:
ring

Result:
no goals
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
    {G : Type*} [LinearOrderedAddCommGroup G] [Nontrivial G] {g : G} :
    Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Nonempty (G ≃+o ℤ)

Proof state:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
⊢ ∀ a ∈ {x | g ≤ x}, ∀ b ∈ {x | g ≤ x}, a < b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x - g) a b

Tactic:
try intro

Result:
case refine_4
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝ : G
⊢ a✝ ∈ {x | g ≤ x} → ∀ b ∈ {x | g ≤ x}, a✝ < b → Function.onFun (fun x1 x2 => x1 < x2) (fun x => x - g) a✝ b