harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Mul.lean
lemma mulVec_injective_of_isUnit [Fintype m] [DecidableEq m] {A : Matrix m m R}
    (ha : IsUnit A) : Function.Injective A.mulVec

Proof state:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
⊢ Function.Injective A.mulVec

Tactic:
intro x y hxy

Result:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
x y : m → R
hxy : A *ᵥ x = A *ᵥ y
⊢ x = y

Proof state:
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
⊢ Function.Injective A.mulVec

Tactic:
obtain ⟨B, hBl, hBr⟩ := isUnit_iff_exists.mp ha

Result:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
⊢ Function.Injective A.mulVec

Proof state:
case intro.intro
m : Type u_2
R : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m R
ha : IsUnit A
B : Matrix m m R
hBl : A * B = 1
hBr : B * A = 1
x y : m → R
hxy : A *ᵥ x = A *ᵥ y
⊢ x = y

Tactic:
simpa [hBr] using congrArg B.mulVec hxy

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem shiftLeft_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
    (h : y &&& z = 0#w₂) :
    x <<< (y ||| z) = x <<< y <<< z

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y z : BitVec w₂
h : y &&& z = 0#w₂
⊢ x <<< (y ||| z) = x <<< y <<< z

Tactic:
rw [← add_eq_or_of_and_eq_zero _ _ h,
  shiftLeft_eq', toNat_add_of_and_eq_zero h]

Result:
w₁ w₂ : Nat
x : BitVec w₁
y z : BitVec w₂
h : y &&& z = 0#w₂
⊢ x <<< (y.toNat + z.toNat) = x <<< y <<< z

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y z : BitVec w₂
h : y &&& z = 0#w₂
⊢ x <<< (y.toNat + z.toNat) = x <<< y <<< z

Tactic:
simp [shiftLeft_add]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_add_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → α) :
    ∏ i ∈ s, (f i + g i) =
      (∏ i ∈ s, f i) +
        ∑ i ∈ s, g i * (∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j

Proof state:
case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ g a * ∏ i ∈ s, f i +
      g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j =
    (g a * ∏ i ∈ s, f i +
        g a * ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j) *
      ∏ j ∈ filter (fun j => a < j) (insert a s), f j

Tactic:
rw [filter_false_of_mem, prod_empty, mul_one]

Result:
case e_a.e_a
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
ha' : a ∉ s
⊢ ∀ x ∈ insert a s, ¬a < x

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
⊢ ∀ (a : ι) (s : Finset ι),
    (∀ x ∈ s, x < a) →
      ∏ i ∈ s, (f i + g i) =
          ∏ i ∈ s, f i +
            ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j →
        ∏ i ∈ insert a s, (f i + g i) =
          ∏ i ∈ insert a s, f i +
            ∑ i ∈ insert a s,
              (g i * ∏ j ∈ filter (fun j => j < i) (insert a s), (f j + g j)) *
                ∏ j ∈ filter (fun j => i < j) (insert a s), f j

Tactic:
intro a s ha ihs

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : LinearOrder ι
f g : ι → α
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs :
  ∏ i ∈ s, (f i + g i) =
    ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j + g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
⊢ ∏ i ∈ insert a s, (f i + g i) =
    ∏ i ∈ insert a s, f i +
      ∑ i ∈ insert a s,
        (g i * ∏ j ∈ filter (fun j => j < i) (insert a s), (f j + g j)) *
          ∏ j ∈ filter (fun j => i < j) (insert a s), f j
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAt.comp_of_eq
    (hh₂ : HasDerivAt h₂ h₂' y) (hh : HasDerivAt h h' x) (hy : y = h x) :
    HasDerivAt (h₂ ∘ h) (h₂' * h') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' y
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
rw [hy] at hh₂

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' y : 𝕜'
hh₂ : HasDerivAt h₂ h₂' (h x)
hh : HasDerivAt h h' x
hy : y = h x
⊢ HasDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
exact hh₂.comp x hh

Result:
no goals
-- Mathlib/Algebra/Regular/SMul.lean
theorem one : IsSMulRegular M (1 : R) := fun a b ab => by
  dsimp only [Function.comp_def] at ab
  rw [one_smul, one_smul] at ab
  assumption

Proof state:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b

Tactic:
rw [one_smul, one_smul] at ab

Result:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b

Proof state:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : (fun x => 1 • x) a = (fun x => 1 • x) b
⊢ a = b

Tactic:
dsimp only [Function.comp_def] at ab

Result:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : 1 • a = 1 • b
⊢ a = b
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
/-- A basic `ext` lemma for objects of `SimplexCategoryGenRel`. -/
@[ext]
lemma ext {x y : SimplexCategoryGenRel} (h : x.len = y.len) : x = y

Proof state:
case H.H
n✝¹ n✝ : ℕ
h : (mk n✝¹).len = (mk n✝).len
⊢ mk n✝¹ = mk n✝

Tactic:
simp only [mk_len] at h

Result:
case H.H
n✝¹ n✝ : ℕ
h : n✝¹ = n✝
⊢ mk n✝¹ = mk n✝

Proof state:
case H
y : SimplexCategoryGenRel
n✝ : ℕ
h : (mk n✝).len = y.len
⊢ mk n✝ = y

Tactic:
cases y

Result:
case H.H
n✝¹ n✝ : ℕ
h : (mk n✝¹).len = (mk n✝).len
⊢ mk n✝¹ = mk n✝

Proof state:
x y : SimplexCategoryGenRel
h : x.len = y.len
⊢ x = y

Tactic:
cases x

Result:
case H
y : SimplexCategoryGenRel
n✝ : ℕ
h : (mk n✝).len = y.len
⊢ mk n✝ = y

Proof state:
case H.H
n✝¹ n✝ : ℕ
h : n✝¹ = n✝
⊢ mk n✝¹ = mk n✝

Tactic:
congr

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem subgraphOfAdj_connected {v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj hvw).Connected

Proof state:
case mk.mk.inr.inl.h
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
(apply Adj.reachable; simp)

Result:
no goals

Proof state:
case mk.mk.inr.inr
V : Type u
G : SimpleGraph V
v b : V
hvw : G.Adj v b
ha hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨b, ha⟩ ⟨b, hb⟩

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).Connected

Tactic:
refine ⟨⟨?_⟩⟩

Result:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).coe.Preconnected

