harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TMToPartrec.lean
theorem codeSupp_comp (f g k) :
    codeSupp (Code.comp f g) k =
      trStmts₁ (trNormal (Code.comp f g) k) ∪ codeSupp g (Cont'.comp f k)

Proof state:
f g : Code
k : Cont'
⊢ codeSupp (f.comp g) k = trStmts₁ (trNormal (f.comp g) k) ∪ codeSupp g (Cont'.comp f k)

Tactic:
simp only [codeSupp, codeSupp', trNormal, Finset.union_assoc, contSupp]

Result:
f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))

Proof state:
f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))

Tactic:
rw [← Finset.union_assoc _ _ (contSupp k),
  Finset.union_eq_right.2 (codeSupp'_self _ _)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_unique {n : Type*} [Unique n] [DecidableEq n] [Fintype n] (A : Matrix n n R) :
    det A = A default default

Proof state:
R : Type v
inst✝³ : CommRing R
n : Type u_3
inst✝² : Unique n
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
⊢ A.det = A default default

Tactic:
simp [det_apply, univ_unique]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem smul_set_pi_of_isUnit {M ι : Type*} {α : ι → Type*} [Monoid M] [∀ i, MulAction M (α i)]
    {c : M} (hc : IsUnit c) (I : Set ι) (s : ∀ i, Set (α i)) : c • I.pi s = I.pi (c • s ·)

Proof state:
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst✝¹ : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
c : M
hc : IsUnit c
I : Set ι
s : (i : ι) → Set (α i)
⊢ c • I.pi s = I.pi fun x => c • s x

Tactic:
lift c to Mˣ using hc

Result:
case intro
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst✝¹ : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
I : Set ι
s : (i : ι) → Set (α i)
c : Mˣ
⊢ ↑c • I.pi s = I.pi fun x => ↑c • s x

Proof state:
case intro
M : Type u_5
ι : Type u_6
α : ι → Type u_7
inst✝¹ : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
I : Set ι
s : (i : ι) → Set (α i)
c : Mˣ
⊢ ↑c • I.pi s = I.pi fun x => ↑c • s x

Tactic:
exact smul_set_pi c I s

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem im_inner_adjoint_mul_self_eq_zero (T : E →ₗ[𝕜] E) (x : E) :
    im ⟪x, LinearMap.adjoint T (T x)⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ im ⟪x, (adjoint T) (T x)⟫_𝕜 = 0

Tactic:
simp only [mul_apply, adjoint_inner_right, inner_self_eq_norm_sq_to_K]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ im (↑‖T x‖ ^ 2) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ im (↑‖T x‖ ^ 2) = 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem toList_eq_nil_of_mem_of_range (w : ReducedWord G A B)
    (hw : w.prod φ ∈ (of.range : Subgroup (HNNExtension G A B φ))) :
    w.toList = []

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ w.toList = []

Tactic:
have : w.prod φ = w'.prod φ := by simp [w', ReducedWord.prod, hg]

Result:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
this : ReducedWord.prod φ w = ReducedWord.prod φ w'
⊢ w.toList = []

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
⊢ w.toList = []

Tactic:
let w' : ReducedWord G A B := { ReducedWord.empty G A B with head := g }

Result:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ w.toList = []

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
this : ReducedWord.prod φ w = ReducedWord.prod φ w'
⊢ w.toList = []

Tactic:
simpa [w'] using (map_fst_eq_and_of_prod_eq φ this).1

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
w' : ReducedWord G A B :=
  let __src := ReducedWord.empty G A B;
  { head := g, toList := __src.toList, chain := ⋯ }
⊢ ReducedWord.prod φ w = ReducedWord.prod φ w'

Tactic:
simp [w', ReducedWord.prod, hg]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
hw : ReducedWord.prod φ w ∈ of.range
⊢ w.toList = []

Tactic:
rcases hw with ⟨g, hg⟩

Result:
case intro
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
w : ReducedWord G A B
g : G
hg : of g = ReducedWord.prod φ w
⊢ w.toList = []
-- Mathlib/Analysis/CStarAlgebra/Exponential.lean
theorem Commute.expUnitary_add {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) :
    expUnitary (a + b) = expUnitary a * expUnitary b

Proof state:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ expUnitary (a + b) = expUnitary a * expUnitary b

Tactic:
ext

Result:
case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)

Proof state:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ Commute (I • ↑a) (I • ↑b)

Tactic:
unfold Commute SemiconjBy

Result:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ I • ↑a * I • ↑b = I • ↑b * I • ↑a

Proof state:
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ I • ↑a * I • ↑b = I • ↑b * I • ↑a

Tactic:
simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]

Result:
no goals

Proof state:
case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)

