harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.lift_post (c : Cone F) :
    G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.mapCone c)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
⊢ G.map (lift F c) ≫ post F G = lift (F ⋙ G) (G.mapCone c)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ (G.map (lift F c) ≫ post F G) ≫ π (F ⋙ G) j✝ = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (c.π.app j✝) = (G.mapCone c).π.app j✝

Tactic:
rfl

Result:
no goals

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ (G.map (lift F c) ≫ post F G) ≫ π (F ⋙ G) j✝ = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝

Tactic:
rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (c.π.app j✝) = (G.mapCone c).π.app j✝
-- Mathlib/Topology/Separation/Basic.lean
theorem continuousAt_update_of_ne [T1Space X] [DecidableEq X] [TopologicalSpace Y]
    {f : X → Y} {x x' : X} {y : Y} (hne : x' ≠ x) :
    ContinuousAt (Function.update f x y) x' ↔ ContinuousAt f x'

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
x x' : X
y : Y
hne : x' ≠ x
⊢ ContinuousAt (update f x y) x' ↔ ContinuousAt f x'

Tactic:
simp only [← continuousWithinAt_univ, continuousWithinAt_update_of_ne hne]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFreeOn_univ : G.CliqueFreeOn Set.univ n ↔ G.CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFreeOn Set.univ n ↔ G.CliqueFree n

Tactic:
simp [CliqueFree, CliqueFreeOn]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- The gaussian distribution pdf integrates to 1 when the variance is not zero. -/
lemma integral_gaussianPDFReal_eq_one (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) :
    ∫ x, gaussianPDFReal μ v x = 1

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ENNReal.ofReal (∫ (x : ℝ), gaussianPDFReal μ v x) = ENNReal.ofReal 1
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x = 1

Tactic:
rwa [← ENNReal.ofReal_eq_ofReal_iff (integral_nonneg (gaussianPDFReal_nonneg _ _)) zero_le_one]

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x = 1

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (integrable_gaussianPDFReal _ _)
  (ae_of_all _ (gaussianPDFReal_nonneg _ _)), ← ENNReal.ofReal_one] at h

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ENNReal.ofReal (∫ (x : ℝ), gaussianPDFReal μ v x) = ENNReal.ofReal 1
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x = 1

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x = 1

Tactic:
have h := lintegral_gaussianPDFReal_eq_one μ hv

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x = 1
-- Mathlib/Data/Set/Insert.lean
theorem pair_diff_left (hne : a ≠ b) : ({a, b} : Set α) \ {a} = {b}

Proof state:
α : Type u
a b : α
hne : a ≠ b
⊢ {a, b} \ {a} = {b}

Tactic:
rw [insert_diff_of_mem _ (mem_singleton a), diff_singleton_eq_self (by simpa)]

Result:
no goals

Proof state:
α : Type u
a b : α
hne : a ≠ b
⊢ a ∉ {b}

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/List.lean
@[simp] lemma sum_zipWith_distrib_left [Semiring R] (f : ι → κ → R) (a : R) :
    ∀ (l₁ : List ι) (l₂ : List κ),
      (zipWith (fun i j ↦ a * f i j) l₁ l₂).sum = a * (zipWith f l₁ l₂).sum
  | [], _ => by simp
  | _, [] => by simp
  | i :: l₁, j :: l₂ => by simp [sum_zipWith_distrib_left, mul_add]

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : Semiring R
f : ι → κ → R
a : R
x✝ : List ι
⊢ (zipWith (fun i j => a * f i j) x✝ []).sum = a * (zipWith f x✝ []).sum

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : Semiring R
f : ι → κ → R
a : R
x✝ : List κ
⊢ (zipWith (fun i j => a * f i j) [] x✝).sum = a * (zipWith f [] x✝).sum

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
R : Type u_5
inst✝ : Semiring R
f : ι → κ → R
a : R
i : ι
l₁ : List ι
j : κ
l₂ : List κ
⊢ (zipWith (fun i j => a * f i j) (i :: l₁) (j :: l₂)).sum = a * (zipWith f (i :: l₁) (j :: l₂)).sum

