harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_flatten (p : α → Bool) (L : Array (Array α)) :
    filter p (flatten L) = flatten (map (filter p) L)

Proof state:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ filter p (List.map List.toArray xss✝).toArray.flatten =
    (map (fun as => filter p as) (List.map List.toArray xss✝).toArray).flatten

Tactic:
simp only [flatten_toArray_map, size_toArray, List.length_flatten, List.filter_toArray',
  List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]

Result:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ (List.map (List.filter p) xss✝).flatten.toArray = (List.map (fun x => (List.filter p x).toArray) xss✝).toArray.flatten

Proof state:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ (List.map (List.filter p) xss✝).flatten.toArray = (List.map (fun x => (List.filter p x).toArray) xss✝).toArray.flatten

Tactic:
rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
L : Array (Array α)
⊢ filter p L.flatten = (map (fun as => filter p as) L).flatten

Tactic:
induction L using array₂_induction

Result:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ filter p (List.map List.toArray xss✝).toArray.flatten =
    (map (fun as => filter p as) (List.map List.toArray xss✝).toArray).flatten
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tendsto_sin_neg_pi_div_two : Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))

Proof state:
case h.e'_5.h.e'_3

⊢ -1 = sin (-(π / 2))

Tactic:
simp

Result:
no goals

Proof state:
⊢ Tendsto sin (𝓝[>] (-(π / 2))) (𝓝 (-1))

Tactic:
convert continuous_sin.continuousWithinAt.tendsto using 2

Result:
case h.e'_5.h.e'_3

⊢ -1 = sin (-(π / 2))
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem integrable_rnDeriv (c : ComplexMeasure α) (μ : Measure α) : Integrable (c.rnDeriv μ) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
⊢ MemLp (fun x => RCLike.re (c.rnDeriv μ x)) 1 μ ∧ MemLp (fun x => RCLike.im (c.rnDeriv μ x)) 1 μ

Tactic:
exact
  ⟨memLp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _),
    memLp_one_iff_integrable.2 (SignedMeasure.integrable_rnDeriv _ _)⟩

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
⊢ Integrable (c.rnDeriv μ) μ

Tactic:
rw [← memLp_one_iff_integrable, ← memLp_re_im_iff]

Result:
α : Type u_1
m : MeasurableSpace α
c : ComplexMeasure α
μ : Measure α
⊢ MemLp (fun x => RCLike.re (c.rnDeriv μ x)) 1 μ ∧ MemLp (fun x => RCLike.im (c.rnDeriv μ x)) 1 μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_empty_of_stop_le_start (as : Array α) {start stop : Nat} (h : stop ≤ start) :
    as.extract start stop = #[]

Proof state:
α : Type u_1
as : Array α
start stop : Nat
h : stop ≤ start
⊢ extract.loop as (min stop as.size - start) start #[] = #[]

Tactic:
rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.zero_min, extract_loop_zero]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
start stop : Nat
h : stop ≤ start
⊢ as.extract start stop = #[]

Tactic:
simp only [extract, Nat.sub_eq, mkEmpty_eq]

Result:
α : Type u_1
as : Array α
start stop : Nat
h : stop ≤ start
⊢ extract.loop as (min stop as.size - start) start #[] = #[]
-- Mathlib/Data/Vector/Basic.lean
theorem get_set_eq_if {v : Vector α n} {i j : Fin n} (a : α) :
    (v.set i a).get j = if i = j then a else v.get j

Proof state:
case pos
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ (v.set i a).get j = a

Tactic:
try simp [*]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
⊢ (v.set i a).get j = if i = j then a else v.get j

Tactic:
split_ifs <;> (try simp [*])

Result:
case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j

Proof state:
case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j

Tactic:
rwa [get_set_of_ne]

Result:
no goals

Proof state:
case pos
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ (v.set i a).get j = a

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem nsmul_eq_self : ∀ {n : ℕ} (_ : n ≠ 0) (a : α), n • a = a
  | 0, h => (h rfl).elim
  | 1, _ => one_nsmul
  | n + 2, _ => fun a ↦ by rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]

Proof state:
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ (n + 2) • a = a

Tactic:
rw [succ_nsmul, nsmul_eq_self n.succ_ne_zero, add_idem]

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem AnalyticAt.comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x))
    (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (g ∘ f) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
hg : AnalyticAt 𝕜 g (f x)
hf : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (g ∘ f) x

Tactic:
rw [← analyticWithinAt_univ] at hg hf ⊢

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f Set.univ x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) Set.univ x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f Set.univ x
⊢ AnalyticWithinAt 𝕜 (g ∘ f) Set.univ x

Tactic:
apply hg.comp hf (by simp)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
hg : AnalyticWithinAt 𝕜 g Set.univ (f x)
hf : AnalyticWithinAt 𝕜 f Set.univ x
⊢ Set.MapsTo f Set.univ Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
@[simp]
lemma inv_cobounded₀ : (cobounded α)⁻¹ = 𝓝[≠] 0

Proof state:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = comap norm (comap Inv.inv atTop)