Tactic:
have hcomm : Commute (I • (a : A)) (I • (b : A)) := by
  unfold Commute SemiconjBy
  simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]

Result:
case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
hcomm : Commute (I • ↑a) (I • ↑b)
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)

Proof state:
case a
A : Type u_1
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : StarRing A
inst✝² : ContinuousStar A
inst✝¹ : CompleteSpace A
inst✝ : StarModule ℂ A
a b : ↥(selfAdjoint A)
h : Commute ↑a ↑b
hcomm : Commute (I • ↑a) (I • ↑b)
⊢ ↑(expUnitary (a + b)) = ↑(expUnitary a * expUnitary b)

Tactic:
simpa only [expUnitary_coe, AddSubgroup.coe_add, smul_add] using exp_add_of_commute hcomm

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.insert_indep_iff_of_not_mem (hI : M.Indep I) (heI : e ∉ I) :
    M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I

Tactic:
rw [mem_diff, hI.mem_closure_iff_of_not_mem heI, dep_iff, not_and, not_imp_not, insert_subset_iff,
  and_iff_left hI.subset_ground]

Result:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))

Tactic:
exact ⟨fun h ↦ ⟨h.subset_ground (mem_insert e I), fun _ ↦ h⟩, fun h ↦ h.2 h.1⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
lemma two_le_natDegree_of_nextCoeff_eraseLead (hlead : f.eraseLead ≠ 0)
    (hnext : f.nextCoeff = 0) : 2 ≤ f.natDegree

Proof state:
case inr.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : (C a * X + C b).nextCoeff = 0
⊢ (C a * X + C b).eraseLead = 0

Tactic:
rw [nextCoeff_C_mul_X_add_C ha] at hnext

Result:
case inr.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
⊢ (C a * X + C b).eraseLead = 0

Proof state:
case inl.intro
R : Type u_1
inst✝ : Semiring R
a : R
hnext : (C a).nextCoeff = 0
⊢ (C a).eraseLead = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hlead : f.eraseLead ≠ 0
hnext : f.nextCoeff = 0
⊢ 2 ≤ f.natDegree

Tactic:
contrapose! hlead

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree < 2
⊢ f.eraseLead = 0

Proof state:
case inr.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X + C 0).eraseLead = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree < 2
⊢ f.eraseLead = 0

Tactic:
rw [Nat.lt_succ_iff, Nat.le_one_iff_eq_zero_or_eq_one, natDegree_eq_zero, natDegree_eq_one]
  at hlead

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : (∃ x, C x = f) ∨ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = f
⊢ f.eraseLead = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : (∃ x, C x = f) ∨ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = f
⊢ f.eraseLead = 0

Tactic:
obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead

Result:
case inl.intro
R : Type u_1
inst✝ : Semiring R
a : R
hnext : (C a).nextCoeff = 0
⊢ (C a).eraseLead = 0

case inr.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : (C a * X + C b).nextCoeff = 0
⊢ (C a * X + C b).eraseLead = 0

Proof state:
case inr.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
⊢ (C a * X + C b).eraseLead = 0

Tactic:
subst b

Result:
case inr.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X + C 0).eraseLead = 0
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycleOn_inv : f⁻¹.IsCycleOn s ↔ f.IsCycleOn s

Proof state:
α : Type u_2
f : Perm α
s : Set α
⊢ f⁻¹.IsCycleOn s ↔ f.IsCycleOn s

Tactic:
simp only [IsCycleOn, sameCycle_inv, and_congr_left_iff]

Result:
α : Type u_2
f : Perm α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y) → (Set.BijOn (⇑f⁻¹) s s ↔ Set.BijOn (⇑f) s s)

Proof state:
α : Type u_2
f : Perm α
s : Set α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → f.SameCycle x y) → (Set.BijOn (⇑f⁻¹) s s ↔ Set.BijOn (⇑f) s s)

Tactic:
exact fun _ ↦ ⟨fun h ↦ Set.BijOn.perm_inv h, fun h ↦ Set.BijOn.perm_inv h⟩

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_ceil_le (a b : α) : ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌈b⌉ ≤ ↑⌈a + b⌉ + 1 - a

