harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineIndependent.injective [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) : Function.Injective p

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent k fun i => p ↑i -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ False

Tactic:
refine ha.ne_zero ⟨i, hij'⟩ (vsub_eq_zero_iff_eq.mpr ?_)

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent k fun i => p ↑i -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ p ↑⟨i, hij'⟩ = p j

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent k fun i => p ↑i -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ p ↑⟨i, hij'⟩ = p j

Tactic:
simp_all only [ne_eq]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i j : ι
hij : p i = p j
⊢ i = j

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub _ _ j] at ha

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent k fun i => p ↑i -ᵥ p j
hij : p i = p j
⊢ i = j

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
⊢ Injective p

Tactic:
intro i j hij

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i j : ι
hij : p i = p j
⊢ i = j

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent k fun i => p ↑i -ᵥ p j
hij : p i = p j
⊢ i = j

Tactic:
by_contra hij'

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
i j : ι
ha : LinearIndependent k fun i => p ↑i -ᵥ p j
hij : p i = p j
hij' : ¬i = j
⊢ False
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_nat {b c k : ℕ} {d e : R} (_ : b = c * k) (_ : a ^ c = d) (_ : d ^ k = e) :
    (a : R) ^ b = e

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
b c k : ℕ
d e : R
x✝² : b = c * k
x✝¹ : a ^ c = d
x✝ : d ^ k = e
⊢ a ^ b = e

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a : R
c k : ℕ
⊢ a ^ (c * k) = (a ^ c) ^ k

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
c k : ℕ
⊢ a ^ (c * k) = (a ^ c) ^ k

Tactic:
simp [pow_mul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem sum_toFinset_count_eq_length [DecidableEq α] (l : List α) :
    ∑ a ∈ l.toFinset, l.count a = l.length

Proof state:
α : Type u_3
inst✝ : DecidableEq α
l : List α
⊢ ∑ a ∈ l.toFinset, count a l = l.length

Tactic:
simpa [List.map_const'] using (Finset.sum_list_map_count l fun _ => (1 : ℕ)).symm

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem coeff_apply (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) :
    h.coeff z i = if hi : i < natDegree f then h.basis.repr z ⟨i, hi⟩ else 0

Proof state:
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : i < f.natDegree
⊢ h.coeff z i = (h.basis.repr z) ⟨i, hi⟩

Tactic:
exact h.coeff_apply_lt z i hi

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
⊢ h.coeff z i = if hi : i < f.natDegree then (h.basis.repr z) ⟨i, hi⟩ else 0

Tactic:
split_ifs with hi

Result:
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : i < f.natDegree
⊢ h.coeff z i = (h.basis.repr z) ⟨i, hi⟩

case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : ¬i < f.natDegree
⊢ h.coeff z i = 0

Proof state:
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : ¬i < f.natDegree
⊢ h.coeff z i = 0

Tactic:
exact h.coeff_apply_le z i (le_of_not_lt hi)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem B_mem_nhdsGT {K : Set F} {r s ε x : ℝ} (hx : x ∈ B f K r s ε) :
    B f K r s ε ∈ 𝓝[>] x

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
⊢ ∃ L ∈ K, x ∈ A f L r ε ∧ x ∈ A f L s ε

Tactic:
simpa only [B, mem_iUnion, mem_inter_iff, exists_prop] using hx

Result:
no goals

Proof state:
case intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
⊢ B f K r s ε ∈ 𝓝[>] x

Tactic:
filter_upwards [A_mem_nhdsGT hL₁, A_mem_nhdsGT hL₂] with y hy₁ hy₂

Result:
case h
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
y : ℝ
hy₁ : y ∈ A f L r ε
hy₂ : y ∈ A f L s ε
⊢ y ∈ B f K r s ε

Proof state:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
⊢ B f K r s ε ∈ 𝓝[>] x

Tactic:
obtain ⟨L, LK, hL₁, hL₂⟩ : ∃ L : F, L ∈ K ∧ x ∈ A f L r ε ∧ x ∈ A f L s ε := by
  simpa only [B, mem_iUnion, mem_inter_iff, exists_prop] using hx

Result:
case intro.intro.intro
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
⊢ B f K r s ε ∈ 𝓝[>] x

Proof state:
case h
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
y : ℝ
hy₁ : y ∈ A f L r ε
hy₂ : y ∈ A f L s ε
⊢ y ∈ B f K r s ε

Tactic:
simp only [B, mem_iUnion, mem_inter_iff, exists_prop]

Result:
case h
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
y : ℝ
hy₁ : y ∈ A f L r ε
hy₂ : y ∈ A f L s ε
⊢ ∃ i ∈ K, y ∈ A f i r ε ∧ y ∈ A f i s ε

Proof state:
case h
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
r s ε x : ℝ
hx : x ∈ B f K r s ε
L : F
LK : L ∈ K
hL₁ : x ∈ A f L r ε
hL₂ : x ∈ A f L s ε
y : ℝ
hy₁ : y ∈ A f L r ε
hy₂ : y ∈ A f L s ε
⊢ ∃ i ∈ K, y ∈ A f i r ε ∧ y ∈ A f i s ε

Tactic:
exact ⟨L, LK, hy₁, hy₂⟩

Result:
no goals
-- Mathlib/RingTheory/Ideal/Height.lean
/-- For a prime ideal, its height equals its prime height. -/
lemma Ideal.height_eq_primeHeight [I.IsPrime] : I.height = I.primeHeight

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ⨅ J, ⨅ (x : J ∈ {I}), Order.height { asIdeal := J, isPrime := ⋯ } = Order.height { asIdeal := I, isPrime := inst✝ }

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.height = I.primeHeight

Tactic:
unfold height primeHeight

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), Order.height { asIdeal := J, isPrime := ⋯ } =
    Order.height { asIdeal := I, isPrime := inst✝ }

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), Order.height { asIdeal := J, isPrime := ⋯ } =
    Order.height { asIdeal := I, isPrime := inst✝ }

