harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_le_iff_le_log {b x c : Ordinal} (hb : 1 < b) (hx : x ≠ 0) :
    b ^ c ≤ x ↔ c ≤ log b x

Proof state:
case mp.h
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : b ^ c ≤ x
hn : log b x < c
⊢ False

Tactic:
apply (lt_opow_succ_log_self hb x).not_le <|
  ((opow_le_opow_iff_right hb).2 <| succ_le_of_lt hn).trans h

Result:
no goals

Proof state:
case mp
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : b ^ c ≤ x
⊢ c ≤ log b x

Tactic:
apply le_of_not_lt

Result:
case mp.h
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : b ^ c ≤ x
⊢ ¬log b x < c

Proof state:
case mp.h
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : b ^ c ≤ x
⊢ ¬log b x < c

Tactic:
intro hn

Result:
case mp.h
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : b ^ c ≤ x
hn : log b x < c
⊢ False

Proof state:
case mpr
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : c ≤ log b x
⊢ b ^ c ≤ x

Tactic:
exact ((opow_le_opow_iff_right hb).2 h).trans <| opow_log_le_self b hx

Result:
no goals

Proof state:
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
constructor <;>
intro h

Result:
case mp
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : b ^ c ≤ x
⊢ c ≤ log b x

case mpr
b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
h : c ≤ log b x
⊢ b ^ c ≤ x
-- Mathlib/RingTheory/Support.lean
/-- Given an exact sequence `0 → M → N → P → 0` of `R`-modules, `Supp N = Supp M ∪ Supp P`. -/
lemma Module.support_of_exact (h : Function.Exact f g)
    (hf : Function.Injective f) (hg : Function.Surjective g) :
    Module.support R N = Module.support R M ∪ Module.support R P

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
exact ⟨_, x.asIdeal.primeCompl.mul_mem hs hr, by rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
⊢ x ∉ support R M ∪ support R P → x ∉ support R N