Proof state:
case mk.mk.inr.inl
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
apply Adj.reachable

Result:
case mk.mk.inr.inl.h
V : Type u
G : SimpleGraph V
a b : V
hvw : G.Adj b a
ha : a ∈ (G.subgraphOfAdj hvw).verts
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Adj ⟨a, ha⟩ ⟨b, hb⟩

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb

Result:
case mk.mk
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha✝ : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩

Proof state:
case mk.mk
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha✝ : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb✝ : b ∈ (G.subgraphOfAdj hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩

Tactic:
obtain rfl | rfl := ha <;> obtain rfl | rfl := hb <;>
  first | rfl | (apply Adj.reachable; simp)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).coe.Preconnected

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

Result:
case mk.mk
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
a : V
ha : a ∈ (G.subgraphOfAdj hvw).verts
b : V
hb : b ∈ (G.subgraphOfAdj hvw).verts
⊢ (G.subgraphOfAdj hvw).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩
-- Mathlib/Data/Nat/Cast/Order/Ring.lean
theorem cast_tsub [OrderedCommSemiring α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α]
    [AddLeftReflectLE α] (m n : ℕ) : ↑(m - n) = (m - n : α)

Proof state:
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_total m n with h | h

Result:
case inl
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

case inr
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Proof state:
case inl
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]

Result:
case inl
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑m ≤ ↑n

Proof state:
case inl
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑m ≤ ↑n

Tactic:
exact mono_cast h

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩

Result:
case inr.intro
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ ↑(m + n - n) = ↑(m + n) - ↑n

Proof state:
case inr.intro
α : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ ↑(m + n - n) = ↑(m + n) - ↑n

Tactic:
rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem back?_attach {xs : Array α} :
    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.back? = { toList := toList✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
⊢ xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
cases xs

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.attach.back? = { toList := toList✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma IsStandardSmooth.comp {g : S →+* T} {f : R →+* S}
    (hg : IsStandardSmooth.{t', w'} g) (hf : IsStandardSmooth.{t, w} f) :
    IsStandardSmooth.{max t t', max w w'} (g.comp f)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardSmooth S T
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ Algebra.IsStandardSmooth R T

Tactic:
exact Algebra.IsStandardSmooth.trans.{t, t', w, w'} R S T

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T

Tactic:
algebraize [f, g, (g.comp f)]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardSmooth S T
algebraizeInst✝ : Algebra.IsStandardSmooth R S
⊢ Algebra.IsStandardSmooth R T

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ (g.comp f).IsStandardSmooth

Tactic:
rw [IsStandardSmooth]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T
-- Mathlib/Topology/Homeomorph.lean
@[simp] lemma toHomeomorph_symm (e : X ≃ Y) (he) :
  (e.toHomeomorph he).symm = e.symm.toHomeomorph fun s ↦ by convert (he _).symm; simp := rfl

Proof state:
case h.e'_2.h.e'_3
X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s
s : Set X
⊢ s = ⇑e ⁻¹' (⇑e.symm ⁻¹' s)

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s
s : Set X
⊢ IsOpen (⇑e.symm ⁻¹' s) ↔ IsOpen s

Tactic:
convert (he _).symm

Result:
case h.e'_2.h.e'_3
X : Type u_1
Y : Type u_2
W : Type u_3
Z✝ : Type u_4
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ Y
he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s
s : Set X
⊢ s = ⇑e ⁻¹' (⇑e.symm ⁻¹' s)
-- Mathlib/CategoryTheory/Monad/Basic.lean
theorem comonadToFunctor_mapIso_comonad_iso_mk {M N : Comonad C} (f : (M : C ⥤ C) ≅ N) (f_ε f_δ) :
    (comonadToFunctor _).mapIso (ComonadIso.mk f f_ε f_δ) = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
⊢ (comonadToFunctor C).mapIso (ComonadIso.mk f f_ε f_δ) = f

Tactic:
ext

Result:
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
x✝ : C
⊢ ((comonadToFunctor C).mapIso (ComonadIso.mk f f_ε f_δ)).hom.app x✝ = f.hom.app x✝

Proof state:
case w.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
M N : Comonad C
f : M.toFunctor ≅ N.toFunctor
f_ε : ∀ (X : C), f.hom.app X ≫ N.ε.app X = M.ε.app X
f_δ : ∀ (X : C), f.hom.app X ≫ N.δ.app X = M.δ.app X ≫ f.hom.app (M.obj X) ≫ N.map (f.hom.app X)
x✝ : C
⊢ ((comonadToFunctor C).mapIso (ComonadIso.mk f f_ε f_δ)).hom.app x✝ = f.hom.app x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem summable_sum_mul_range_of_summable_mul (h : Summable fun x : ℕ × ℕ ↦ f x.1 * g x.2) :
    Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Proof state:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f x.1 * g x.2
⊢ Summable fun n => ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]

