harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_sum_of_nonneg {ι : Type*} {a : ℝ} (ha : 0 ≤ a) {s : Finset ι} {f : ι → ℝ}
    (h : ∀ x ∈ s, 0 ≤ f x) : (a ^ ∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x

Proof state:
case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : ∀ x ∈ cons i s hi, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
rw [forall_mem_cons] at h

Result:
case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Proof state:
case empty
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ x ∈ ∅, 0 ≤ f x
⊢ a ^ ∑ x ∈ ∅, f x = ∏ x ∈ ∅, a ^ f x

Tactic:
rw [sum_empty, Finset.prod_empty, rpow_zero]

Result:
no goals

Proof state:
case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]

Result:
no goals

Proof state:
ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h : ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x

Tactic:
induction' s using Finset.cons_induction with i s hi ihs

Result:
case empty
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
h : ∀ x ∈ ∅, 0 ≤ f x
⊢ a ^ ∑ x ∈ ∅, f x = ∏ x ∈ ∅, a ^ f x

case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : ∀ x ∈ cons i s hi, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x
-- Mathlib/Data/Set/Finite/Lattice.lean
lemma map_finite_iInf {F ι : Type*} [CompleteLattice α] [CompleteLattice β] [FunLike F α β]
    [InfTopHomClass F α β] [Finite ι] (f : F) (g : ι → α) :
    f (⨅ i, g i) = ⨅ i, f (g i)

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : InfTopHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨅ x ∈ univ, g x) = ⨅ x ∈ univ, f (g x)

Tactic:
exact map_finite_biInf finite_univ f g

Result:
no goals

Proof state:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : InfTopHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨅ i, g i) = ⨅ i, f (g i)

Tactic:
rw [← iInf_univ (f := g), ← iInf_univ (f := fun i ↦ f (g i))]

Result:
α : Type u
β : Type v
F : Type u_1
ι : Type u_2
inst✝⁴ : CompleteLattice α
inst✝³ : CompleteLattice β
inst✝² : FunLike F α β
inst✝¹ : InfTopHomClass F α β
inst✝ : Finite ι
f : F
g : ι → α
⊢ f (⨅ x ∈ univ, g x) = ⨅ x ∈ univ, f (g x)
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is continuous when `t ≠ ∞`. -/
@[fun_prop]
lemma continuous_truncateToReal {t : ℝ≥0∞} (t_ne_top : t ≠ ∞) : Continuous (truncateToReal t)

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
⊢ Continuous (min t)

Tactic:
fun_prop

Result:
no goals

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
⊢ Continuous t.truncateToReal

Tactic:
apply continuousOn_toReal.comp_continuous (by fun_prop)

Result:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
⊢ ∀ (x : ℝ≥0∞), t ⊓ x ∈ {a | a ≠ ⊤}

Proof state:
t : ℝ≥0∞
t_ne_top : t ≠ ⊤
⊢ ∀ (x : ℝ≥0∞), t ⊓ x ∈ {a | a ≠ ⊤}

Tactic:
simp [t_ne_top]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem diagonalSucc_inv_single_single (g : G) (f : Gⁿ) (a b : k) :
    (diagonalSucc k G n).inv.hom (Finsupp.single g a ⊗ₜ Finsupp.single f b) =
      single (g • partialProd f) (a * b)

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ single (g • partialProd f) ((TensorProduct.lid k k) (a ⊗ₜ[k] b)) = single (g • partialProd f) (a * b)

Tactic:
rfl

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ mapDomain (actionDiagonalSucc G n).inv.hom
      ((lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k))
        ((finsuppTensorFinsupp k k k k G (Fin n → G)) (single g a ⊗ₜ[k] single f b))) =
    single (g • partialProd f) (a * b)

Tactic:
rw [finsuppTensorFinsupp_single, lcongr_single, mapDomain_single, Equiv.refl_apply,
  actionDiagonalSucc_inv_apply]

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ single (g • partialProd f) ((TensorProduct.lid k k) (a ⊗ₜ[k] b)) = single (g • partialProd f) (a * b)

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ (ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single g a ⊗ₜ[k] single f b) = single (g • partialProd f) (a * b)