Tactic:
simp [sum_zipWith_distrib_left, mul_add]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_inv_hom_hom_hom_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom =
      (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv :=
  eq_of_inv_eq_inv (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom) =
    inv ((α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem mem_iUnion₂ {x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋃ (i) (j), s i j) ↔ ∃ i j, x ∈ s i j

Proof state:
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j

Tactic:
simp_rw [mem_iUnion]

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
theorem vadd_absorbs {M E : Type*} [Bornology M] [AddZeroClass E] [DistribSMul M E]
    {s₁ s₂ t : Set E} {x : E} (h₁ : Absorbent M s₁) (h₂ : Absorbs M s₂ t) :
    Absorbs M (s₁ + s₂) (x +ᵥ t)

Proof state:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) ({x} +ᵥ t)

Tactic:
exact (h₁ x).add h₂

Result:
no goals

Proof state:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) (x +ᵥ t)

Tactic:
rw [← singleton_vadd]

Result:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) ({x} +ᵥ t)
-- Mathlib/Computability/Reduce.lean
theorem add_le {d₁ d₂ d₃ : ManyOneDegree} : d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃

Proof state:
d₁ d₂ d₃ : ManyOneDegree
⊢ d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃

Tactic:
induction d₁ using ManyOneDegree.ind_on

Result:
case h
d₂ d₃ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ + d₂ ≤ d₃ ↔ of p✝ ≤ d₃ ∧ d₂ ≤ d₃

Proof state:
case h.h
d₃ : ManyOneDegree
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ + of p✝ ≤ d₃ ↔ of p✝¹ ≤ d₃ ∧ of p✝ ≤ d₃

Tactic:
induction d₃ using ManyOneDegree.ind_on

Result:
case h.h.h
p✝² p✝¹ p✝ : Set ℕ
⊢ of p✝² + of p✝¹ ≤ of p✝ ↔ of p✝² ≤ of p✝ ∧ of p✝¹ ≤ of p✝

Proof state:
case h
d₂ d₃ : ManyOneDegree
p✝ : Set ℕ
⊢ of p✝ + d₂ ≤ d₃ ↔ of p✝ ≤ d₃ ∧ d₂ ≤ d₃

Tactic:
induction d₂ using ManyOneDegree.ind_on

Result:
case h.h
d₃ : ManyOneDegree
p✝¹ p✝ : Set ℕ
⊢ of p✝¹ + of p✝ ≤ d₃ ↔ of p✝¹ ≤ d₃ ∧ of p✝ ≤ d₃

Proof state:
case h.h.h
p✝² p✝¹ p✝ : Set ℕ
⊢ of p✝² + of p✝¹ ≤ of p✝ ↔ of p✝² ≤ of p✝ ∧ of p✝¹ ≤ of p✝

Tactic:
simpa only [← add_of, of_le_of] using disjoin_le

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_units_conj (M : (Matrix m m R)ˣ) (N : Matrix m m R) :
    det (M.val * N * M⁻¹.val) = det N

Proof state:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * N * ↑M⁻¹).det = N.det

Tactic:
rw [det_mul_right_comm, Units.mul_inv, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_shiftRight : eval assign (.shiftRight lhs rhs) = (eval assign lhs) >>> (eval assign rhs)

Proof state:
assign : Assignment
a✝¹ : Nat
lhs : BVExpr a✝¹
a✝ : Nat
rhs : BVExpr a✝
⊢ eval assign (lhs.shiftRight rhs) = eval assign lhs >>> eval assign rhs

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem minkowskiBound_pos : 0 < minkowskiBound K I

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ 0 < minkowskiBound K I

Tactic:
refine zero_lt_iff.mpr (mul_ne_zero ?_ ?_)

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) ≠ 0

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ 2 ^ finrank ℝ (mixedSpace K) ≠ 0

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ 2 ^ finrank ℝ (mixedSpace K) ≠ 0

Tactic:
exact ENNReal.pow_ne_zero two_ne_zero _

Result:
no goals

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) ≠ 0

Tactic:
exact ZSpan.measure_fundamentalDomain_ne_zero _

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_update_of_mem [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) :
    ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ singleton i, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
b : β
⊢ (∏ x ∈ s ∩ {i}, b) * ∏ x ∈ s \ {i}, f x = b * ∏ x ∈ s \ {i}, f x

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
b : β
⊢ ∏ x ∈ s, update f i b x = b * ∏ x ∈ s \ {i}, f x