Result:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f x.1 * g x.2
⊢ Summable fun n => ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Proof state:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x => f x.1 * g x.2
⊢ Summable fun n => ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact summable_sum_mul_antidiagonal_of_summable_mul h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem le_rpow_inv_iff {x y : ℝ≥0∞} {z : ℝ} (hz : 0 < z) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
nth_rw 1 [← @mul_inv_cancel₀ _ _ z hz.ne']

Result:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
nth_rw 1 [← rpow_one x]

Result:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rw [rpow_mul, @rpow_le_rpow_iff _ _ z⁻¹ (by simp [hz])]

Result:
no goals

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
simp [hz]

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Prime.ne_one {p : ℕ+} : p.Prime → p ≠ 1

Proof state:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ ↑p = 1

Tactic:
rw [PNat.coe_eq_one_iff]

Result:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ p = 1

Proof state:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ False

Tactic:
apply Nat.Prime.ne_one pp

Result:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ ↑p = 1

Proof state:
p : ℕ+
⊢ p.Prime → p ≠ 1

Tactic:
intro pp

Result:
p : ℕ+
pp : p.Prime
⊢ p ≠ 1

Proof state:
p : ℕ+
pp : p.Prime
⊢ p ≠ 1

Tactic:
intro contra

Result:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ False

Proof state:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ p = 1

Tactic:
apply contra

Result:
no goals
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem add (hf : UnifTight f p μ) (hg : UnifTight g p μ)
    (hf_meas : ∀ i, AEStronglyMeasurable (f i) μ) (hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) :
    UnifTight (f + g) p μ := fun ε hε ↦ by
  rcases exists_Lp_half β μ p (coe_ne_zero.mpr hε.ne') with ⟨η, hη_pos, hη⟩
  by_cases hη_top : η = ∞
  · replace hη := hη_top ▸ hη
    refine ⟨∅, (by measurability), fun i ↦ ?_⟩
    simp only [compl_empty, indicator_univ, Pi.add_apply]
    exact (hη (f i) (g i) (hf_meas i) (hg_meas i) le_top le_top).le
  obtain ⟨s, hμs, hsm, hfs, hgs⟩ :
      ∃ s ∈ μ.cofinite, MeasurableSet s ∧
        (∀ i, eLpNorm (s.indicator (f i)) p μ ≤ η) ∧
        (∀ i, eLpNorm (s.indicator (g i)) p μ ≤ η) :=
    ((hf.eventually_cofinite_indicator hη_pos.ne').and
      (hg.eventually_cofinite_indicator hη_pos.ne')).exists_measurable_mem_of_smallSets
  refine ⟨sᶜ, ne_of_lt hμs, fun i ↦ ?_⟩
  have η_cast : ↑η.toNNReal = η := coe_toNNReal hη_top
  calc
    eLpNorm (indicator sᶜᶜ (f i + g i)) p μ
      = eLpNorm (indicator s (f i) + indicator s (g i)) p μ

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη_top : η = ⊤
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ⊤ → eLpNorm g p μ ≤ ⊤ → eLpNorm (f + g) p μ < ↑ε
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator ((f + g) i)) p μ ≤ ↑ε

Tactic:
refine ⟨∅, (by measurability), fun i ↦ ?_⟩

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifTight f p μ
hg : UnifTight g p μ
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ≥0
hε : 0 < ε
η : ℝ≥0∞
hη_pos : 0 < η
hη_top : η = ⊤
hη :
  ∀ (f g : α → β),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ → eLpNorm f p μ ≤ ⊤ → eLpNorm g p μ ≤ ⊤ → eLpNorm (f + g) p μ < ↑ε
i : ι
⊢ eLpNorm (∅ᶜ.indicator ((f + g) i)) p μ ≤ ↑ε