Tactic:
simp_rw [Ideal.minimalPrimes_eq_subsingleton_self]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ⨅ J, ⨅ (x : J ∈ {I}), Order.height { asIdeal := J, isPrime := ⋯ } = Order.height { asIdeal := I, isPrime := inst✝ }
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_differentiable_iff {f : G → E} : Differentiable 𝕜 (iso ∘ f) ↔ Differentiable 𝕜 f

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
⊢ Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f

Tactic:
rw [← differentiableOn_univ, ← differentiableOn_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
⊢ DifferentiableOn 𝕜 (⇑iso ∘ f) univ ↔ DifferentiableOn 𝕜 f univ

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
⊢ DifferentiableOn 𝕜 (⇑iso ∘ f) univ ↔ DifferentiableOn 𝕜 f univ

Tactic:
exact iso.comp_differentiableOn_iff

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem supermartingale_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f)
    (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i, μ[f (i + 1)|𝒢 i] ≤ᵐ[μ] f i) :
    Supermartingale f 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i
⊢ Supermartingale f 𝒢 μ

Tactic:
rw [← neg_neg f]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i
⊢ Supermartingale (- -f) 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
refine (submartingale_nat hadp.neg (fun i => (hint i).neg) fun i =>
  EventuallyLE.trans ?_ (condExp_neg ..).symm.le).neg

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i
i : ℕ
⊢ (-f) i ≤ᶠ[ae μ] -μ[f (i + 1)|↑𝒢 i]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i
i : ℕ
⊢ (-f) i ≤ᶠ[ae μ] -μ[f (i + 1)|↑𝒢 i]

Tactic:
filter_upwards [hf i] with x hx using neg_le_neg hx

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
lemma log_inv {x : ℝ≥0∞} : log x⁻¹ = - log x

Proof state:
x : ℝ≥0∞
⊢ x⁻¹.log = -x.log

Tactic:
simp [← rpow_neg_one, log_rpow]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem _root_.IsClosed.mem_iff_infDist_zero (h : IsClosed s) (hs : s.Nonempty) :
    x ∈ s ↔ infDist x s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : IsClosed s
hs : s.Nonempty
⊢ x ∈ s ↔ infDist x s = 0

Tactic:
rw [← mem_closure_iff_infDist_zero hs, h.closure_eq]