Tactic:
rw [update_eq_piecewise, prod_piecewise]

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∈ s
f : α → β
b : β
⊢ (∏ x ∈ s ∩ {i}, b) * ∏ x ∈ s \ {i}, f x = b * ∏ x ∈ s \ {i}, f x
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_add_of_right_mem [AddRightCancelMonoid ι] [GradedRing 𝒜] {a b : A}
    (b_mem : b ∈ 𝒜 j) : (decompose 𝒜 (a * b) (i + j) : A) = decompose 𝒜 a i * b

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ ↑(((decompose 𝒜) (a * ↑b)) (i + j)) = ↑(((decompose 𝒜) a) i) * ↑b

Tactic:
rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]

Result:
no goals

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 j
⊢ ↑(((decompose 𝒜) (a * b)) (i + j)) = ↑(((decompose 𝒜) a) i) * b

Tactic:
lift b to 𝒜 j using b_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddRightCancelMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 j)
⊢ ↑(((decompose 𝒜) (a * ↑b)) (i + j)) = ↑(((decompose 𝒜) a) i) * ↑b
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem induction_on_mul_T {Q : R[T;T⁻¹] → Prop} (f : R[T;T⁻¹])
    (Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-n))) : Q f

Proof state:
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))
⊢ Q f

Tactic:
rcases f.exists_T_pow with ⟨n, f', hf⟩

Result:
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ Q f

Proof state:
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ Q (toLaurent f' * T (-↑n))

Tactic:
exact Qf

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ Q f

Tactic:
rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub,
  ← mul_assoc, ← hf]