Tactic:
simp only [comap_comap, Function.comp_def, norm_inv]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (cobounded α)⁻¹ = 𝓝[≠] 0

Tactic:
rw [← comap_norm_atTop, ← Filter.comap_inv, ← comap_norm_nhdsGT_zero, ← inv_atTop₀,
  ← Filter.comap_inv]

Result:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = comap norm (comap Inv.inv atTop)
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem affineIndependent_iff_not_collinear_of_ne {p : Fin 3 → P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂)
    (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) :
    AffineIndependent k p ↔ ¬Collinear k ({p i₁, p i₂, p i₃} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}

Tactic:
rw [affineIndependent_iff_not_collinear, ← Set.image_univ, ← Finset.coe_univ, hu,
  Finset.coe_insert, Finset.coe_insert, Finset.coe_singleton, Set.image_insert_eq, Set.image_pair]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Finset.univ = {i₁, i₂, i₃}

Tactic:
revert i₁ i₂ i₃

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
⊢ ∀ {i₁ i₂ i₃ : Fin 3}, i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → Finset.univ = {i₁, i₂, i₃}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}

Tactic:
have hu : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃} := by
  revert i₁ i₂ i₃; decide

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hu : Finset.univ = {i₁, i₂, i₃}
⊢ AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
⊢ ∀ {i₁ i₂ i₃ : Fin 3}, i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → Finset.univ = {i₁, i₂, i₃}

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Even.add [Add β] {f g : α → β} (hf : f.Even) (hg : g.Even) : (f + g).Even

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f + g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f + g) (-a) = (f + g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f + g) (-a) = (f + g) a

