harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem rightHom_comp_inl : (rightHom : N ⋊[φ] G →* G).comp inl = 1

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
⊢ rightHom.comp inl = 1

Tactic:
ext

Result:
case h
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : N
⊢ (rightHom.comp inl) x✝ = 1 x✝

Proof state:
case h
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : N
⊢ (rightHom.comp inl) x✝ = 1 x✝

Tactic:
simp [rightHom]

Result:
no goals
-- Mathlib/Topology/Bases.lean
lemma IsSeparable.prod {β : Type*} [TopologicalSpace β]
    {s : Set α} {t : Set β} (hs : IsSeparable s) (ht : IsSeparable t) :
    IsSeparable (s ×ˢ t)

Proof state:
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsSeparable s
ht : IsSeparable t
⊢ IsSeparable (s ×ˢ t)

Tactic:
rcases hs with ⟨cs, cs_count, hcs⟩

Result:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
ht : IsSeparable t
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
⊢ IsSeparable (s ×ˢ t)

Proof state:
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure ct
⊢ s ×ˢ t ⊆ closure cs ×ˢ closure ct

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
ht : IsSeparable t
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
⊢ IsSeparable (s ×ˢ t)

Tactic:
rcases ht with ⟨ct, ct_count, hct⟩

Result:
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure ct
⊢ IsSeparable (s ×ˢ t)

Proof state:
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure ct
⊢ s ×ˢ t ⊆ closure (cs ×ˢ ct)

Tactic:
rw [closure_prod_eq]

Result:
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure ct
⊢ s ×ˢ t ⊆ closure cs ×ˢ closure ct

Proof state:
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure ct
⊢ IsSeparable (s ×ˢ t)

Tactic:
refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩

Result:
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure ct
⊢ s ×ˢ t ⊆ closure (cs ×ˢ ct)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_toList {α n} (xs : Vector α n) (i : Nat) :
    xs.toList[i]? = xs[i]?

Proof state:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList[i]? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
i : Nat
⊢ xs.toList[i]? = xs[i]?

Tactic:
cases xs

Result:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toList[i]? =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]?
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem dvd_lcm_right (x y : R) : y ∣ lcm x y :=
  by_cases
    (fun hxy : gcd x y = 0 => by
      rw [lcm, hxy, div_zero]
      exact dvd_zero _)
    fun hxy =>
    let ⟨z, hz⟩ := (gcd_dvd x y).1
    ⟨z, Eq.symm <| eq_div_of_mul_eq_right hxy <| by rw [← mul_assoc, mul_right_comm, ← hz]⟩

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ lcm x y

Tactic:
rw [lcm, hxy, div_zero]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
⊢ gcd x y * (y * z) = x * y

Tactic:
rw [← mul_assoc, mul_right_comm, ← hz]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- A trivial block is a block. -/
@[to_additive "A trivial block is a block."]
lemma IsTrivialBlock.isBlock (hB : IsTrivialBlock B) : IsBlock G B

Proof state:
case inr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsBlock G univ

Tactic:
exact .univ

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : B.Subsingleton
⊢ IsBlock G B

Tactic:
exact .of_subsingleton hB

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsTrivialBlock B
⊢ IsBlock G B

Tactic:
obtain hB | rfl := hB

Result:
case inl
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : B.Subsingleton
⊢ IsBlock G B

case inr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsBlock G univ
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_nonneg_iff_abs_toReal_le_pi_div_two {θ : Angle} : 0 ≤ cos θ ↔ |θ.toReal| ≤ π / 2

Proof state:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2) ∨ π / 2 < θ.toReal
⊢ Real.cos θ.toReal < 0

Tactic:
rcases hn with (hn | hn)

Result:
case inl
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2)
⊢ Real.cos θ.toReal < 0

case inr
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : π / 2 < θ.toReal
⊢ Real.cos θ.toReal < 0

Proof state:
case inl
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2)
⊢ -θ.toReal < π + π / 2

Tactic:
linarith [neg_pi_lt_toReal θ]

Result:
no goals

Proof state:
θ : Angle
⊢ 0 ≤ (↑θ.toReal).cos ↔ |θ.toReal| ≤ π / 2

Tactic:
rw [abs_le, cos_coe]

Result:
θ : Angle
⊢ 0 ≤ Real.cos θ.toReal ↔ -(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2

Proof state:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2) ∨ π / 2 < θ.toReal
⊢ False

Tactic:
refine (not_lt.2 h) ?_

Result:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2) ∨ π / 2 < θ.toReal
⊢ Real.cos θ.toReal < 0

Proof state:
case inl
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2)
⊢ Real.cos (-θ.toReal) < 0

Tactic:
refine cos_neg_of_pi_div_two_lt_of_lt (by linarith) ?_

Result:
case inl
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2)
⊢ -θ.toReal < π + π / 2

Proof state:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2)
⊢ π / 2 < -θ.toReal

Tactic:
linarith

Result:
no goals

Proof state:
case inr
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : π / 2 < θ.toReal
⊢ Real.cos θ.toReal < 0

Tactic:
refine cos_neg_of_pi_div_two_lt_of_lt hn ?_

