harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_flatMap {β} (l : Vector α n) (f : α → Vector β m) :
    (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f)

Proof state:
α : Type u_1
n m : Nat
β : Type u_2
l : Vector α n
f : α → Vector β m
⊢ (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
β : Type u_2
f : α → Vector β m
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.flatMap f).reverse =
    { toArray := l, size_toArray := ⋯ }.reverse.flatMap (reverse ∘ f)

Proof state:
case mk
α : Type u_1
m : Nat
β : Type u_2
f : α → Vector β m
l : Array α
⊢ ({ toArray := l, size_toArray := ⋯ }.flatMap f).reverse =
    { toArray := l, size_toArray := ⋯ }.reverse.flatMap (reverse ∘ f)

Tactic:
simp [Array.reverse_flatMap, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ENormedSpace.lean
theorem map_zero : e 0 = 0

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
⊢ ↑e 0 = 0

Tactic:
rw [← zero_smul 𝕜 (0 : V), e.map_smul]

Result:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
⊢ ↑‖0‖₊ * ↑e 0 = 0

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
⊢ ↑‖0‖₊ * ↑e 0 = 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_mul_eq_one : a⁻¹ * b = 1 ↔ a = b

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a⁻¹ * b = 1 ↔ a = b

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} (hab : a == b) :
    get? m a = get? m b

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a b : α
hab : (a == b) = true
⊢ get? m a = get? m b

Tactic:
simp_to_model using List.getValue?_congr

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem isOpenEmbedding_iff_restrictPreimage (h : Continuous f) :
    IsOpenEmbedding f ↔ ∀ i, IsOpenEmbedding ((U i).1.restrictPreimage f)