Result:
no goals
-- Mathlib/Probability/Martingale/OptionalSampling.lean
theorem stoppedValue_ae_eq_condExp_of_le_of_countable_range (h : Martingale f ℱ μ)
    (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ x, τ x ≤ n)
    (hτ_countable_range : (Set.range τ).Countable) (hσ_countable_range : (Set.range σ).Countable)
    [SigmaFinite (μ.trim (hσ.measurableSpace_le_of_le fun x => (hσ_le_τ x).trans (hτ_le x)))] :
    stoppedValue f σ =ᵐ[μ] μ[stoppedValue f τ|hσ.measurableSpace]

Proof state:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]

Tactic:
have : SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le)) :=
  sigmaFiniteTrim_mono _ (IsStoppingTime.measurableSpace_mono hσ hτ hσ_le_τ)

Result:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
ι : Type u_3
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : SigmaFiniteFiltration μ ℱ
τ σ : Ω → ι
f : ι → Ω → E
n : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]
-- Mathlib/Data/Ordmap/Ordset.lean
theorem raised_iff {n m} : Raised n m ↔ n ≤ m ∧ m ≤ n + 1

Proof state:
case mp.inl
m : ℕ
⊢ m ≤ m ∧ m ≤ m + 1

Tactic:
exact ⟨le_rfl, Nat.le_succ _⟩

Result:
no goals

Proof state:
case mpr.intro.inl
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n

Tactic:
exact Or.inl rfl

Result:
no goals

Proof state:
case mpr.intro
n m : ℕ
h₁ : n ≤ m
h₂ : m ≤ n + 1
⊢ Raised n m

Tactic:
rcases eq_or_lt_of_le h₁ with (rfl | h₁)

Result:
case mpr.intro.inl
n : ℕ
h₁ : n ≤ n
h₂ : n ≤ n + 1
⊢ Raised n n

case mpr.intro.inr
n m : ℕ
h₁✝ : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m

Proof state:
case mp
n m : ℕ
⊢ Raised n m → n ≤ m ∧ m ≤ n + 1

Tactic:
rintro (rfl | rfl)

Result:
case mp.inl
m : ℕ
⊢ m ≤ m ∧ m ≤ m + 1

case mp.inr
n : ℕ
⊢ n ≤ n + 1 ∧ n + 1 ≤ n + 1

Proof state:
case mp.inr
n : ℕ
⊢ n ≤ n + 1 ∧ n + 1 ≤ n + 1

Tactic:
exact ⟨Nat.le_succ _, le_rfl⟩

Result:
no goals

Proof state:
n m : ℕ
⊢ Raised n m ↔ n ≤ m ∧ m ≤ n + 1

Tactic:
constructor

Result:
case mp
n m : ℕ
⊢ Raised n m → n ≤ m ∧ m ≤ n + 1

case mpr
n m : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 → Raised n m

Proof state:
case mpr
n m : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 → Raised n m

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
n m : ℕ
h₁ : n ≤ m
h₂ : m ≤ n + 1
⊢ Raised n m

Proof state:
case mpr.intro.inr
n m : ℕ
h₁✝ : n ≤ m
h₂ : m ≤ n + 1
h₁ : n < m
⊢ Raised n m

Tactic:
exact Or.inr (le_antisymm h₂ h₁)

Result:
no goals
-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
private lemma weaken_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : #(A * A) < 2 * #A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < 2 * ↑(#A)

Tactic:
linarith only [h]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ #(A * A) < 2 * #A

Tactic:
rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < 2 * ↑(#A)
-- Mathlib/Data/Int/CardIntervalMod.lean
theorem Ico_filter_dvd_card : #{x ∈ Ico a b | r ∣ x} = max (⌈b / (r : ℚ)⌉ - ⌈a / (r : ℚ)⌉) 0

Proof state:
a b r : ℤ
hr : 0 < r
⊢ ↑(#(filter (fun x => r ∣ x) (Ico a b))) = (⌈↑b / ↑r⌉ - ⌈↑a / ↑r⌉) ⊔ 0

Tactic:
rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunction_succ (f : ℕ → Bool) (h1 : 0 ≤ c) (h2 : c < 1) :
    cantorFunction c f = cond (f 0) 1 0 + c * cantorFunction c fun n => f (n + 1)

Proof state:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunction c f = (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)

Tactic:
rw [cantorFunction, tsum_eq_zero_add (summable_cantor_function f h1 h2)]

Result:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunctionAux c f 0 + ∑' (b : ℕ), cantorFunctionAux c f (b + 1) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)

Proof state:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ (bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n => f (n + 1)) x =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)

Tactic:
rfl

Result:
no goals

Proof state:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunctionAux c f 0 + ∑' (b : ℕ), cantorFunctionAux c f (b + 1) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)

Tactic:
rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, _root_.pow_zero]