Tactic:
simp only [Set.mem_union, not_or, and_imp, not_mem_support_iff']

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
⊢ (∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0) →
    (∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0) → ∀ (m : N), ∃ r ∉ x.asIdeal, r • m = 0

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
obtain ⟨s, hs, e₁⟩ := H₁ m'

Result:
case intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
s : R
hs : s ∉ x.asIdeal
e₁ : s • m' = 0
⊢ ∃ r ∉ x.asIdeal, r • m = 0
-- Mathlib/Order/PFilter.lean
theorem principal_le_principal_iff {p q : P} : principal q ≤ principal p ↔ p ≤ q

Proof state:
P : Type u_1
inst✝ : Preorder P
p q : P
⊢ principal q ≤ principal p ↔ p ≤ q

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_le_of_forall_ne (h₁ : ∀ a' < a, a' + b ≠ c) (h₂ : ∀ b' < b, a + b' ≠ c) :
    a + b ≤ c

Proof state:
a b c : Nimber
h₁ : ∀ a' < a, a' + b ≠ c
h₂ : ∀ b' < b, a + b' ≠ c
h : c < a + b
this : (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c
⊢ False

Tactic:
tauto

Result:
no goals

Proof state:
a b c : Nimber
h₁ : ∀ a' < a, a' + b ≠ c
h₂ : ∀ b' < b, a + b' ≠ c
h : c < a + b
⊢ False

Tactic:
have := exists_of_lt_add h

Result:
a b c : Nimber
h₁ : ∀ a' < a, a' + b ≠ c
h₂ : ∀ b' < b, a + b' ≠ c
h : c < a + b
this : (∃ a' < a, a' + b = c) ∨ ∃ b' < b, a + b' = c
⊢ False

Proof state:
a b c : Nimber
h₁ : ∀ a' < a, a' + b ≠ c
h₂ : ∀ b' < b, a + b' ≠ c
⊢ a + b ≤ c

Tactic:
by_contra! h

Result:
a b c : Nimber
h₁ : ∀ a' < a, a' + b ≠ c
h₂ : ∀ b' < b, a + b' ≠ c
h : c < a + b
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem sum_eq_sum_toList [Add α] [Zero α] (as : Array α) : as.toList.sum = as.sum

Proof state:
α : Type u_1
inst✝¹ : Add α
inst✝ : Zero α
as : Array α
⊢ as.toList.sum = as.sum

Tactic:
cases as

Result:
case mk
α : Type u_1
inst✝¹ : Add α
inst✝ : Zero α
toList✝ : List α
⊢ { toList := toList✝ }.toList.sum = { toList := toList✝ }.sum

Proof state:
case mk
α : Type u_1
inst✝¹ : Add α
inst✝ : Zero α
toList✝ : List α
⊢ { toList := toList✝ }.toList.sum = { toList := toList✝ }.sum

Tactic:
simp [Array.sum, List.sum]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sup_equiv_sup {a₁ b₁ a₂ b₂ : CauSeq α abs} (ha : a₁ ≈ a₂) (hb : b₁ ≈ b₂) :
    a₁ ⊔ b₁ ≈ a₂ ⊔ b₂

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε

Tactic:
obtain ⟨ai, hai⟩ := ha ε ε0

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε

Proof state:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε

Tactic:
exact
  ⟨ai ⊔ bi, fun i hi =>
    (abs_max_sub_max_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
      (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε

Tactic:
obtain ⟨bi, hbi⟩ := hb ε ε0

Result:
case intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
⊢ a₁ ⊔ b₁ ≈ a₂ ⊔ b₂

Tactic:
intro ε ε0

Result:
α : Type u_1
inst✝ : LinearOrderedField α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε
-- Mathlib/Analysis/Meromorphic/Basic.lean
theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜}
    (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, AnalyticAt 𝕜 f y

Proof state:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : y ∈ {x}ᶜ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y

Tactic:
rw [Set.mem_compl_iff, Set.mem_singleton_iff] at hy

Result:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y

Proof state:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y

Tactic:
have := ((analyticAt_id (𝕜 := 𝕜).sub analyticAt_const).pow n).inv
  (pow_ne_zero _ (sub_ne_zero_of_ne hy))

Result:
case intro.refine_2.hp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 (fun x_1 => (_root_.id - fun x_2 => x) x_1 ^ n)⁻¹ y
⊢ AnalyticAt 𝕜 f y

Proof state:
case intro.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : 𝕜 → E
x : 𝕜
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z => (z - x) ^ n • f z) y
⊢ 𝓝[≠] x ≤ 𝓝 x

Tactic:
simp [nhdsWithin]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_rightAngleRotationAux₁_left (x y : E) : ⟪o.rightAngleRotationAux₁ x, y⟫ = ω x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ((InnerProductSpace.toDual ℝ E).symm (LinearMap.toContinuousLinearMap.symm.symm (o.areaForm x))) y =
    (o.areaForm x) y

Tactic:
rw [InnerProductSpace.toDual_symm_apply]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (LinearMap.toContinuousLinearMap.symm.symm (o.areaForm x)) y = (o.areaForm x) y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (LinearMap.toContinuousLinearMap.symm.symm (o.areaForm x)) y = (o.areaForm x) y

Tactic:
norm_cast

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (o.rightAngleRotationAux₁ x) y = (o.areaForm x) y

Tactic:
simp only [rightAngleRotationAux₁, LinearEquiv.trans_symm, LinearIsometryEquiv.toLinearEquiv_symm,
  LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply,
  LinearIsometryEquiv.coe_toLinearEquiv]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ((InnerProductSpace.toDual ℝ E).symm (LinearMap.toContinuousLinearMap.symm.symm (o.areaForm x))) y =
    (o.areaForm x) y
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
/-- Given a measurable embedding to a Borel space which is also a topological embedding, then the
source space is also a Borel space. -/
lemma MeasurableEmbedding.borelSpace {α β : Type*} [MeasurableSpace α] [TopologicalSpace α]
    [MeasurableSpace β] [TopologicalSpace β] [hβ : BorelSpace β] {e : α → β}
    (h'e : MeasurableEmbedding e) (h''e : IsInducing e) :
    BorelSpace α

Proof state:
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ MeasurableSpace.comap e (borel β) = inst✝³

Tactic:
simpa [hβ.measurable_eq] using h'e.comap_eq

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ BorelSpace α

Tactic:
constructor

Result:
case measurable_eq
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ inst✝³ = borel α

Proof state:
case measurable_eq
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst✝³
⊢ inst✝³ = borel α

Tactic:
rw [← this, ← borel_comap, h''e.eq_induced]

Result:
no goals

Proof state:
case measurable_eq
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ inst✝³ = borel α

Tactic:
have : MeasurableSpace.comap e (borel β) = ‹_› := by simpa [hβ.measurable_eq] using h'e.comap_eq

Result:
case measurable_eq
α : Type u_6
β : Type u_7
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace β
inst✝ : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst✝³
⊢ inst✝³ = borel α
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_ext [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l)
    (hl' : DistinctKeys l') (h : ∀ a, getEntry? a l = getEntry? a l') : Perm l l'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
⊢ (⟨k, v⟩ :: t).Perm l'

Tactic:
have hl'k₂ : containsKey k l' := by
  rw [containsKey_eq_isSome_getEntry?, hl'k₁, Option.isSome_some]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
⊢ (⟨k, v⟩ :: t).Perm l'
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
theorem smul [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : μ ≪ ν) (c : R) :
    c • μ ≪ c • ν

Proof state:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : (c • ν) s = 0
⊢ (c • μ) s = 0

Tactic:
rw [smul_apply, ← smul_one_smul ℝ≥0∞, smul_eq_mul, mul_eq_zero] at hνs ⊢

Result:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : c • 1 = 0 ∨ ν s = 0
⊢ c • 1 = 0 ∨ μ s = 0

Proof state:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : c • 1 = 0 ∨ ν s = 0
⊢ c • 1 = 0 ∨ μ s = 0

Tactic:
exact hνs.imp_right fun hs ↦ h hs

Result:
no goals

Proof state:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
⊢ c • μ ≪ c • ν

Tactic:
intro s hνs

Result:
α : Type u_1
R : Type u_5
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : μ ≪ ν
c : R
s : Set α
hνs : (c • ν) s = 0
⊢ (c • μ) s = 0
-- Mathlib/Algebra/CharP/Algebra.lean
theorem charZero_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A]
    {f : R →+* A} (h : Function.Injective f) [CharZero R] : CharZero A where
  cast_injective _ _ _ := CharZero.cast_injective <| h <| by simpa only [map_natCast f]

Proof state:
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
x✝² x✝¹ : ℕ
x✝ : ↑x✝² = ↑x✝¹
⊢ f ↑x✝² = f ↑x✝¹

Tactic:
simpa only [map_natCast f]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem ofEven_comp_toEven : (ofEven Q).comp (toEven Q) = AlgHom.id R _ :=
  CliffordAlgebra.hom_ext <|
    LinearMap.ext fun m =>
      calc
        ofEven Q (toEven Q (ι Q m)) = ofEven Q ⟨_, (toEven Q (ι Q m)).prop⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0) = (ι Q) m

Tactic:
rw [map_one, map_zero, map_zero, sub_zero, zero_add, one_mul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (ofEven Q) ((toEven Q) ((ι Q) m)) = (ofEven Q) ⟨↑((toEven Q) ((ι Q) m)), ⋯⟩

Tactic:
rw [Subtype.coe_eta]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (ofEven Q) ⟨↑((toEven Q) ((ι Q) m)), ⋯⟩ =
    ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0)

Tactic:
simp_rw [toEven_ι]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (ofEven Q) ⟨e0 Q * (v Q) m, ⋯⟩ =
    ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (ofEven Q) ⟨e0 Q * (v Q) m, ⋯⟩ =
    ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0)

Tactic:
exact ofEven_ι Q _ _

Result:
no goals
-- Mathlib/Data/Set/Monotone.lean
theorem _root_.MonotoneOn.congr (h₁ : MonotoneOn f₁ s) (h : s.EqOn f₁ f₂) : MonotoneOn f₂ s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₂ a ≤ f₂ b

Tactic:
rw [← h ha, ← h hb]

Result:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
⊢ MonotoneOn f₂ s

Tactic:
intro a ha b hb hab

Result:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₂ a ≤ f₂ b

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₁ a ≤ f₁ b

Tactic:
exact h₁ ha hb hab

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem interpolate_empty : interpolate ∅ v r = 0

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
⊢ (interpolate ∅ v) r = 0

Tactic:
rw [interpolate_apply, sum_empty]

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem rotation_trans (a b : Circle) : (rotation a).trans (rotation b) = rotation (b * a)

Proof state:
a b : Circle
⊢ (rotation a).trans (rotation b) = rotation (b * a)

Tactic:
ext1

Result:
case h
a b : Circle
x✝ : ℂ
⊢ ((rotation a).trans (rotation b)) x✝ = (rotation (b * a)) x✝

Proof state:
case h
a b : Circle
x✝ : ℂ
⊢ ((rotation a).trans (rotation b)) x✝ = (rotation (b * a)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/FermatPsp.lean
theorem bp_helper {b p : ℕ} (hb : 0 < b) (hp : 1 ≤ p) :
    b ^ (2 * p) - 1 - (b ^ 2 - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b) :=
  have hi_bsquared : 1 ≤ b ^ 2 := Nat.one_le_pow _ _ hb
  calc
    b ^ (2 * p) - 1 - (b ^ 2 - 1) = b ^ (2 * p) - (1 + (b ^ 2 - 1))

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p) ^ 2 - b ^ 2 = (b ^ p + b) * (b ^ p - b)

Tactic:
rw [Nat.sq_sub_sq]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - 1 - (b ^ 2 - 1) = b ^ (2 * p) - (1 + (b ^ 2 - 1))

Tactic:
rw [Nat.sub_sub]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p + b) * (b ^ p - b) = (b ^ p - b) * (b ^ p + b)

Tactic:
rw [mul_comm]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ (p - 1 + 1) - b) * (b ^ p + b)

Tactic:
rw [Nat.sub_add_cancel hp]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - b ^ 2 = b ^ (p * 2) - b ^ 2

Tactic:
rw [mul_comm]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b * b ^ (p - 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b * 1) * (b ^ p + b)

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - (1 + (b ^ 2 - 1)) = b ^ (2 * p) - (1 + b ^ 2 - 1)

Tactic:
rw [Nat.add_sub_assoc hi_bsquared]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b * b ^ (p - 1) - b * 1) * (b ^ p + b) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
rw [Nat.mul_sub_left_distrib]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (p * 2) - b ^ 2 = (b ^ p) ^ 2 - b ^ 2

Tactic:
rw [pow_mul]

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ (p - 1 + 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)

Tactic:
rw [pow_succ']

Result:
no goals

Proof state:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - (1 + b ^ 2 - 1) = b ^ (2 * p) - b ^ 2

Tactic:
rw [Nat.add_sub_cancel_left]

Result:
no goals