Tactic:
change mapDomain (actionDiagonalSucc G n).inv.hom
  (lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k)
    (finsuppTensorFinsupp k k k k G (Fin n → G) (single g a ⊗ₜ[k] single f b)))
  = single (g • partialProd f) (a * b)

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
g : G
f : Fin n → G
a b : k
⊢ mapDomain (actionDiagonalSucc G n).inv.hom
      ((lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k))
        ((finsuppTensorFinsupp k k k k G (Fin n → G)) (single g a ⊗ₜ[k] single f b))) =
    single (g • partialProd f) (a * b)
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_eq_contract_apply (x : Module.Dual R M ⊗[R] M) :
    (LinearMap.trace R M) ((dualTensorHom R M M) x) = contractLeft R M x

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
x : Dual R M ⊗[R] M
⊢ (trace R M) ((dualTensorHom R M M) x) = (contractLeft R M) x

Tactic:
rw [← comp_apply, trace_eq_contract]

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem smul_tprod_one_asModule (r : MonoidAlgebra k G) (x : V) (y : W) :
    -- Porting note: required to since Lean 4 doesn't unfold asModule
    let x' : ρV.asModule := x
    let z : (ρV.tprod 1).asModule := x ⊗ₜ y
    r • z = (r • x') ⊗ₜ y

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : MonoidAlgebra k G
x : V
y : W
⊢ ∑ x_1 ∈ r.support, r x_1 • (ρV x_1) x ⊗ₜ[k] y = ∑ a ∈ r.support, (r a • (ρV a) x) ⊗ₜ[k] y

Tactic:
rfl

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : MonoidAlgebra k G
x : V
y : W
⊢ ((ρV ⊗ 1).asAlgebraHom r) (x ⊗ₜ[k] y) = (ρV.asAlgebraHom r) x ⊗ₜ[k] y

Tactic:
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply,
  LinearMap.finsupp_sum_apply, LinearMap.smul_apply, TensorProduct.map_tmul, LinearMap.one_apply]

Result:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • (ρV i) x ⊗ₜ[k] y) = (Finsupp.sum r fun i d => d • (ρV i) x) ⊗ₜ[k] y

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : MonoidAlgebra k G
x : V
y : W
⊢ let x' := x;
  let z := x ⊗ₜ[k] y;
  r • z = (r • x') ⊗ₜ[k] y

Tactic:
show asAlgebraHom (ρV ⊗ 1) _ _ = asAlgebraHom ρV _ _ ⊗ₜ _

Result:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : MonoidAlgebra k G
x : V
y : W
⊢ ((ρV ⊗ 1).asAlgebraHom r) (x ⊗ₜ[k] y) = (ρV.asAlgebraHom r) x ⊗ₜ[k] y

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • (ρV i) x ⊗ₜ[k] y) = (Finsupp.sum r fun i d => d • (ρV i) x) ⊗ₜ[k] y

Tactic:
simp only [Finsupp.sum, TensorProduct.sum_tmul]

Result:
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
r : MonoidAlgebra k G
x : V
y : W
⊢ ∑ x_1 ∈ r.support, r x_1 • (ρV x_1) x ⊗ₜ[k] y = ∑ a ∈ r.support, (r a • (ρV a) x) ⊗ₜ[k] y
-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem iSup_ι_range_eq_top : ⨆ i : ℕ, LinearMap.range (ι Q) ^ i = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ⨆ i, ⨆ j, LinearMap.range (ι Q) ^ ↑j = ⨆ i, LinearMap.range (ι Q) ^ ↑i.snd

Tactic:
rw [iSup_sigma]

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
⊢ ⨆ i, LinearMap.range (ι Q) ^ i = ⊤

Tactic:
rw [← (DirectSum.Decomposition.isInternal (evenOdd Q)).submodule_iSup_eq_top, eq_comm]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ iSup (evenOdd Q) = ⨆ i, LinearMap.range (ι Q) ^ i

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ iSup (evenOdd Q) = ⨆ i, LinearMap.range (ι Q) ^ i