Result:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ (bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n => f (n + 1)) x =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_top_right : relfinrank A ⊤ = finrank A E

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ A.relfinrank ⊤ = finrank (↥A) E

Tactic:
simp [relfinrank_eq_toNat_relrank, finrank]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem smul_integral_comp_add_mul (c d) :
    (c • ∫ x in a..b, f (d + c * x)) = ∫ x in d + c * a..d + c * b, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c • ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_add_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_nz_of_isRat_neg {n : ℤ} : (NormNum.IsRat e n d) → (decide (n / d < (0 : ℚ)))
    → (decide ((-1 : ℚ) < n / d)) → (Real.log (e : ℝ) ≠ 0)
  | ⟨inv, eq⟩, h₁, h₂ => by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have h₁' : (n : ℝ) / d < 0

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log e ≠ 0

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log (↑n / ↑d) ≠ 0

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ -1 < ↑n / ↑d

Tactic:
exact_mod_cast of_decide_eq_true h₂

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
h₂' : -1 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
exact ne_of_lt <| Real.log_neg_of_lt_zero h₁' h₂'

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
have h₁' : (n : ℝ) / d < 0 := by exact_mod_cast of_decide_eq_true h₁

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ Real.log (↑n / ↑d) ≠ 0

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
⊢ ↑n / ↑d < 0

Tactic:
exact_mod_cast of_decide_eq_true h₁

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
⊢ Real.log (↑n / ↑d) ≠ 0

Tactic:
have h₂' : -1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h₂

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h₁ : decide (↑n / ↑d < 0) = true
h₂ : decide (-1 < ↑n / ↑d) = true
h₁' : ↑n / ↑d < 0
h₂' : -1 < ↑n / ↑d
⊢ Real.log (↑n / ↑d) ≠ 0
-- Mathlib/Data/Sigma/Basic.lean
theorem _root_.Function.eq_of_sigmaMk_comp {γ : Type*} [Nonempty γ]
    {a b : α} {f : γ → β a} {g : γ → β b} (h : Sigma.mk a ∘ f = Sigma.mk b ∘ g) :
    a = b ∧ HEq f g

Proof state:
case intro
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
i : γ
⊢ a = b ∧ HEq f g

Tactic:
obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)

Result:
case intro
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ a = a ∧ HEq f g

Proof state:
case intro
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ a = a ∧ HEq f g

Tactic:
simpa [funext_iff] using h

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
⊢ a = b ∧ HEq f g

Tactic:
rcases ‹Nonempty γ› with ⟨i⟩

Result:
case intro
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
i : γ
⊢ a = b ∧ HEq f g
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalkPushforward_germ (f : X ⟶ Y) (F : X.Presheaf C) (U : Opens Y)
    (x : X) (hx : f x ∈ U) :
      (f _* F).germ U (f x) hx ≫ F.stalkPushforward C f x = F.germ ((Opens.map f).obj U) x hx

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
U : Opens ↑Y
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ U
⊢ ((pushforward C f).obj F).germ U ((ConcreteCategory.hom f) x) hx ≫ stalkPushforward C f F x =
    F.germ ((Opens.map f).obj U) x hx

Tactic:
simp [germ, stalkPushforward]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem intCast_eq (z1 z2 : ℤ) : (z1 : ℤ_[p]) = z2 ↔ z1 = z2

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ
⊢ ↑z1 = ↑z2 ↔ z1 = z2

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_subtype_compl [Fintype α] (p : α → Prop) [Fintype { x // p x }]
    [Fintype { x // ¬p x }] :
    Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x }

Proof state:
case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
intro

Result:
case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ {x | p x}ᶜ.toFinset ↔ ¬p x✝

Proof state:
case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
x✝ : α
⊢ x✝ ∈ {x | p x}ᶜ.toFinset ↔ ¬p x✝

Tactic:
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.sub_eq' [AddCommGroup α] (h : Periodic f c) : f (c - x) = f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : AddCommGroup α
h : Periodic f c
⊢ f (c - x) = f (-x)

Tactic:
simpa only [sub_eq_neg_add] using h (-x)

Result:
no goals