harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_filterMap {f : α → Option β} {l : List α} {b : β} :
    b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
b : β
⊢ b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b

Tactic:
induction l <;> simp [filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ filterMap f tail✝ ↔ ∃ a, a ∈ tail✝ ∧ f a = some b
⊢ (b ∈
      match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) ↔
    f head✝ = some b ∨ ∃ a, a ∈ tail✝ ∧ f a = some b

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : b ∈ filterMap f tail✝ ↔ ∃ a, a ∈ tail✝ ∧ f a = some b
⊢ (b ∈
      match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) ↔
    f head✝ = some b ∨ ∃ a, a ∈ tail✝ ∧ f a = some b

Tactic:
split <;> simp [*, eq_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_over_two_pow : ∀ n : ℕ, cos (π / 2 ^ (n + 1)) = sqrtTwoAddSeries 0 n / 2
  | 0 => by simp
  | n + 1 => by
    have A : (1 : ℝ) < 2 ^ (n + 1) := one_lt_pow₀ one_lt_two n.succ_ne_zero
    have B : π / 2 ^ (n + 1) < π := div_lt_self pi_pos A
    have C : 0 < π / 2 ^ (n + 1)

Proof state:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
⊢ 0 < π / 2 ^ (n + 1)

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
have C : 0 < π / 2 ^ (n + 1) := by positivity

Result:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Proof state:
⊢ cos (π / 2 ^ (0 + 1)) = sqrtTwoAddSeries 0 0 / 2

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
A : 1 < 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
have B : π / 2 ^ (n + 1) < π := div_lt_self pi_pos A

Result:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Proof state:
n : ℕ
A : 1 < 2 ^ (n + 1)
B : π / 2 ^ (n + 1) < π
C : 0 < π / 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
  add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self] <;>
  linarith [sqrtTwoAddSeries_nonneg le_rfl n]

Result:
no goals

Proof state:
n : ℕ
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
have A : (1 : ℝ) < 2 ^ (n + 1) := one_lt_pow₀ one_lt_two n.succ_ne_zero

Result:
n : ℕ
A : 1 < 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffOn_zero_iff :
    ContMDiffOn I I' 0 f s ↔ ContinuousOn f s

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
h : ContinuousOn f s
x : M
y : M'
⊢ ContinuousOn (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
apply (continuousOn_extChartAt _).comp

Result:
case hf
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
h : ContinuousOn f s
x : M
y : M'
⊢ ContinuousOn (f ∘ ↑(extChartAt I x).symm)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
h : ContinuousOn f s
x : M
y : M'
⊢ MapsTo (f ∘ ↑(extChartAt I x).symm)
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) (extChartAt I' y).source
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem map_subtype {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.map f = l.unattach.map g

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
l : Array { x // p x }
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ map f l = map g l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ map f { toList := toList✝ } = map g { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ map f { toList := toList✝ } = map g { toList := toList✝ }.unattach

Tactic:
simp only [List.map_toArray, List.unattach_toArray]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ (List.map f toList✝).toArray = (List.map g toList✝.unattach).toArray

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x

Tactic:
simp [hf]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ (List.map f toList✝).toArray = (List.map g toList✝.unattach).toArray

Tactic:
rw [List.map_subtype]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : { x // p x } → β
g : α → β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
-- Mathlib/Algebra/Order/Group/Defs.lean
theorem exists_one_lt' [Nontrivial α] : ∃ a : α, 1 < a

Proof state:
case intro.inr
α : Type u
inst✝¹ : LinearOrderedCommGroup α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a

Tactic:
exact ⟨y, h⟩

Result:
no goals

Proof state:
case intro
α : Type u
inst✝¹ : LinearOrderedCommGroup α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
⊢ ∃ a, 1 < a

Tactic:
obtain h|h := hy.lt_or_lt

Result:
case intro.inl
α : Type u
inst✝¹ : LinearOrderedCommGroup α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a

case intro.inr
α : Type u
inst✝¹ : LinearOrderedCommGroup α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a

Proof state:
case intro.inl
α : Type u
inst✝¹ : LinearOrderedCommGroup α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a

Tactic:
exact ⟨y⁻¹, one_lt_inv'.mpr h⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : LinearOrderedCommGroup α
inst✝ : Nontrivial α
⊢ ∃ a, 1 < a

Tactic:
obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)

Result:
case intro
α : Type u
inst✝¹ : LinearOrderedCommGroup α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
⊢ ∃ a, 1 < a
-- Mathlib/Algebra/Order/Floor.lean
theorem one_le_ceil_iff : 1 ≤ ⌈a⌉ ↔ 0 < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ 1 ≤ ⌈a⌉ ↔ 0 < a

Tactic:
rw [← zero_add (1 : ℤ), add_one_le_ceil_iff, cast_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Convolution.lean
theorem mconv_comm {M : Type*} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] (μ : Measure M)
    (ν : Measure M) [SFinite μ] [SFinite ν] : μ ∗ ν = ν ∗ μ

Proof state:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ μ ∗ ν = ν ∗ μ

Tactic:
unfold mconv

Result:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ map (fun x => x.1 * x.2) (μ.prod ν) = map (fun x => x.1 * x.2) (ν.prod μ)

Proof state:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ map ((fun x => x.1 * x.2) ∘ Prod.swap) (ν.prod μ) = map (fun x => x.1 * x.2) (ν.prod μ)

Tactic:
simp [Function.comp_def, mul_comm]

Result:
no goals

Proof state:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ Measurable fun x => x.1 * x.2

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ Measurable Prod.swap

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ map (fun x => x.1 * x.2) (μ.prod ν) = map (fun x => x.1 * x.2) (ν.prod μ)

Tactic:
rw [← prod_swap, map_map (by fun_prop)]

Result:
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ map ((fun x => x.1 * x.2) ∘ Prod.swap) (ν.prod μ) = map (fun x => x.1 * x.2) (ν.prod μ)

M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν : Measure M
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ Measurable Prod.swap
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem borel_le_caratheodory : S ≤ μ.outerMeasure.caratheodory

Proof state:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this : ↑U' \ U ⊆ ↑U' \ ↑L'
⊢ μ L' + μ.innerContent { carrier := ↑U' \ ↑L', is_open' := ⋯ } ≤ μ.outerMeasure ↑U'

Tactic:
simp only [innerContent, iSup_subtype']

Result:
case mk
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this : ↑U' \ U ⊆ ↑U' \ ↑L'
⊢ μ L' + ⨆ x, μ ↑x ≤ μ.outerMeasure ↑U'

Proof state:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ μ.outerMeasure (↑U' ∩ U) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
rw [μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)]

Result:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ μ.innerContent { carrier := ↑U' ∩ U, is_open' := ⋯ } + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
-- Mathlib/Order/OrdContinuous.lean
theorem le_iff (hf : LeftOrdContinuous f) (h : Injective f) {x y} : f x ≤ f y ↔ x ≤ y

Proof state:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
simp only [← sup_eq_right, ← hf.map_sup, h.eq_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
/-- The **Cauchy-Schwarz inequality** for positive semidefinite symmetric forms. -/
lemma apply_sq_le_of_symm (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm) (x y : M) :
    (B x y) ^ 2 ≤ (B x x) * (B y y)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
exact apply_mul_apply_le_of_forall_zero_le B hs x y

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 = (B x) y * (B y) x

Tactic:
rw [sq, ← hB, RingHom.id_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 ≤ (B x) x * (B y) y

Tactic:
rw [show (B x y) ^ 2 = (B x y) * (B y x) by rw [sq, ← hB, RingHom.id_apply]]

Result:
R : Type u_1
M : Type u_5
inst✝² : LinearOrderedCommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_singleton_right : image₂ f s {b} = s.image fun a => f a b :=
  ext fun x => by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
x : γ
⊢ x ∈ image₂ f s {b} ↔ x ∈ image (fun a => f a b) s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Functor.lean
theorem uncurry_expComparison (A B : C) :
    CartesianClosed.uncurry ((expComparison F A).natTrans.app B) =
      inv (prodComparison F _ _) ≫ F.map ((exp.ev _).app _)

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ uncurry ((expComparison F A).natTrans.app B) = inv (prodComparison F A (A ⟹ B)) ≫ F.map ((exp.ev A).app B)

Tactic:
rw [uncurry_eq, expComparison_ev]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem smul_mk [SMul R M] [IsScalarTower R M M] (c : R) (a b) :
    c • (mk a b : Localization S) = mk (c • a) b

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ (c • 1) • a /ₒ (b * 1) = c • a /ₒ b

Tactic:
rw [smul_assoc, one_smul, mul_one]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ OreLocalization.oreNum (c • 1) b • a /ₒ (OreLocalization.oreDenom (c • 1) b * 1) = c • a /ₒ b

Tactic:
show (c • 1) • a /ₒ (b * 1) = _

Result:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ (c • 1) • a /ₒ (b * 1) = c • a /ₒ b

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • mk a b = mk (c • a) b

Tactic:
rw [mk, mk, ← OreLocalization.smul_one_oreDiv_one_smul, OreLocalization.oreDiv_smul_oreDiv]

Result:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ OreLocalization.oreNum (c • 1) b • a /ₒ (OreLocalization.oreDenom (c • 1) b * 1) = c • a /ₒ b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_flatten' (f : α → β → β) (b : β) (L : Array (Array α))
    (w : start = L.flatten.size) :
    (flatten L).foldr f b start 0 = L.foldr (fun l b => l.foldr f b) b

Proof state:
case of
α : Type u_1
β : Type u_2
f : α → β → β
b : β
xss✝ : List (List α)
⊢ foldr f b (List.map List.toArray xss✝).toArray.flatten =
    foldr (fun l b => foldr f b l) b (List.map List.toArray xss✝).toArray

Tactic:
simp [List.foldr_flatten, List.foldr_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
L : Array (Array α)
⊢ foldr f b L.flatten = foldr (fun l b => foldr f b l) b L

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
β : Type u_2
f : α → β → β
b : β
xss✝ : List (List α)
⊢ foldr f b (List.map List.toArray xss✝).toArray.flatten =
    foldr (fun l b => foldr f b l) b (List.map List.toArray xss✝).toArray

Proof state:
α : Type u_1
β : Type u_2
start : Nat
f : α → β → β
b : β
L : Array (Array α)
w : start = L.flatten.size
⊢ foldr f b L.flatten start = foldr (fun l b => foldr f b l) b L

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
L : Array (Array α)
⊢ foldr f b L.flatten = foldr (fun l b => foldr f b l) b L
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_X (n) : trunc (n + 2) X = (Polynomial.X : R[X])

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (if d < n + 2 then if d = 1 then 1 else 0 else 0) = Polynomial.X.coeff d

Tactic:
split_ifs with h₁ h₂

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ 1 = Polynomial.X.coeff d

case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d

case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ False

Tactic:
apply h₁

Result:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ d < n + 2

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (trunc (n + 2) X).coeff d = Polynomial.X.coeff d

Tactic:
rw [coeff_trunc, coeff_X]

Result:
case a
R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (if d < n + 2 then if d = 1 then 1 else 0 else 0) = Polynomial.X.coeff d

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ trunc (n + 2) X = Polynomial.X

Tactic:
ext d

Result:
case a
R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (trunc (n + 2) X).coeff d = Polynomial.X.coeff d

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ d ≠ 1

Tactic:
intro hd

Result:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ False

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ 1 = Polynomial.X.coeff d

Tactic:
rw [h₂, coeff_X_one]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d

Tactic:
rw [coeff_X_of_ne_one h₂]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ d < n + 2

Tactic:
rw [hd]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ 1 < n + 2

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ 1 < n + 2

Tactic:
exact n.one_lt_succ_succ

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d

Tactic:
rw [coeff_X_of_ne_one]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ d ≠ 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig len) (h : x ≤ aig.decls.size) :
    x ≤ (f aig input).aig.decls.size

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ (f aig input).aig.decls.size

Tactic:
apply Nat.le_trans

Result:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ Nat

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ x ≤ ?m

Tactic:
exact h

Result:
no goals

Proof state:
case a
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len x : Nat
aig : AIG α
input : β aig len
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

Tactic:
exact le_size aig input

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean
theorem contMDiffWithinAt_iff_contDiffWithinAt {f : E → E'} {s : Set E} {x : E} :
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
x : E
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
simp +contextual only [ContMDiffWithinAt, liftPropWithinAt_iff',
  ContDiffWithinAtProp, iff_def, mfld_simps]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
x : E
⊢ ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
s : Set E
x : E
⊢ ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x

Tactic:
exact ContDiffWithinAt.continuousWithinAt

Result:
no goals