Proof state:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsOpen (range f) ↔ ∀ (x : ι), IsOpen (Subtype.val ⁻¹' range f)

Tactic:
exact hU.isOpen_iff_coe_preimage

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

Tactic:
exact hU.isEmbedding_iff_restrictPreimage h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsOpenEmbedding f ↔ ∀ (i : ι), IsOpenEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [isOpenEmbedding_iff, forall_and]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ∧ IsOpen (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsOpen (range ((U x).carrier.restrictPreimage f))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ∧ IsOpen (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsOpen (range ((U x).carrier.restrictPreimage f))

Tactic:
apply and_congr

Result:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsOpen (range f) ↔ ∀ (x : ι), IsOpen (range ((U x).carrier.restrictPreimage f))

Proof state:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsOpen (range f) ↔ ∀ (x : ι), IsOpen (range ((U x).carrier.restrictPreimage f))

Tactic:
simp_rw [range_restrictPreimage]

Result:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsOpen (range f) ↔ ∀ (x : ι), IsOpen (Subtype.val ⁻¹' range f)
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.const_mul (c : 𝔸) (hd : HasStrictDerivAt d d' x) :
    HasStrictDerivAt (fun y => c * d y) (c * d') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt (fun y => c * d y) (c * d') x

Tactic:
convert (hasStrictDerivAt_const _ _).mul hd using 1

Result:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ c * d' = 0 * d x + c * d'

Proof state:
case h.e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ c * d' = 0 * d x + c * d'

Tactic:
rw [zero_mul, zero_add]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean
theorem range_toProdMulOpposite :
    Set.range toProdMulOpposite =
      { lr : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ | ∀ x y, unop lr.2 x * y = x * lr.1 y } :=
  Set.ext fun x =>
    ⟨by
      rintro ⟨a, rfl⟩
      exact a.central, fun hx => ⟨⟨(x.1, unop x.2), hx⟩, Prod.ext rfl rfl⟩⟩

Proof state:
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProdMulOpposite ∈ {lr | ∀ (x y : A), (unop lr.2) x * y = x * lr.1 y}

Tactic:
exact a.central

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
x : (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ
⊢ x ∈ Set.range toProdMulOpposite → x ∈ {lr | ∀ (x y : A), (unop lr.2) x * y = x * lr.1 y}

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
⊢ a.toProdMulOpposite ∈ {lr | ∀ (x y : A), (unop lr.2) x * y = x * lr.1 y}
-- Mathlib/Data/Complex/Trigonometric.lean
theorem ofReal_cos_ofReal_re (x : ℝ) : ((cos x).re : ℂ) = cos x :=
  conj_eq_iff_re.1 <| by rw [← cos_conj, conj_ofReal]

Proof state:
x : ℝ
⊢ (starRingEnd ℂ) (cos ↑x) = cos ↑x

Tactic:
rw [← cos_conj, conj_ofReal]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mdifferentiableAt_neg :
    MDifferentiableAt I 𝓘(𝕜, E') (-f) z ↔ MDifferentiableAt I 𝓘(𝕜, E') f z :=
  ⟨fun hf => by convert hf.neg; rw [neg_neg], fun hf => hf.neg⟩

Proof state:
case h.e'_21
𝕜 : 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'
z : M
f : M → E'
hf : MDifferentiableAt I 𝓘(𝕜, E') (-f) z
⊢ f = - -f

Tactic:
rw [neg_neg]

Result:
no goals

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'
z : M
f : M → E'
hf : MDifferentiableAt I 𝓘(𝕜, E') (-f) z
⊢ MDifferentiableAt I 𝓘(𝕜, E') f z

Tactic:
convert hf.neg

Result:
case h.e'_21
𝕜 : 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'
z : M
f : M → E'
hf : MDifferentiableAt I 𝓘(𝕜, E') (-f) z
⊢ f = - -f
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem biUnion_coe_eq_coe (I : WithBot (Box ι)) :
    ⋃ (J : Box ι) (_ : ↑J = I), (J : Set (ι → ℝ)) = I

Proof state:
ι : Type u_1
I : WithBot (Box ι)
⊢ ⋃ J, ⋃ (_ : ↑J = I), ↑J = ↑I

Tactic:
induction I <;> simp [WithBot.coe_eq_coe]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem I_pow_four : I ^ 4 = 1

Proof state:
⊢ 4 = 2 * 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ I ^ 4 = 1

Tactic:
rw [(by norm_num : 4 = 2 * 2), pow_mul, I_sq, neg_one_sq]

Result:
no goals
-- Mathlib/Analysis/VonNeumannAlgebra/Basic.lean
theorem mem_commutant_iff {S : VonNeumannAlgebra H} {z : H →L[ℂ] H} :
    z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g

Proof state:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ (↑S).centralizer ↔ ∀ g ∈ S, g * z = z * g

Tactic:
rfl

Result:
no goals

Proof state:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g

Tactic:
rw [← SetLike.mem_coe, coe_commutant]

Result:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ (↑S).centralizer ↔ ∀ g ∈ S, g * z = z * g
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma rewrites_reverse_comm : r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
u v : List (Symbol T N)
⊢ r.reverse.Rewrites u v ↔ r.Rewrites u.reverse v.reverse

Tactic:
rw [← rewrites_reverse, reverse_reverse]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
theorem map_π_preserves_coequalizer_inv_desc {W : D} (k : G.obj Y ⟶ W)
    (wk : G.map f ≫ k = G.map g ≫ k) : G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫ coequalizer.desc k wk = k

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv ≫ coequalizer.desc k wk = k

Tactic:
rw [← Category.assoc, map_π_preserves_coequalizer_inv, coequalizer.π_desc]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_map_equiv (f : α ≃ᵐ δ) (g : δ → β) :
    Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α ≃ᵐ δ
g : δ → β
⊢ Integrable g (Measure.map (⇑f) μ) ↔ Integrable (g ∘ ⇑f) μ

Tactic:
simp_rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α ≃ᵐ δ
g : δ → β
⊢ MemLp g 1 (Measure.map (⇑f) μ) ↔ MemLp (g ∘ ⇑f) 1 μ

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α ≃ᵐ δ
g : δ → β
⊢ MemLp g 1 (Measure.map (⇑f) μ) ↔ MemLp (g ∘ ⇑f) 1 μ

Tactic:
exact f.memLp_map_measure_iff

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem UniformSpace.comap_comap {α β γ} {uγ : UniformSpace γ} {f : α → β} {g : β → γ} :
    UniformSpace.comap (g ∘ f) uγ = UniformSpace.comap f (UniformSpace.comap g uγ)

Proof state:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ 𝓤 α = 𝓤 α

Tactic:
simp only [uniformity_comap, Filter.comap_comap, Prod.map_comp_map]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ comap (g ∘ f) uγ = comap f (comap g uγ)

Tactic:
ext1

Result:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ 𝓤 α = 𝓤 α
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_sub {x : ℝ≥0∞} (y z : ℝ) (hx : x ≠ 0) (h'x : x ≠ ⊤) : x ^ (y - z) = x ^ y / x ^ z

Proof state:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ⊤
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
rw [sub_eq_add_neg, rpow_add _ _ hx h'x, rpow_neg, div_eq_mul_inv]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem card_units (p : ℕ) [Fact p.Prime] : Fintype.card (ZMod p)ˣ = p - 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rw [Fintype.card_units, card]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma eq_one_of_mul_eq_one_left (H : m * n = 1) : n = 1 :=
  eq_one_of_mul_eq_one_right (n := m) (by rwa [Nat.mul_comm])

Proof state:
m n : ℕ
H : m * n = 1
⊢ n * m = 1

Tactic:
rwa [Nat.mul_comm]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iio_filter_lt {α} [LinearOrder α] [LocallyFiniteOrderBot α] (a b : α) :
    {x ∈ Iio a | x < b} = Iio (min a b)

Proof state:
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ filter (fun x => x < b) (Iio a) = Iio (a ⊓ b)

Tactic:
ext

Result:
case h
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b a✝ : α
⊢ a✝ ∈ filter (fun x => x < b) (Iio a) ↔ a✝ ∈ Iio (a ⊓ b)

Proof state:
case h
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrderBot α
a b a✝ : α
⊢ a✝ ∈ filter (fun x => x < b) (Iio a) ↔ a✝ ∈ Iio (a ⊓ b)

Tactic:
simp [and_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Center.lean
theorem rightUnitor_inv_f (X : Center C) : Hom.f (ρ_ X).inv = (ρ_ X.1).inv

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (X ⊗ 𝟙_ (Center C))).f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst

Tactic:
rfl

Result:
no goals

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (ρ_ X.fst).hom ≫ (ρ_ X).inv.f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst

Tactic:
rw [← rightUnitor_hom_f, ← comp_f, Iso.hom_inv_id]

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (𝟙 (X ⊗ 𝟙_ (Center C))).f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (ρ_ X).inv.f = (ρ_ X.fst).inv

Tactic:
apply Iso.inv_ext'

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (ρ_ X.fst).hom ≫ (ρ_ X).inv.f = 𝟙 (X ⊗ 𝟙_ (Center C)).fst
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_permute_rows (σ : Perm n) (M : Matrix n n R) :
    (M.submatrix id σ).permanent = M.permanent

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
σ : Perm n
M : Matrix n n R
⊢ (M.submatrix id ⇑σ).permanent = M.permanent

Tactic:
rw [← permanent_transpose, transpose_submatrix, permanent_permute_cols, permanent_transpose]

Result:
no goals
-- Mathlib/Topology/LocallyFinite.lean
theorem closure (hf : LocallyFinite f) : LocallyFinite fun i => closure (f i)

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
⊢ ∃ t ∈ 𝓝 x, {i | ((fun i => closure (f i)) i ∩ t).Nonempty}.Finite

Tactic:
rcases hf x with ⟨s, hsx, hsf⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : {i | (f i ∩ s).Nonempty}.Finite
⊢ ∃ t ∈ 𝓝 x, {i | ((fun i => closure (f i)) i ∩ t).Nonempty}.Finite

Proof state:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : {i | (f i ∩ s).Nonempty}.Finite
⊢ ∃ t ∈ 𝓝 x, {i | ((fun i => closure (f i)) i ∩ t).Nonempty}.Finite

Tactic:
refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : {i | (f i ∩ s).Nonempty}.Finite
i : ι
hi : i ∈ {i | ((fun i => closure (f i)) i ∩ interior s).Nonempty}
⊢ i ∈ {i | (f i ∩ s).Nonempty}

Proof state:
case intro.intro
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : {i | (f i ∩ s).Nonempty}.Finite
i : ι
hi : i ∈ {i | ((fun i => closure (f i)) i ∩ interior s).Nonempty}
⊢ i ∈ {i | (f i ∩ s).Nonempty}

Tactic:
exact (hi.mono isOpen_interior.closure_inter).of_closure.mono
  (inter_subset_inter_right _ interior_subset)

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ LocallyFinite fun i => closure (f i)

Tactic:
intro x

Result:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
⊢ ∃ t ∈ 𝓝 x, {i | ((fun i => closure (f i)) i ∩ t).Nonempty}.Finite
-- Mathlib/Data/Real/Irrational.lean
theorem of_neg (h : Irrational (-x)) : Irrational x := fun ⟨q, hx⟩ => h ⟨-q, by rw [cast_neg, hx]⟩

Proof state:
x : ℝ
h : Irrational (-x)
x✝ : x ∈ Set.range Rat.cast
q : ℚ
hx : ↑q = x
⊢ ↑(-q) = -x

Tactic:
rw [cast_neg, hx]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹

Proof state:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

Tactic:
simp [nonsing_inv_apply_not_isUnit _ h]

Result:
no goals

Proof state:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

Tactic:
rw [nonsing_inv_nonsing_inv _ h]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

Tactic:
by_cases h : IsUnit A.det

Result:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹⁻¹⁻¹ = A⁻¹

case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
-- Mathlib/Computability/Primrec.lean
theorem list_findIdx₁ {p : α → β → Bool} (hp : Primrec₂ p) :
    ∀ l : List β, Primrec fun a => l.findIdx (p a)
| [] => const 0
| a :: l => (cond (hp.comp .id (const a)) (const 0) (succ.comp (list_findIdx₁ hp l))).of_eq fun n =>
  by simp [List.findIdx_cons]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
p : α → β → Bool
hp : Primrec₂ p
a : β
l : List β
n : α
⊢ (bif p (id n) a then 0 else (List.findIdx (p n) l).succ) = List.findIdx (p n) (a :: l)

Tactic:
simp [List.findIdx_cons]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
@[simp] lemma card_eq_top : card α = ⊤ ↔ Infinite α

Proof state:
α : Type u_1
⊢ card α = ⊤ ↔ Infinite α

Tactic:
simp [card, aleph0_le_mk_iff]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_single_ne {i j : ι} (x : β i) (h : i ≠ j) : (single i x).erase j = single i x

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
x : β i
h : i ≠ j
⊢ erase j (single i x) = single i x

Tactic:
rw [erase_single, if_neg h]

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_eq_zero_iff : egauge 𝕜 s x = 0 ↔ ∃ᶠ c : 𝕜 in 𝓝 0, x ∈ c • s

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ egauge 𝕜 s x = 0 ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s

Tactic:
refine (iInf₂_eq_bot _).trans ?_

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ (∀ b > ⊥, ∃ i, ∃ (_ : x ∈ i • s), ‖i‖ₑ < b) ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ (∀ b > ⊥, ∃ i, ∃ (_ : x ∈ i • s), ‖i‖ₑ < b) ↔
    ∀ (i : ℝ≥0∞), 0 < i → ∃ x_1 ∈ {y | (y, 0) ∈ {p | edist p.1 p.2 < i}}, x ∈ x_1 • s

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ (∀ b > ⊥, ∃ i, ∃ (_ : x ∈ i • s), ‖i‖ₑ < b) ↔ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • s

Tactic:
rw [(nhds_basis_uniformity uniformity_basis_edist).frequently_iff]

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ (∀ b > ⊥, ∃ i, ∃ (_ : x ∈ i • s), ‖i‖ₑ < b) ↔
    ∀ (i : ℝ≥0∞), 0 < i → ∃ x_1 ∈ {y | (y, 0) ∈ {p | edist p.1 p.2 < i}}, x ∈ x_1 • s
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_right [DecidableEq β] (h : s.Nonempty) : image₂ (fun _ y => y) s t = t :=
  coe_injective <| by
    push_cast
    exact image2_right h

Proof state:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq β
h : s.Nonempty
⊢ ↑(image₂ (fun x y => y) s t) = ↑t

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq β
h : s.Nonempty
⊢ image2 (fun x y => y) ↑s ↑t = ↑t

Proof state:
α : Type u_1
β : Type u_3
s : Finset α
t : Finset β
inst✝ : DecidableEq β
h : s.Nonempty
⊢ image2 (fun x y => y) ↑s ↑t = ↑t

Tactic:
exact image2_right h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem _root_.MeasurableEmbedding.integrableOn_map_iff [MeasurableSpace β] {e : α → β}
    (he : MeasurableEmbedding e) {f : β → E} {μ : Measure α} {s : Set β} :
    IntegrableOn f s (μ.map e) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure α
s : Set β
⊢ IntegrableOn f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Tactic:
simp_rw [IntegrableOn, he.restrict_map, he.integrable_map_iff]

Result:
no goals