harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem alterKey_cons_perm {k : α} {f : Option (β k) → Option (β k)} {k' : α} {v' : β k'}
    {l : List ((a : α) × β a)} : Perm (alterKey k f (⟨k', v'⟩ :: l))
      (if hk : k' == k then
        match f (some (cast (congrArg β (eq_of_beq hk)) v')) with
          | none => l
          | some v => ⟨k, v⟩ :: l
        else
          ⟨k', v'⟩ :: alterKey k f l)

Proof state:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = false
⊢ (match f (getValueCast? k l) with
      | none => ⟨k', v'⟩ :: eraseKey k l
      | some v => insertEntry k v (⟨k', v'⟩ :: l)).Perm
    (⟨k', v'⟩ ::
      match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l)

Tactic:
split

Result:
case neg.h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = false
x✝ : Option (β k)
heq✝ : f (getValueCast? k l) = none
⊢ (⟨k', v'⟩ :: eraseKey k l).Perm (⟨k', v'⟩ :: eraseKey k l)

case neg.h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = false
x✝ : Option (β k)
v✝ : β k
heq✝ : f (getValueCast? k l) = some v✝
⊢ (insertEntry k v✝ (⟨k', v'⟩ :: l)).Perm (⟨k', v'⟩ :: insertEntry k v✝ l)

Proof state:
case neg.h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
k' : α
v' : β k'
l : List ((a : α) × β a)
hk' : (k' == k) = false
x✝ : Option (β k)
heq✝ : f (getValueCast? k l) = none
⊢ (⟨k', v'⟩ :: eraseKey k l).Perm (⟨k', v'⟩ :: eraseKey k l)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_assoc {m : δ → γ → ε} {n : α → β → δ} {m' : α → ε' → ε} {n' : β → γ → ε'}
    {h : Filter γ} (h_assoc : ∀ a b c, m (n a b) c = m' a (n' b c)) :
    map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map (fun p => m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) =
    map ((fun p => m' p.1 (n' p.2.1 p.2.2)) ∘ ⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h)

Tactic:
simp only [h_assoc, Function.comp_def, Equiv.prodAssoc_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)

Tactic:
rw [← map_prod_eq_map₂ n, ← map_prod_eq_map₂ n', map₂_map_left, map₂_map_right,
  ← map_prod_eq_map₂, ← map_prod_eq_map₂, ← prod_assoc, map_map]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map (fun p => m (n p.1.1 p.1.2) p.2) ((f ×ˢ g) ×ˢ h) =
    map ((fun p => m' p.1 (n' p.2.1 p.2.2)) ∘ ⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h)
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem threeAPFree_iff_eq_right {s : Set ℕ} :
    ThreeAPFree s ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ∀ ⦃c⦄, c ∈ s → a + c = b + b → a = c

Proof state:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = c → a = b

Tactic:
rintro rfl

Result:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ a = b

Proof state:
case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
c : ℕ
hc : c ∈ s
hb : a ∈ s
habc : a + c = a + a
⊢ a = c

Tactic:
exact (add_left_cancel habc).symm

Result:
no goals

Proof state:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ a = b

Tactic:
simp_rw [← two_mul] at habc

Result:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : 2 * a = 2 * b
⊢ a = b

Proof state:
case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = b → a = c

Tactic:
rintro rfl

Result:
case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
c : ℕ
hc : c ∈ s
hb : a ∈ s
habc : a + c = a + a
⊢ a = c

Proof state:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : 2 * a = 2 * b
⊢ a = b

Tactic:
exact mul_left_cancel₀ two_ne_zero habc

Result:
no goals

Proof state:
s : Set ℕ
⊢ ThreeAPFree s ↔ ∀ ⦃a : ℕ⦄, a ∈ s → ∀ ⦃b : ℕ⦄, b ∈ s → ∀ ⦃c : ℕ⦄, c ∈ s → a + c = b + b → a = c

Tactic:
refine forall₄_congr fun a _ha b hb => forall₃_congr fun c hc habc => ⟨?_, ?_⟩

Result:
case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = b → a = c

case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = c → a = b
-- Mathlib/Data/List/Induction.lean
theorem bidirectionalRec_singleton {motive : List α → Sort*}
    (nil : motive []) (singleton : ∀ a : α, motive [a])
    (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b]))) (a : α) :
    bidirectionalRec nil singleton cons_append [a] = singleton a