Tactic:
calc
  ⨆ (i : ZMod 2) (j : { n : ℕ // ↑n = i }), LinearMap.range (ι Q) ^ (j : ℕ) =
      ⨆ i : Σ i : ZMod 2, { n : ℕ // ↑n = i }, LinearMap.range (ι Q) ^ (i.2 : ℕ) := by
    rw [iSup_sigma]
  _ = ⨆ i : ℕ, LinearMap.range (ι Q) ^ i :=
    Function.Surjective.iSup_congr (fun i => i.2) (fun i => ⟨⟨_, i, rfl⟩, rfl⟩) fun _ => rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_neg_one : arccos (-1) = π

Proof state:
⊢ arccos (-1) = π

Tactic:
simp [arccos, add_halves]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sInter_apply {x : Class.{u}} {y : ZFSet.{u}} : (⋂₀ x) y ↔ ∀ z : ZFSet.{u}, x z → y ∈ z

Proof state:
x : Class.{u}
y : ZFSet.{u}
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

Tactic:
refine ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, ?_⟩

Result:
x : Class.{u}
y : ZFSet.{u}
⊢ (∀ (z : ZFSet.{u}), x z → y ∈ z) → (⋂₀ x) y

Proof state:
x : Class.{u}
y : ZFSet.{u}
⊢ (∀ (z : ZFSet.{u}), x z → y ∈ z) → (⋂₀ x) y

Tactic:
rintro H - ⟨z, rfl, hxz⟩

Result:
case intro.intro
x : Class.{u}
y : ZFSet.{u}
H : ∀ (z : ZFSet.{u}), x z → y ∈ z
z : ZFSet.{u}
hxz : x z
⊢ y ∈ ↑z

Proof state:
case intro.intro
x : Class.{u}
y : ZFSet.{u}
H : ∀ (z : ZFSet.{u}), x z → y ∈ z
z : ZFSet.{u}
hxz : x z
⊢ y ∈ ↑z

Tactic:
exact H _ hxz

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem finite_support (A : ι → S) (x : DirectSum ι fun i => A i) :
    (Function.support fun i => (x i : M)).Finite

Proof state:
ι : Type v
M : Type u_1
S : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (support fun i => ↑(x i)).Finite

Tactic:
classical
exact (DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)

Result:
no goals

Proof state:
ι : Type v
M : Type u_1
S : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (support fun i => ↑(x i)).Finite

Tactic:
exact (DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)

Result:
no goals
-- Mathlib/Data/Set/BoolIndicator.lean
theorem preimage_boolIndicator_eq_union (t : Set Bool) :
    s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Proof state:
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
split_ifs <;> simp [*]

Result:
no goals

Proof state:
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ x ∈ s.boolIndicator ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
simp only [boolIndicator, mem_preimage]

Result:
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Proof state:
α : Type u_1
s : Set α
t : Set Bool
⊢ s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅

Tactic:
ext x

Result:
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ x ∈ s.boolIndicator ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem coe_setBasisOfLinearIndependentOfCardEqFinrank {s : Set V} [Nonempty s] [Fintype s]
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.toFinset.card = finrank K V) :
    ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = ((↑) : s → V)

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s : Set V
inst✝¹ : Nonempty ↑s
inst✝ : Fintype ↑s
lin_ind : LinearIndependent K Subtype.val
card_eq : s.toFinset.card = finrank K V
⊢ ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯) = Subtype.val

Tactic:
exact Basis.coe_mk _ _

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s : Set V
inst✝¹ : Nonempty ↑s
inst✝ : Fintype ↑s
lin_ind : LinearIndependent K Subtype.val
card_eq : s.toFinset.card = finrank K V
⊢ ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = Subtype.val

Tactic:
rw [setBasisOfLinearIndependentOfCardEqFinrank]

Result:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s : Set V
inst✝¹ : Nonempty ↑s
inst✝ : Fintype ↑s
lin_ind : LinearIndependent K Subtype.val
card_eq : s.toFinset.card = finrank K V
⊢ ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯) = Subtype.val
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjoint_adjoint (A : E →ₗ[𝕜] F) : LinearMap.adjoint (LinearMap.adjoint A) = A

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ adjoint (adjoint A) = A

Tactic:
ext v

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
v : E
⊢ (adjoint (adjoint A)) v = A v

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
v : E
w : F
⊢ ⟪w, (adjoint (adjoint A)) v⟫_𝕜 = ⟪w, A v⟫_𝕜

Tactic:
rw [adjoint_inner_right, adjoint_inner_left]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
v : E
⊢ (adjoint (adjoint A)) v = A v

Tactic:
refine ext_inner_left 𝕜 fun w => ?_

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
v : E
w : F
⊢ ⟪w, (adjoint (adjoint A)) v⟫_𝕜 = ⟪w, A v⟫_𝕜
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
lemma ValuativeCriterion.eq :
    ValuativeCriterion = Existence ⊓ Uniqueness

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion f ↔ (Existence ⊓ Uniqueness) f

Tactic:
exact iff

Result:
no goals

Proof state:
⊢ ValuativeCriterion = Existence ⊓ Uniqueness

Tactic:
ext X Y f