Tactic:
refine (ceil_lt_add_one _).le.trans ?_

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ b + 1 ≤ ↑⌈a + b⌉ + 1 - a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

Tactic:
rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌈b⌉ ≤ ↑⌈a + b⌉ + 1 - a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b ≤ ↑⌈a + b⌉

Tactic:
exact le_ceil _

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ b + 1 ≤ ↑⌈a + b⌉ + 1 - a

Tactic:
rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b ≤ ↑⌈a + b⌉
-- Mathlib/RingTheory/Algebraic/LinearIndependent.lean
theorem Transcendental.linearIndependent_sub_inv
    {F E : Type*} [Field F] [Field E] [Algebra F E] {x : E} (H : Transcendental F x) :
    LinearIndependent F fun a ↦ (x - algebraMap F E a)⁻¹

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
hm : (aeval i) p = (aeval i) 0
⊢ m i = 0

Tactic:
have h2 : ∀ j ∈ s.erase i, m j * ((s.erase j).prod fun x ↦ i - x) = 0 := fun j hj ↦ by
  have := Finset.mem_erase_of_ne_of_mem (Finset.ne_of_mem_erase hj).symm hi
  simp_rw [← (s.erase j).prod_erase_mul _ this, sub_self, mul_zero]

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
H : ∀ (p : F[X]), (aeval x) p = 0 → p = 0
s : Finset F
m : F → F
i : F
hi : i ∈ s
hnz : ∀ (a : F), x - (algebraMap F E) a ≠ 0
b : E := ∏ j ∈ s, (x - (algebraMap F E) j)
h1 : ∀ i ∈ s, m i • (b * (x - (algebraMap F E) i)⁻¹) = m i • ∏ j ∈ s.erase i, (x - (algebraMap F E) j)
p : F[X] := ∑ i ∈ s, C (m i) * ∏ j ∈ s.erase i, (X - C j)
hm : (aeval i) p = (aeval i) 0
h2 : ∀ j ∈ s.erase i, m j * ∏ x ∈ s.erase j, (i - x) = 0
⊢ m i = 0
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_le_iff {a b} : nfp f a ≤ b ↔ ∀ n, f^[n] a ≤ b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
exact Ordinal.iSup_le_iff

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ nfp f a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b

Tactic:
rw [← iSup_iterate_eq_nfp]

Result:
f : Ordinal.{u} → Ordinal.{u}
a b : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ b ↔ ∀ (n : ℕ), f^[n] a ≤ b
-- Mathlib/LinearAlgebra/Dual.lean
theorem flip_injective_iff₁ [FiniteDimensional K V₁] : Injective B.flip ↔ Surjective B

Proof state:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Surjective (⇑B.flip.dualMap ∘ ⇑(evalEquiv K V₁).toEquiv) ↔ Surjective ⇑B

Tactic:
rfl

Result:
no goals

Proof state:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Injective ⇑B.flip ↔ Surjective ⇑B

Tactic:
rw [← dualMap_surjective_iff, ← (evalEquiv K V₁).toEquiv.surjective_comp]

Result:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Surjective (⇑B.flip.dualMap ∘ ⇑(evalEquiv K V₁).toEquiv) ↔ Surjective ⇑B
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
theorem integral_eq_integral_nnrealPart_sub [OpensMeasurableSpace X] (f : X →ᵇ ℝ) :
    ∫ x, f x ∂μ = (∫ x, (f.nnrealPart x : ℝ) ∂μ) - ∫ x, ((-f).nnrealPart x : ℝ) ∂μ

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ ∫ (a : X), (NNReal.toReal ∘ ⇑f.nnrealPart) a ∂μ - ∫ (a : X), (NNReal.toReal ∘ ⇑(-f).nnrealPart) a ∂μ =
    ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ

Tactic:
simp only [Function.comp_apply]

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ

Tactic:
simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub,
           integrable_of_nnreal]

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ ∫ (a : X), (NNReal.toReal ∘ ⇑f.nnrealPart) a ∂μ - ∫ (a : X), (NNReal.toReal ∘ ⇑(-f).nnrealPart) a ∂μ =
    ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem toNonUnitalSubsemiring_injective :
    Function.Injective
      (toNonUnitalSubsemiring : NonUnitalSubalgebra R A → NonUnitalSubsemiring A) :=
  fun S T h =>
  ext fun x => by rw [← mem_toNonUnitalSubsemiring, ← mem_toNonUnitalSubsemiring, h]

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubsemiring = T.toNonUnitalSubsemiring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubsemiring, ← mem_toNonUnitalSubsemiring, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
@[simp]
lemma tilted_of_not_aemeasurable (hf : ¬ AEMeasurable f μ) : μ.tilted f = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ μ.tilted f = 0