Tactic:
simp only [hf a, hg a, Pi.add_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma vecMul_self_mul_conjTranspose_eq_zero (A : Matrix m n R) (v : m → R) :
    v ᵥ* (A * Aᴴ) = 0 ↔ v ᵥ* A = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : m → R
⊢ v ᵥ* (A * Aᴴ) = 0 ↔ v ᵥ* A = 0

Tactic:
simpa only [conjTranspose_conjTranspose] using vecMul_conjTranspose_mul_self_eq_zero Aᴴ _

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
theorem Algebra.FormallySmooth.iff_split_injection :
    Algebra.FormallySmooth R S ↔ ∃ l, l ∘ₗ (kerCotangentToTensor R P S) = LinearMap.id

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
this :
  (∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id) ↔
    ∃ g, (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S
⊢ FormallySmooth R S ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id

Tactic:
rw [this, ← Algebra.FormallySmooth.iff_split_surjection _ hf]

Result:
no goals

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ FormallySmooth R S ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id

Tactic:
have := (retractionKerCotangentToTensorEquivSection (R := R) hf).nonempty_congr

Result:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
this :
  Nonempty { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ↔
    Nonempty { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }
⊢ FormallySmooth R S ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
this :
  Nonempty { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ↔
    Nonempty { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }
⊢ FormallySmooth R S ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id

Tactic:
simp only [nonempty_subtype] at this

Result:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
this :
  (∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id) ↔
    ∃ g, (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S
⊢ FormallySmooth R S ↔ ∃ l, l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
-- Mathlib/Analysis/Convex/Basic.lean
theorem stdSimplex_eq_inter : stdSimplex 𝕜 ι = (⋂ x, { f | 0 ≤ f x }) ∩ { f | ∑ x, f x = 1 }

Proof state:
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
⊢ stdSimplex 𝕜 ι = (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}

Tactic:
ext f

Result:
case h
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}

Proof state:
case h
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ x, {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}

Tactic:
simp only [stdSimplex, Set.mem_inter_iff, Set.mem_iInter, Set.mem_setOf_eq]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
theorem BddBelow.image2_bddAbove : BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddBelow s → BddBelow t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)

Tactic:
exact ⟨f a b, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha hb⟩

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem pellZd_add (m) : ∀ n, pellZd a1 (m + n) = pellZd a1 m * pellZd a1 n
  | 0 => (mul_one _).symm
  | n + 1 => by rw [← add_assoc, pellZd_succ, pellZd_succ, pellZd_add _ n, ← mul_assoc]

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ pellZd a1 (m + (n + 1)) = pellZd a1 m * pellZd a1 (n + 1)

Tactic:
rw [← add_assoc, pellZd_succ, pellZd_succ, pellZd_add _ n, ← mul_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean
@[simp]
lemma equivFreeAlgebra_ι_apply (b : Basis κ R M) (i : κ) :
    equivFreeAlgebra b (ι R (b i)) = FreeAlgebra.ι R i :=
  (TensorAlgebra.lift_ι_apply _ _).trans <| by simp

Proof state:
κ : Type uκ
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis κ R M
i : κ
⊢ (Finsupp.linearCombination R (FreeAlgebra.ι R) ∘ₗ ↑b.repr) (b i) = FreeAlgebra.ι R i

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem setIntegral_prod_mul {L : Type*} [RCLike L] (f : α → L) (g : β → L) (s : Set α)
    (t : Set β) :
    ∫ z in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ x in s, f x ∂μ) * ∫ y in t, g y ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
L : Type u_5
inst✝ : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ ∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν

Tactic:
rw [← Measure.prod_restrict s t]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
L : Type u_5
inst✝ : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ ∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
L : Type u_5
inst✝ : RCLike L
f : α → L
g : β → L
s : Set α
t : Set β
⊢ ∫ (z : α × β), f z.1 * g z.2 ∂(μ.restrict s).prod (ν.restrict t) = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν

Tactic:
apply integral_prod_mul

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Colimits.lean
lemma Quot.desc_toCocone_desc_app [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A)
    (hc : IsColimit c) (x : Quot F) : hc.desc (toCocone F f) (Quot.desc F c x) = f x

Proof state:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ (ConcreteCategory.hom (hc.desc (toCocone F f))) ((desc F c) x) =
    ((Hom.hom (hc.desc (toCocone F f))).comp (desc F c)) x

Tactic:
dsimp

Result:
no goals

Proof state:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ (ConcreteCategory.hom (hc.desc (toCocone F f))) ((desc F c) x) = f x

Tactic:
conv_rhs => rw [← Quot.desc_toCocone_desc F c f hc]

Result:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ (ConcreteCategory.hom (hc.desc (toCocone F f))) ((desc F c) x) =
    ((Hom.hom (hc.desc (toCocone F f))).comp (desc F c)) x
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_lt (hx : 0 ≤ x) (hy : 0 ≤ y) : √x < y ↔ x < y ^ 2

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ x < y ^ 2

Tactic:
rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean
/-- A product over all subsets of `s ∪ {x}` is obtained by multiplying the product over all subsets
of `s`, and over all subsets of `s` to which one adds `x`. -/
@[to_additive "A sum over all subsets of `s ∪ {x}` is obtained by summing the sum over all subsets
of `s`, and over all subsets of `s` to which one adds `x`."]
lemma prod_powerset_insert [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) :
    ∏ t ∈ (insert a s).powerset, f t =
      (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)

Tactic:
aesop (add simp [disjoint_left, insert_subset_iff])

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ ∀ x ∈ s.powerset, ∀ y ∈ s.powerset, insert a x = insert a y → x = y

Tactic:
exact insert_erase_invOn.2.injOn.mono fun t ht ↦ not_mem_mono (mem_powerset.1 ht) ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

Tactic:
rw [powerset_insert, prod_union, prod_image]

Result:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ ∀ x ∈ s.powerset, ∀ y ∈ s.powerset, insert a x = insert a y → x = y

α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ Disjoint s.powerset (image (insert a) s.powerset)
-- Mathlib/Data/Matroid/Circuit.lean
/-- The fundamental isCircuit of `e` and `X` has the junk value `{e}` if `e ∈ X` -/
lemma fundCircuit_eq_of_mem (heX : e ∈ X) : M.fundCircuit e X = {e}

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ M.fundCircuit e X = {e}

Tactic:
suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
  simpa [subset_antisymm_iff, fundCircuit]

Result:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e

Tactic:
exact fun b hbX h ↦ h _ (singleton_subset_iff.2 heX) Subset.rfl

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
simpa [subset_antisymm_iff, fundCircuit]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_abs (x : ℝ) : ((x : EReal).abs : EReal) = (|x| : ℝ)

Proof state:
x : ℝ
⊢ ↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)

Tactic:
rfl

Result:
no goals

Proof state:
x : ℝ
⊢ ↑(↑x).abs = ↑|x|

Tactic:
rw [abs_def, ← Real.coe_nnabs, ENNReal.ofReal_coe_nnreal]

Result:
x : ℝ
⊢ ↑↑(Real.nnabs x) = ↑↑(Real.nnabs x)
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem getVert_zero {u v} (w : G.Walk u v) : w.getVert 0 = u

Proof state:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
⊢ w.getVert 0 = u

Tactic:
cases w <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallySurjective_of_le {K : GrothendieckTopology C} (hJK : J ≤ K) {F G : Cᵒᵖ ⥤ A}
    (f : F ⟶ G) (h : IsLocallySurjective J f) : IsLocallySurjective K f where
  imageSieve_mem s

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
K : GrothendieckTopology C
hJK : J ≤ K
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
h : IsLocallySurjective J f
U✝ : C
s : ToType (G.obj (op U✝))
⊢ imageSieve f s ∈ J U✝

Tactic:
exact h.1 _

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
K : GrothendieckTopology C
hJK : J ≤ K
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
h : IsLocallySurjective J f
U✝ : C
s : ToType (G.obj (op U✝))
⊢ imageSieve f s ∈ K U✝

Tactic:
apply hJK

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
K : GrothendieckTopology C
hJK : J ≤ K
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
h : IsLocallySurjective J f
U✝ : C
s : ToType (G.obj (op U✝))
⊢ imageSieve f s ∈ J U✝
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_add_Ioo : (fun x => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' Ioo b c = Ioo (b - a) (c - a)

Tactic:
simp [← Ioi_inter_Iio]

Result:
no goals