Result:
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : toLaurent f' = f * T ↑n
⊢ Q (toLaurent f' * T (-↑n))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    (l : Vector α n) (f : α → β → β) (init : β) :
    forIn l init (fun a b => pure (.yield (f a b))) =
      pure (f := m) (l.foldl (fun b a => f a b) init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
f : α → β → β
init : β
⊢ (forIn l init fun a b => pure (ForInStep.yield (f a b))) = pure (foldl (fun b a => f a b) init l)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → β
init : β
l : Array α
⊢ (forIn { toArray := l, size_toArray := ⋯ } init fun a b => pure (ForInStep.yield (f a b))) =
    pure (foldl (fun b a => f a b) init { toArray := l, size_toArray := ⋯ })

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → β
init : β
l : Array α
⊢ (forIn { toArray := l, size_toArray := ⋯ } init fun a b => pure (ForInStep.yield (f a b))) =
    pure (foldl (fun b a => f a b) init { toArray := l, size_toArray := ⋯ })

Tactic:
simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_add_const (l : List α) (a b : Nat) :
    l.foldr (fun _ x => x + a) b = b + a * l.length

Proof state:
α : Type u_1
l : List α
a b : Nat
⊢ foldr (fun x x => x + a) b l = b + a * l.length

Tactic:
induction l generalizing b with
| nil => simp
| cons y l ih =>
  simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
a b : Nat
⊢ foldr (fun x x => x + a) b [] = b + a * [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
a : Nat
y : α
l : List α
ih : ∀ (b : Nat), foldr (fun x x => x + a) b l = b + a * l.length
b : Nat
⊢ foldr (fun x x => x + a) b (y :: l) = b + a * (y :: l).length

Tactic:
simp only [foldr_cons, ih, length_cons, Nat.mul_add, Nat.mul_one, Nat.add_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem HasLineDerivAt.smul (h : HasLineDerivAt 𝕜 f f' x v) (c : 𝕜) :
    HasLineDerivAt 𝕜 f (c • f') x (c • v)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
f' : F
h : HasLineDerivAt 𝕜 f f' x v
c : 𝕜
⊢ HasLineDerivAt 𝕜 f (c • f') x (c • v)

Tactic:
simp only [← hasLineDerivWithinAt_univ] at h ⊢

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
f' : F
c : 𝕜
h : HasLineDerivWithinAt 𝕜 f f' univ x v
⊢ HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
f' : F
c : 𝕜
h : HasLineDerivWithinAt 𝕜 f f' univ x v
⊢ HasLineDerivWithinAt 𝕜 f (c • f') univ x (c • v)

Tactic:
exact HasLineDerivWithinAt.smul h c

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem rank_closure_finite_le_nat_card (s : Set G) [Finite s] :
    Group.rank (closure s) ≤ Nat.card s

Proof state:
G : Type u_3
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
⊢ Group.rank ↥(closure s) ≤ Nat.card ↑s

Tactic:
haveI := Fintype.ofFinite s

Result:
G : Type u_3
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank ↥(closure s) ≤ Nat.card ↑s

Proof state:
G : Type u_3
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank ↥(closure ↑s.toFinset) ≤ s.toFinset.card

Tactic:
exact rank_closure_finset_le_card s.toFinset

Result:
no goals

Proof state:
G : Type u_3
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank ↥(closure s) ≤ Nat.card ↑s

Tactic:
rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]

Result:
G : Type u_3
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ Group.rank ↥(closure ↑s.toFinset) ≤ s.toFinset.card
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiffAt.div₀ (hf : ContMDiffAt I' I n f a) (hg : ContMDiffAt I' I n g a)
    (h₀ : g a ≠ 0) : ContMDiffAt I' I n (f / g) a

Proof state:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : ContMDiffInv₀ I n G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f g : M → G
a : M
hf : ContMDiffAt I' I n f a
hg : ContMDiffAt I' I n g a
h₀ : g a ≠ 0
⊢ ContMDiffAt I' I n (f / g) a

Tactic:
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem inseparable_one_iff_norm {a : E} : Inseparable a 1 ↔ ‖a‖ = 0

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ Inseparable a 1 ↔ ‖a‖ = 0

Tactic:
rw [Metric.inseparable_iff, dist_one_right]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem AnalyticAt.sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) :
    AnalyticAt 𝕜 (f - g) x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hf : AnalyticAt 𝕜 f x
hg : AnalyticAt 𝕜 g x
⊢ AnalyticAt 𝕜 (f - g) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_eq_some_getValueCast! [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    [Inhabited (β a)] (h : containsKey a l = true) :
    getValueCast? a l = some (getValueCast! a l)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
a : α
inst✝ : Inhabited (β a)
h : containsKey a l = true
⊢ getValueCast? a l = some (getValueCast! a l)

Tactic:
rw [getValueCast?_eq_some_getValueCast h, getValueCast_eq_getValueCast!]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem inf_left_eq_bot_iff (h : IsCompl y z) : x ⊓ y = ⊥ ↔ x ≤ z

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]

Result:
no goals
-- Mathlib/RingTheory/Smooth/Basic.lean
theorem localization_map [FormallySmooth R S] : FormallySmooth Rₘ Sₘ

Proof state:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
this : FormallySmooth S Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
haveI : FormallySmooth R Sₘ := FormallySmooth.comp R S Sₘ

Result:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
this✝ : FormallySmooth S Sₘ
this : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Proof state:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
this✝ : FormallySmooth S Sₘ
this : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
exact FormallySmooth.localization_base M

Result:
no goals

Proof state:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
⊢ FormallySmooth Rₘ Sₘ

Tactic:
haveI : FormallySmooth S Sₘ := FormallySmooth.of_isLocalization (M.map (algebraMap R S))

Result:
R S Rₘ Sₘ : Type u
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallySmooth R S
this : FormallySmooth S Sₘ
⊢ FormallySmooth Rₘ Sₘ
-- Mathlib/Topology/Connected/Basic.lean
theorem isPreconnected_of_forall_pair {s : Set α}
    (H : ∀ x ∈ s, ∀ y ∈ s, ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t) :
    IsPreconnected s

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)

Result:
case inl
α : Type u
inst✝ : TopologicalSpace α
H : ∀ x ∈ ∅, ∀ y ∈ ∅, ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected ∅

case inr.intro
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
x : α
hx : x ∈ s
⊢ IsPreconnected s

Proof state:
case inl
α : Type u
inst✝ : TopologicalSpace α
H : ∀ x ∈ ∅, ∀ y ∈ ∅, ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected ∅

case inr.intro
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
x : α
hx : x ∈ s
⊢ IsPreconnected s

Tactic:
exacts [isPreconnected_empty, isPreconnected_of_forall x fun y => H x hx y]

Result:
no goals