Result:
case h
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion f ↔ (Existence ⊓ Uniqueness) f
-- Mathlib/Topology/Algebra/Order/Field.lean
@[simp]
lemma inv_nhdsGT_zero : (𝓝[>] (0 : 𝕜))⁻¹ = atTop

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ (𝓝[>] 0)⁻¹ = atTop

Tactic:
rw [← inv_atTop₀, inv_inv]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem mapPath_comp {a b : V} (p : Path a b) :
    ∀ {c : V} (q : Path b c), F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)
  | _, Path.nil => rfl
  | c, Path.cons q e => by dsimp; rw [mapPath_comp p q]

Proof state:
V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ F.mapPath (p.comp (q.cons e)) = (F.mapPath p).comp (F.mapPath (q.cons e))

Tactic:
dsimp

Result:
V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ (F.mapPath (p.comp q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)

Proof state:
V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ (F.mapPath (p.comp q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)

Tactic:
rw [mapPath_comp p q]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    (ofList l).getKey? k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ (ofList l).getKey? k = none

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem ae_eq_set_compl {s t : Set α} : sᶜ =ᵐ[μ] t ↔ s =ᵐ[μ] tᶜ

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ sᶜ =ᶠ[ae μ] t ↔ s =ᶠ[ae μ] tᶜ

Tactic:
rw [← ae_eq_set_compl_compl, compl_compl]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux_nil (is : List α) : permutationsAux [] is = []

Proof state:
α : Type u_1
is : List α
⊢ [].permutationsAux is = []

Tactic:
rw [permutationsAux, permutationsAux.rec]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Dense.borel_eq_generateFrom_Ioc_mem {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMaxOrder α] {s : Set α}
    (hd : Dense s) :
    borel α = .generateFrom { S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S } :=
  hd.borel_eq_generateFrom_Ioc_mem_aux (by simp) fun _ _ hxy H =>
    ((nonempty_Ioo.2 hxy).ne_empty H).elim

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : SecondCountableTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
s : Set α
hd : Dense s
⊢ ∀ (x : α), IsTop x → x ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_shiftConcat_zero {x : BitVec w} (b : Bool) (h : 0 < w) :
    (x.shiftConcat b)[0] = b

Proof state:
w : Nat
x : BitVec w
b : Bool
h : 0 < w
⊢ (x.shiftConcat b)[0] = b

Tactic:
simp [getElem_shiftConcat]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem inner_indicatorConstLp_one (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (f : Lp 𝕜 2 μ) :
    ⟪indicatorConstLp 2 hs hμs (1 : 𝕜), f⟫ = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
𝕜 : Type u_4
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp 𝕜 2 μ)
⊢ inner (indicatorConstLp 2 hs hμs 1) f = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
rw [L2.inner_indicatorConstLp_eq_inner_setIntegral 𝕜 hs hμs (1 : 𝕜) f]

Result:
α : Type u_1
𝕜 : Type u_4
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp 𝕜 2 μ)
⊢ inner 1 (∫ (x : α) in s, ↑↑f x ∂μ) = ∫ (x : α) in s, ↑↑f x ∂μ

Proof state:
α : Type u_1
𝕜 : Type u_4
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp 𝕜 2 μ)
⊢ inner 1 (∫ (x : α) in s, ↑↑f x ∂μ) = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
@[simp]
lemma norm_le_one_of_discrete
    (x : 𝕜) : ‖x‖ ≤ 1

Proof state:
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ ≤ 1

Tactic:
rcases eq_or_ne x 0 with rfl|hx

Result:
case inl
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
⊢ ‖0‖ ≤ 1

case inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ ≤ 1

Proof state:
case inl
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
⊢ ‖0‖ ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case inr
𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ ≤ 1

Tactic:
simp [norm_eq_one_iff_ne_zero_of_discrete.mpr hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂)

Proof state:
α : Sort u
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ (a₁ = b₁) = (a₂ = b₂)

Tactic:
rw [h₁, h₂, Eq.comm (a := a₂)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_eq_fallback [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β}
    (h : containsKey a l = false) : getValueD a l fallback = fallback

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
fallback : β
h : containsKey a l = false
⊢ getValueD a l fallback = fallback

Tactic:
rw [containsKey_eq_isSome_getValue?, Bool.eq_false_iff, ne_eq, Option.not_isSome_iff_eq_none] at h

Result:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
fallback : β
h : getValue? a l = none
⊢ getValueD a l fallback = fallback

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
fallback : β
h : getValue? a l = none
⊢ getValueD a l fallback = fallback

Tactic:
rw [getValueD_eq_getValue?, h, Option.getD_none]

Result:
no goals