Tactic:
refine tilted_of_not_integrable ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (fun x => rexp (f x)) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
this : ¬AEMeasurable (fun x => rexp (f x)) μ
⊢ ¬Integrable (fun x => rexp (f x)) μ

Tactic:
exact fun h ↦ this h.1.aemeasurable

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable (fun x => rexp (f x)) μ

Tactic:
exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (fun x => rexp (f x)) μ

Tactic:
suffices ¬ AEMeasurable (fun x ↦ exp (f x)) μ by exact fun h ↦ this h.1.aemeasurable

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬AEMeasurable f μ
⊢ ¬AEMeasurable (fun x => rexp (f x)) μ
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.isoCoproduct_hom {f : J → C} [HasBiproduct f] :
    (biproduct.isoCoproduct f).hom = biproduct.desc (Sigma.ι f) :=
  biproduct.hom_ext' _ _ fun j => by simp [← Iso.eq_comp_inv]

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ ι f j ≫ (isoCoproduct f).hom = ι f j ≫ desc (Sigma.ι f)

Tactic:
simp [← Iso.eq_comp_inv]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem interior_pi_set {I : Set ι} (hI : I.Finite) {s : ∀ i, Set (π i)} :
    interior (pi I s) = I.pi fun i => interior (s i)

Proof state:
case h
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ a ∈ interior (I.pi s) ↔ a ∈ I.pi fun i => interior (s i)

Tactic:
simp only [Set.mem_pi, mem_interior_iff_mem_nhds, set_pi_mem_nhds_iff hI]

Result:
no goals

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
⊢ interior (I.pi s) = I.pi fun i => interior (s i)

Tactic:
ext a

Result:
case h
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ a ∈ interior (I.pi s) ↔ a ∈ I.pi fun i => interior (s i)
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nat_le_lift_iff {n : ℕ} {a : Cardinal.{u}} : n ≤ lift.{v} a ↔ n ≤ a

Proof state:
n : ℕ
a : Cardinal.{u}
⊢ ↑n ≤ lift.{v, u} a ↔ ↑n ≤ a

Tactic:
rw [← lift_natCast.{v,u}, lift_le]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_comp_right {s : Set α} (f : β → α) {g : α → M} {x : β} :
    mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → α
g : α → M
x : β
⊢ (f ⁻¹' s).mulIndicator (g ∘ f) x = s.mulIndicator g (f x)

Tactic:
simp only [mulIndicator, Function.comp]

Result:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → α
g : α → M
x : β
⊢ (if x ∈ f ⁻¹' s then g (f x) else 1) = if f x ∈ s then g (f x) else 1

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → α
g : α → M
x : β
h : x ∉ f ⁻¹' s
h'' : f x ∈ s
⊢ 1 = g (f x)

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → α
g : α → M
x : β
⊢ (if x ∈ f ⁻¹' s then g (f x) else 1) = if f x ∈ s then g (f x) else 1

Tactic:
split_ifs with h h' h'' <;> first | rfl | contradiction

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : β → α
g : α → M
x : β
h : x ∉ f ⁻¹' s
h'' : f x ∉ s
⊢ 1 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem comp_id (f : R →ₑ+*[φ] S) : f.comp (MulSemiringActionHom.id M) = f :=
  ext fun x => by rw [comp_apply, id_apply]

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
R : Type u_10
inst✝³ : Semiring R
inst✝² : MulSemiringAction M R
S : Type u_12
inst✝¹ : Semiring S
inst✝ : MulSemiringAction N S
f : R →ₑ+*[φ] S
x : R
⊢ (f.comp (MulSemiringActionHom.id M)) x = f x

Tactic:
rw [comp_apply, id_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem ennreal_coeFn_eq_coeFn_toMeasure (ν : ProbabilityMeasure Ω) (s : Set Ω) :
    (ν s : ℝ≥0∞) = (ν : Measure Ω) s

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ ↑(ν s) = ↑ν s

Tactic:
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
  toMeasure_comp_toFiniteMeasure_eq_toMeasure]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_empty (s s' : Set α) : Set.ite ∅ s s' = s'

Proof state:
α : Type u
s s' : Set α
⊢ ∅.ite s s' = s'

Tactic:
simp [Set.ite]

Result:
no goals