Proof state:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a : α
⊢ bidirectionalRec nil singleton cons_append [a] = singleton a

Tactic:
simp [bidirectionalRec]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_neg (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (fun y => -f y) s x

Tactic:
simpa

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt h,
  fderivWithin_zero_of_not_differentiableWithinAt, neg_zero]

Result:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (fun y => -f y) s x

Proof state:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x

Tactic:
exact h.hasFDerivWithinAt.neg.fderivWithin hxs

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s x

Result:
case pos
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x

case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (fun y => -f y) s x = -fderivWithin 𝕜 f s x
-- Mathlib/Tactic/Ring/Basic.lean
theorem zero_pow {b : ℕ} (_ : 0 < b) : (0 : R) ^ b = 0 := match b with | b+1 => by simp [pow_succ]

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b✝ b : ℕ
x✝ : 0 < b + 1
⊢ 0 ^ (b + 1) = 0

Tactic:
simp [pow_succ]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem PseudoMetricSpace.replaceUniformity_eq {α} [U : UniformSpace α] (m : PseudoMetricSpace α)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : m.replaceUniformity H = m

Proof state:
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ m.replaceUniformity H = m

Tactic:
ext

Result:
case h.dist.h.h
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Proof state:
case h.dist.h.h
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_aux_uniformity_eq [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
    𝓤 (WithLp p (α × β)) = 𝓤[instUniformSpaceProd]

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
A : IsUniformInducing ⇑(WithLp.equiv p (α × β))
⊢ (fun x => ((WithLp.equiv p (α × β)) x.1, (WithLp.equiv p (α × β)) x.2)) = id

Tactic:
ext i <;> rfl

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
A : IsUniformInducing ⇑(WithLp.equiv p (α × β))
⊢ 𝓤 (WithLp p (α × β)) = 𝓤 (α × β)

Tactic:
have : (fun x : WithLp p (α × β) × WithLp p (α × β) =>
  ((WithLp.equiv p (α × β)) x.fst, (WithLp.equiv p (α × β)) x.snd)) = id := by
  ext i <;> rfl

Result:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
A : IsUniformInducing ⇑(WithLp.equiv p (α × β))
this : (fun x => ((WithLp.equiv p (α × β)) x.1, (WithLp.equiv p (α × β)) x.2)) = id
⊢ 𝓤 (WithLp p (α × β)) = 𝓤 (α × β)

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
A : IsUniformInducing ⇑(WithLp.equiv p (α × β))
this : (fun x => ((WithLp.equiv p (α × β)) x.1, (WithLp.equiv p (α × β)) x.2)) = id
⊢ 𝓤 (WithLp p (α × β)) = 𝓤 (α × β)

Tactic:
rw [← A.comap_uniformity, this, comap_id]

Result:
no goals

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
⊢ 𝓤 (WithLp p (α × β)) = 𝓤 (α × β)

Tactic:
have A : IsUniformInducing (WithLp.equiv p (α × β)) :=
  (prod_antilipschitzWith_equiv_aux p α β).isUniformInducing
    (prod_lipschitzWith_equiv_aux p α β).uniformContinuous

Result:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
A : IsUniformInducing ⇑(WithLp.equiv p (α × β))
⊢ 𝓤 (WithLp p (α × β)) = 𝓤 (α × β)
-- Mathlib/CategoryTheory/Monad/Basic.lean
lemma isSplitMono_iff_isIso_unit (T : Monad C) (X : C) [IsIso T.μ] :
    IsSplitMono (T.η.app X) ↔ IsIso (T.η.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
⊢ IsSplitMono (T.η.app X) ↔ IsIso (T.η.app X)

Tactic:
refine ⟨fun _ ↦ ⟨retraction (T.η.app X), by simp, ?_⟩, fun _ ↦ inferInstance⟩

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ T.η.app X ≫ retraction (T.η.app X) = 𝟙 ((𝟭 C).obj X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ T.η.app (T.obj X) ≫ T.map ⋯.some.1 = T.η.app (T.obj X) ≫ T.map (retraction (T.η.app X))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = 𝟙 (T.obj X)

Tactic:
erw [← map_id, ← IsSplitMono.id (T.η.app X), map_comp, T.map_unit_app X, T.η.naturality]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ T.η.app (T.obj X) ≫ T.map ⋯.some.1 = T.η.app (T.obj X) ≫ T.map (retraction (T.η.app X))
-- Mathlib/Topology/Algebra/Polynomial.lean
theorem tendsto_abv_atTop {R k α : Type*} [Ring R] [LinearOrderedField k] (abv : R → k)
    [IsAbsoluteValue abv] (p : R[X]) (h : 0 < degree p) {l : Filter α} {z : α → R}
    (hz : Tendsto (abv ∘ z) l atTop) : Tendsto (fun x => abv (p.eval (z x))) l atTop

Proof state:
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < p.degree
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x => abv (eval (z x) p)) l atTop

Tactic:
apply tendsto_abv_eval₂_atTop _ _ _ h _ hz

Result:
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < p.degree
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ (RingHom.id R) p.leadingCoeff ≠ 0

Proof state:
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < p.degree
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ (RingHom.id R) p.leadingCoeff ≠ 0

Tactic:
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma monovary_inv₀ (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Monovary f⁻¹ g⁻¹ ↔ Monovary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
f : ι → α
g : ι → β
hf : StrongLT 0 f
hg : StrongLT 0 g
⊢ Monovary f⁻¹ g⁻¹ ↔ Monovary f g

Tactic:
rw [monovary_inv_left₀ hf, antivary_inv_right₀ hg]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem pow_right_mono (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n

Proof state:
case succ
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ n✝ * I ≤ J ^ n✝ * J

Tactic:
exact Ideal.mul_mono hn e

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
⊢ I ^ 0 ≤ J ^ 0

Tactic:
rw [Submodule.pow_zero, Submodule.pow_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
⊢ I ^ n ≤ J ^ n

Tactic:
induction' n with _ hn

Result:
case zero
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
⊢ I ^ 0 ≤ J ^ 0

case succ
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ (n✝ + 1) ≤ J ^ (n✝ + 1)

Proof state:
case succ
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ (n✝ + 1) ≤ J ^ (n✝ + 1)

Tactic:
rw [Submodule.pow_succ, Submodule.pow_succ]

Result:
case succ
R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n✝ : ℕ
hn : I ^ n✝ ≤ J ^ n✝
⊢ I ^ n✝ * I ≤ J ^ n✝ * J
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem zsmul_pow_two_powHalf (m : ℤ) (n k : ℕ) :
    (m * 2 ^ n) * powHalf (n + k) = m * powHalf k

Proof state:
case e_a
m : ℤ
n k : ℕ
⊢ 2 ^ n * powHalf (n + k) = powHalf k

Tactic:
exact nsmul_pow_two_powHalf' n k

Result:
no goals

Proof state:
m : ℤ
n k : ℕ
⊢ ↑m * 2 ^ n * powHalf (n + k) = ↑m * powHalf k

Tactic:
rw [mul_assoc]

Result:
m : ℤ
n k : ℕ
⊢ ↑m * (2 ^ n * powHalf (n + k)) = ↑m * powHalf k

Proof state:
m : ℤ
n k : ℕ
⊢ ↑m * (2 ^ n * powHalf (n + k)) = ↑m * powHalf k

Tactic:
congr

Result:
case e_a
m : ℤ
n k : ℕ
⊢ 2 ^ n * powHalf (n + k) = powHalf k
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem quasiMeasurePreserving_fst : QuasiMeasurePreserving Prod.fst (μ.prod ν) μ

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ (map Prod.fst (μ.prod ν)) s = 0

Tactic:
rw [map_apply measurable_fst hs, ← prod_univ, prod_prod, h2s, zero_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
⊢ QuasiMeasurePreserving Prod.fst (μ.prod ν) μ

Tactic:
refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ (map Prod.fst (μ.prod ν)) s = 0
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_inf_distrib (a b : α) : ￢(a ⊓ b) = ￢a ⊔ ￢b

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢(a ⊓ b) = ￢a ⊔ ￢b

Tactic:
simp_rw [← top_sdiff', sdiff_inf_distrib]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_mk {xs : Array α} {h : xs.size = n} {P : α → Prop} {H : ∀ x ∈ mk xs h, P x} :
    (mk xs h).attachWith P H = mk (xs.attachWith P (by simpa using H)) (by simpa using h)

Proof state:
α : Type u_1
n : Nat
xs : Array α
h : xs.size = n
P : α → Prop
H : ∀ (x : α), x ∈ { toArray := xs, size_toArray := h } → P x
⊢ { toArray := xs, size_toArray := h }.attachWith P H = { toArray := xs.attachWith P ⋯, size_toArray := ⋯ }

Tactic:
simp [attachWith]

Result:
no goals

Proof state:
α : Type ?u.817
n : Nat
xs : Array α
h : xs.size = n
P : α → Prop
H : ∀ (x : α), x ∈ { toArray := xs, size_toArray := h } → P x
⊢ (xs.attachWith P ⋯).size = n

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type ?u.817
n : Nat
xs : Array α
h : xs.size = n
P : α → Prop
H : ∀ (x : α), x ∈ { toArray := xs, size_toArray := h } → P x
⊢ ∀ (x : α), x ∈ xs → P x

Tactic:
simpa using H

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem nonMemberSubfamily_nonMemberSubfamily :
    (𝒜.nonMemberSubfamily a).nonMemberSubfamily a = 𝒜.nonMemberSubfamily a

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ nonMemberSubfamily a 𝒜

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) = nonMemberSubfamily a 𝒜

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (nonMemberSubfamily a 𝒜) ↔ a✝ ∈ nonMemberSubfamily a 𝒜
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem edist_mulIndicator (s t : Set α) (f : α → E) (x : α) :
    edist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(s ∆ t).mulIndicator f x‖₊

Proof state:
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(s ∆ t).mulIndicator f x‖₊

Tactic:
rw [edist_nndist, nndist_mulIndicator]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma homMk_eq {X Y : C} (f : LeftFraction W X Y) :
    homMk f = f.map (Q W) (Localization.inverts _ W)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : W.LeftFraction X Y
⊢ homMk f = f.map (Q W) ⋯

Tactic:
have := Localization.inverts (Q W) W f.s f.hs

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ homMk f = f.map (Q W) ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ homMk f = f.map (Q W) ⋯

Tactic:
rw [← Q_map_comp_Qinv f.f f.s f.hs, ← cancel_mono ((Q W).map f.s),
  assoc, Qiso_inv_hom_id, comp_id, map_comp_map_s]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_inclusion (p p' : Submodule R M) (h : p ≤ p') : ker (inclusion h) = ⊥

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ ker (inclusion h) = ⊥

Tactic:
rw [inclusion, ker_codRestrict, ker_subtype]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Central.lean
theorem succ_mul_centralBinom_succ (n : ℕ) :
    (n + 1) * centralBinom (n + 1) = 2 * (2 * n + 1) * centralBinom n :=
  calc
    (n + 1) * (2 * (n + 1)).choose (n + 1) = (2 * n + 2).choose (n + 1) * (n + 1) := mul_comm _ _
    _ = (2 * n + 1).choose n * (2 * n + 2)

Proof state:
n : ℕ
⊢ 2 * ((2 * n).choose n * (2 * n + 1)) = 2 * (2 * n + 1) * (2 * n).choose n

Tactic:
rw [mul_assoc, mul_comm (2 * n + 1)]

Result:
no goals

Proof state:
n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (n + 1)) = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n))

Tactic:
rw [two_mul n, add_assoc,
    Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
n : ℕ
⊢ (2 * n + 2).choose (n + 1) * (n + 1) = (2 * n + 1).choose n * (2 * n + 2)

Tactic:
rw [choose_succ_right_eq, choose_mul_succ_eq]

Result:
no goals

Proof state:
n : ℕ
⊢ 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) = 2 * ((2 * n).choose n * (2 * n + 1))

Tactic:
rw [choose_mul_succ_eq]

Result:
no goals

Proof state:
n : ℕ
⊢ (2 * n + 1).choose n * (2 * n + 2) = 2 * ((2 * n + 1).choose n * (n + 1))

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma monotone_map (F : C ⥤ D) :
    Monotone (map · F)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F : C ⥤ D
⊢ Monotone fun x => x.map F

Tactic:
intro P Q h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ Q.map F f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{u_2, u_1} D
F : C ⥤ D
P Q : MorphismProperty C
h : P ≤ Q
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ Q.map F f

Tactic:
exact ⟨X', Y', f', h _ hf', ⟨e⟩⟩

Result:
no goals