Result:
case inr
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : π / 2 < θ.toReal
⊢ θ.toReal < π + π / 2

Proof state:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : ¬(-(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2)
⊢ False

Tactic:
rw [not_and_or, not_le, not_le] at hn

Result:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2) ∨ π / 2 < θ.toReal
⊢ False

Proof state:
θ : Angle
⊢ 0 ≤ Real.cos θ.toReal ↔ -(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2

Tactic:
refine ⟨fun h => ?_, cos_nonneg_of_mem_Icc⟩

Result:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
⊢ -(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2

Proof state:
case inl
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2)
⊢ Real.cos θ.toReal < 0

Tactic:
rw [← Real.cos_neg]

Result:
case inl
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : θ.toReal < -(π / 2)
⊢ Real.cos (-θ.toReal) < 0

Proof state:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
⊢ -(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2

Tactic:
by_contra hn

Result:
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : ¬(-(π / 2) ≤ θ.toReal ∧ θ.toReal ≤ π / 2)
⊢ False

Proof state:
case inr
θ : Angle
h : 0 ≤ Real.cos θ.toReal
hn : π / 2 < θ.toReal
⊢ θ.toReal < π + π / 2

Tactic:
linarith [toReal_le_pi θ]

Result:
no goals

Proof state:
θ : Angle
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
nth_rw 1 [← coe_toReal θ]

Result:
θ : Angle
⊢ 0 ≤ (↑θ.toReal).cos ↔ |θ.toReal| ≤ π / 2
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_iSup {ι : Sort*} (s : ι → X.Opens) :
    (f ''ᵁ ⨆ (i : ι), s i) = ⨆ (i : ι), f ''ᵁ s i

Proof state:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ ↑(f ''ᵁ ⨆ i, s i) = ↑(⨆ i, f ''ᵁ s i)

Tactic:
simp [Set.image_iUnion]

Result:
no goals

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ f ''ᵁ ⨆ i, s i = ⨆ i, f ''ᵁ s i

Tactic:
ext : 1

Result:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ ↑(f ''ᵁ ⨆ i, s i) = ↑(⨆ i, f ''ᵁ s i)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem mem_iff_getEntry?_eq_some [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
    {p : (a : α) × β a} (h : DistinctKeys l) : p ∈ l ↔ getEntry? p.1 l = some p

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
h : DistinctKeys []
⊢ p ∈ [] ↔ getEntry? p.fst [] = some p

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
p : (a : α) × β a
h : DistinctKeys l
⊢ p ∈ l ↔ getEntry? p.fst l = some p

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
h : DistinctKeys []
⊢ p ∈ [] ↔ getEntry? p.fst [] = some p

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : DistinctKeys tail✝ → (p ∈ tail✝ ↔ getEntry? p.fst tail✝ = some p)
h : DistinctKeys (⟨k✝, v✝⟩ :: tail✝)
⊢ p ∈ ⟨k✝, v✝⟩ :: tail✝ ↔ getEntry? p.fst (⟨k✝, v✝⟩ :: tail✝) = some p

Proof state:
case refine_1.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
hk : getEntry? p.fst t = some p
⊢ (k == p.fst) = false

Tactic:
refine Bool.eq_false_iff.2 fun hcon => Bool.false_ne_true ?_

Result:
case refine_1.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
hk : getEntry? p.fst t = some p
hcon : (k == p.fst) = true
⊢ false = true
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_nsmul (n : ℕ) (A : Matrix m m 𝔸) : exp 𝕂 (n • A) = exp 𝕂 A ^ n

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (n • A) = exp 𝕂 A ^ n

Tactic:
exact exp_nsmul n A

Result:
no goals

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
⊢ exp 𝕂 (n • A) = exp 𝕂 A ^ n

Tactic:
letI : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (n • A) = exp 𝕂 A ^ n

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (n • A) = exp 𝕂 A ^ n

Tactic:
letI : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (n • A) = exp 𝕂 A ^ n

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (n • A) = exp 𝕂 A ^ n

Tactic:
letI : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
n : ℕ
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (n • A) = exp 𝕂 A ^ n
-- Mathlib/Order/Defs/LinearOrder.lean
lemma max_le (h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
h : ¬a ≤ b
⊢ max a b ≤ c

Tactic:
simpa [max_def, if_neg h] using h₁

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
⊢ max a b ≤ c

Tactic:
if h : a ≤ b
then simpa [max_def, if_pos h] using h₂
else simpa [max_def, if_neg h] using h₁

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a ≤ c
h₂ : b ≤ c
h : a ≤ b
⊢ max a b ≤ c

Tactic:
simpa [max_def, if_pos h] using h₂

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_castAdd_natAdd {f : Fin (m + n) → α} :
    append (fun i ↦ f (castAdd n i)) (fun i ↦ f (natAdd m i)) = f

Proof state:
m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (fun i =>
      if hi : ↑i < m then ⋯ ▸ (fun i => f (castAdd n i)) (i.castLT hi)
      else ⋯ ▸ (fun i => f (natAdd m i)) (subNat m (Fin.cast ⋯ i) ⋯)) =
    f

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (append (fun i => f (castAdd n i)) fun i => f (natAdd m i)) = f

Tactic:
unfold append addCases

Result:
m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (fun i =>
      if hi : ↑i < m then ⋯ ▸ (fun i => f (castAdd n i)) (i.castLT hi)
      else ⋯ ▸ (fun i => f (natAdd m i)) (subNat m (Fin.cast ⋯ i) ⋯)) =
    f
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem disjoint_ball_closedBall_iff (hδ : 0 < δ) (hε : 0 ≤ ε) :
    Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < δ + ε
⊢ False

Tactic:
rw [add_comm] at hxy

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
⊢ False

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y ≤ ε
⊢ False

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
rw [dist_comm] at hxz

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y ≤ ε
⊢ False

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
⊢ Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y

Tactic:
refine ⟨fun h => le_of_not_lt fun hxy => ?_, ball_disjoint_closedBall⟩

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < δ + ε
⊢ False
-- Mathlib/MeasureTheory/Constructions/Pi.lean
lemma pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpace (β i)]
    (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] :
    ((Measure.pi fun i ↦ μ (some i)).prod (μ none)).map
      (MeasurableEquiv.piOptionEquivProd β).symm = Measure.pi μ

Proof state:
case h
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
⊢ x ∈ ⇑e_meas ⁻¹' univ.pi s ↔ x ∈ (univ.pi fun i => s (some i)) ×ˢ s none

Tactic:
simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, mem_prod]

Result:
case h
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
⊢ (∀ (i : Option ι), e_meas x i ∈ s i) ↔ (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none

Proof state:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)

Tactic:
let e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) :=
  MeasurableEquiv.piOptionEquivProd β |>.symm

Result:
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
⊢ (map (⇑(MeasurableEquiv.piOptionEquivProd β).symm) ((Measure.pi fun i => μ (some i)).prod (μ none))) (univ.pi s) =
    ∏ i : Option ι, (μ i) (s i)

Proof state:
case h
ι : Type u_1
inst✝² : Fintype ι
β : Option ι → Type u_4
inst✝¹ : (i : Option ι) → MeasurableSpace (β i)
μ : (i : Option ι) → Measure (β i)
inst✝ : ∀ (i : Option ι), SigmaFinite (μ i)
s : (i : Option ι) → Set (β i)
x✝¹ : ∀ (i : Option ι), MeasurableSet (s i)
e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := (MeasurableEquiv.piOptionEquivProd β).symm
me : MeasurableEmbedding ⇑e_meas
x : ((i : ι) → β (some i)) × β none
x✝ : (∀ (i : ι), x.1 i ∈ s (some i)) ∧ x.2 ∈ s none
i : Option ι
⊢ e_meas x i ∈ s i

Tactic:
rcases i <;> tauto

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem isoRestrict_hom_ofRestrict : (isoRestrict f).hom ≫ Y.ofRestrict _ = f

Proof state:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ SheafedSpace.forgetToPresheafedSpace.preimage (PresheafedSpace.IsOpenImmersion.isoRestrict f.toHom).hom ≫
      Hom.toShHom (Y.ofRestrict ⋯) =
    Hom.toShHom f

Tactic:
apply SheafedSpace.forgetToPresheafedSpace.map_injective

Result:
case h.a
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ SheafedSpace.forgetToPresheafedSpace.map
      (SheafedSpace.forgetToPresheafedSpace.preimage (PresheafedSpace.IsOpenImmersion.isoRestrict f.toHom).hom ≫
        Hom.toShHom (Y.ofRestrict ⋯)) =
    SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f)

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f

Tactic:
ext1

Result:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Hom.toShHom ((isoRestrict f).hom ≫ Y.ofRestrict ⋯) = Hom.toShHom f

Proof state:
case h.a
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (PresheafedSpace.IsOpenImmersion.isoRestrict f.toHom).hom ≫
      SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom (Y.ofRestrict ⋯)) =
    SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f)

Tactic:
exact SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f.1

Result:
no goals

Proof state:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Hom.toShHom ((isoRestrict f).hom ≫ Y.ofRestrict ⋯) = Hom.toShHom f

Tactic:
dsimp [isoRestrict, isoOfSheafedSpaceIso]

Result:
case h
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ SheafedSpace.forgetToPresheafedSpace.preimage (PresheafedSpace.IsOpenImmersion.isoRestrict f.toHom).hom ≫
      Hom.toShHom (Y.ofRestrict ⋯) =
    Hom.toShHom f

Proof state:
case h.a
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ SheafedSpace.forgetToPresheafedSpace.map
      (SheafedSpace.forgetToPresheafedSpace.preimage (PresheafedSpace.IsOpenImmersion.isoRestrict f.toHom).hom ≫
        Hom.toShHom (Y.ofRestrict ⋯)) =
    SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f)

Tactic:
rw [Functor.map_comp, SheafedSpace.forgetToPresheafedSpace.map_preimage]

Result:
case h.a
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (PresheafedSpace.IsOpenImmersion.isoRestrict f.toHom).hom ≫
      SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom (Y.ofRestrict ⋯)) =
    SheafedSpace.forgetToPresheafedSpace.map (Hom.toShHom f)