harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_source'' : (e.trans e').source = e.symm '' (e.target ∩ e'.source)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)

Tactic:
rw [e.trans_source', e.symm_image_target_inter_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_bne : ∀ (a b : Bool), ((!a) != b) = !(a != b)

Proof state:
⊢ ∀ (a b : Bool), ((!a) != b) = !a != b

Tactic:
decide

Result:
no goals
-- Mathlib/Tactic/Ring/RingNF.lean
theorem int_rawCast_neg {R} [Ring R] : (Int.rawCast (.negOfNat n) : R) = -Nat.rawCast n

Proof state:
n : ℕ
R : Type u_2
inst✝ : Ring R
⊢ (Int.negOfNat n).rawCast = -n.rawCast

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_eq_of_eq_mul_left {a b c : Int}
    (H1 : b ≠ 0) (H2 : a = c * b) : a / b = c :=
  Int.ediv_eq_of_eq_mul_right H1 (by rw [Int.mul_comm, H2])

Proof state:
a b c : Int
H1 : b ≠ 0
H2 : a = c * b
⊢ a = b * c

Tactic:
rw [Int.mul_comm, H2]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_exp : ∫ x in a..b, exp x = exp b - exp a

Proof state:
case hcont
a b : ℝ
⊢ ContinuousOn rexp [[a, b]]

Tactic:
exact continuousOn_exp

Result:
no goals

Proof state:
case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x

Tactic:
exact fun _ _ => differentiableAt_exp

Result:
no goals

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a

Tactic:
rw [integral_deriv_eq_sub']

Result:
case hderiv
a b : ℝ
⊢ deriv rexp = rexp

case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ rexp x

case hcont
a b : ℝ
⊢ ContinuousOn rexp [[a, b]]

Proof state:
case hderiv
a b : ℝ
⊢ deriv rexp = rexp

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem dvd_mul_gcd_of_dvd_mul [GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ m * gcd k n

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ n * m
⊢ k ∣ gcd k n * m

Tactic:
exact dvd_gcd_mul_of_dvd_mul H

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ k ∣ m * gcd k n

Tactic:
rw [mul_comm] at H ⊢

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ n * m
⊢ k ∣ gcd k n * m
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_toArray (l : List (List α)) :
    (l.toArray.map List.toArray).flatten = l.flatten.toArray

Proof state:
case h
α : Type u_1
l : List (List α)
⊢ (Array.map toArray l.toArray).flatten.toList = l.flatten.toArray.toList

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
l : List (List α)
⊢ (Array.map toArray l.toArray).flatten = l.flatten.toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List (List α)
⊢ (Array.map toArray l.toArray).flatten.toList = l.flatten.toArray.toList
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma leadingCoeff_Φ [Nontrivial R] (n : ℤ) : (W.Φ n).leadingCoeff = 1

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
⊢ (W.Φ n).leadingCoeff = 1

Tactic:
rw [leadingCoeff, natDegree_Φ, coeff_Φ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_mapIdx_iff {l : List α} :
    mapIdx f l = mapIdx g l ↔ ∀ i : Nat, (h : i < l.length) → f i l[i] = g i l[i]

Proof state:
case mpr.h
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
⊢ ∀ (i : Nat) (h₁ : i < (mapIdx f l).length) (h₂ : i < (mapIdx g l).length), (mapIdx f l)[i] = (mapIdx g l)[i]

Tactic:
intro i h₁ h₂

Result:
case mpr.h
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
i : Nat
h₁ : i < (mapIdx f l).length
h₂ : i < (mapIdx g l).length
⊢ (mapIdx f l)[i] = (mapIdx g l)[i]

Proof state:
case mpr.h
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
i : Nat
h₁ : i < (mapIdx f l).length
h₂ : i < (mapIdx g l).length
⊢ (mapIdx f l)[i] = (mapIdx g l)[i]

Tactic:
simp [w]

Result:
no goals

Proof state:
case mp
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : mapIdx f l = mapIdx g l
i : Nat
h : i < l.length
⊢ f i l[i] = g i l[i]

Tactic:
simpa [h] using congrArg (fun l => l[i]?) w

Result:
no goals

Proof state:
case mpr.hl
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
⊢ (mapIdx f l).length = (mapIdx g l).length

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
⊢ mapIdx f l = mapIdx g l → ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]

Tactic:
intro w i h

Result:
case mp
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : mapIdx f l = mapIdx g l
i : Nat
h : i < l.length
⊢ f i l[i] = g i l[i]

Proof state:
case mpr
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
⊢ mapIdx f l = mapIdx g l

Tactic:
apply ext_getElem

Result:
case mpr.hl
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
⊢ (mapIdx f l).length = (mapIdx g l).length

case mpr.h
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
⊢ ∀ (i : Nat) (h₁ : i < (mapIdx f l).length) (h₂ : i < (mapIdx g l).length), (mapIdx f l)[i] = (mapIdx g l)[i]

Proof state:
case mpr
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
⊢ (∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]) → mapIdx f l = mapIdx g l

Tactic:
intro w

Result:
case mpr
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
w : ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
⊢ mapIdx f l = mapIdx g l

Proof state:
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
⊢ mapIdx f l = mapIdx g l ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]

Tactic:
constructor

Result:
case mp
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
⊢ mapIdx f l = mapIdx g l → ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]

case mpr
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : List α
⊢ (∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]) → mapIdx f l = mapIdx g l
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem lt_one_div (ha : 0 < a) (hb : 0 < b) : a < 1 / b ↔ b < 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
hb : 0 < b
⊢ a < 1 / b ↔ b < 1 / a

Tactic:
simpa using lt_inv_comm₀ ha hb

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma disjointSum_indep_iff {h I} :
    (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
⊢ (M.disjointSum N h).Indep I ↔ M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E

Tactic:
simp [disjointSum, and_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPushout.inl_iso_inv :
    G.map (pushout.inl _ _) ≫ (PreservesPushout.iso G f g).inv = pushout.inl _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ G.map (pushout.inl f g) ≫ (iso G f g).inv = pushout.inl (G.map f) (G.map g)

Tactic:
simp [PreservesPushout.iso, Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem norm [NumberField K] (x : (𝓞 K)ˣ) :
    |Algebra.norm ℚ (x : K)| = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ |(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑x)| = 1

Tactic:
rw [← RingOfIntegers.coe_norm, isUnit_iff_norm.mp x.isUnit]

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem proj_of_mem {t : ℝ} (ht : t ∈ Icc v.tMin v.tMax) : ↑(v.proj t) = t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
t : ℝ
ht : t ∈ Icc v.tMin v.tMax
⊢ ↑(v.proj t) = t

Tactic:
simp only [proj, projIcc_of_mem v.tMin_le_tMax ht]

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicator_mono {δ₁ δ₂ : ℝ} (δ₁_pos : 0 < δ₁) (δ₂_pos : 0 < δ₂) (hle : δ₁ ≤ δ₂)
    (E : Set α) : ⇑(thickenedIndicator δ₁_pos E) ≤ thickenedIndicator δ₂_pos E

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
⊢ ⇑(thickenedIndicator δ₁_pos E) ≤ ⇑(thickenedIndicator δ₂_pos E)

Tactic:
intro x

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ (thickenedIndicator δ₁_pos E) x ≤ (thickenedIndicator δ₂_pos E) x

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ (thickenedIndicator δ₁_pos E) x ≤ (thickenedIndicator δ₂_pos E) x

Tactic:
apply (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne thickenedIndicatorAux_lt_top.ne).mpr

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x

Tactic:
apply thickenedIndicatorAux_mono hle

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_iff (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
    QuasiIsoAt f i ↔
      ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Proof state:
case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f) → QuasiIsoAt f i

Tactic:
intro h

Result:
case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
h : ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)
⊢ QuasiIsoAt f i

Proof state:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
h : QuasiIsoAt f i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
exact h.quasiIso

Result:
no goals

Proof state:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i → ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
intro h

Result:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
h : QuasiIsoAt f i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Proof state:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i ↔ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
constructor

Result:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i → ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f) → QuasiIsoAt f i

Proof state:
case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
h : ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)
⊢ QuasiIsoAt f i

Tactic:
exact ⟨h⟩

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Basic.lean
lemma val_sum_apply {ι : Type*} (s : Finset ι) (f : ι → AdicCompletion I M) (n : ℕ) :
    (∑ i ∈ s, f i).val n = ∑ i ∈ s, (f i).val n

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_6
s : Finset ι
f : ι → AdicCompletion I M
n : ℕ
⊢ ↑(∑ i ∈ s, f i) n = ∑ i ∈ s, ↑(f i) n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_add_natCast {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
simpa using rpow_add_intCast hx y n

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/Basic.lean
protected lemma leibniz_lie (x : L) (D₁ D₂ : LieDerivation R L L) :
    ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆

Proof state:
case H
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D₁ D₂ : LieDerivation R L L
y : L
⊢ ⁅x, ⁅D₁, D₂⁆⁆ y = (⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆) y

Tactic:
simp [-lie_skew, ← lie_skew (D₁ x) (D₂ y), ← lie_skew (D₂ x) (D₁ y), sub_eq_neg_add]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D₁ D₂ : LieDerivation R L L
⊢ ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆

Tactic:
ext y

Result:
case H
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
D₁ D₂ : LieDerivation R L L
y : L
⊢ ⁅x, ⁅D₁, D₂⁆⁆ y = (⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆) y
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem isNilpotent_range_toEnd_iff :
    IsNilpotent (toEnd R L M).range M ↔ IsNilpotent L M

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ (∃ k, lowerCentralSeries R (↥(toEnd R L M).range) M k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
constructor <;> rintro ⟨k, hk⟩ <;> use k <;>
    rw [← LieSubmodule.toSubmodule_inj] at hk ⊢ <;>
  simpa using hk

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ IsNilpotent (↥(toEnd R L M).range) M ↔ IsNilpotent L M

Tactic:
simp only [isNilpotent_iff R _ M]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ (∃ k, lowerCentralSeries R (↥(toEnd R L M).range) M k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k = ⊥
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getElem_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
    (x + y)[i] = (x[i] ^^ (y[i] ^^ carry i x y false))

Proof state:
w i : Nat
i_lt : i < w
x y : BitVec w
⊢ (x + y)[i] = (x[i] ^^ (y[i] ^^ carry i x y false))

Tactic:
simpa using getElem_add_add_bool i_lt x y false

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_mul_le_iff₀'` for a version with multiplication on the other side. -/
lemma inv_mul_le_iff₀ (hc : 0 < c) : c⁻¹ * b ≤ a ↔ b ≤ c * a where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hc : 0 < c
h : b ≤ c * a
⊢ c⁻¹ * b ≤ a

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_left h (inv_nonneg.2 hc.le)

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulMono G₀
hc : 0 < c
h : c⁻¹ * b ≤ a
⊢ b ≤ c * a

Tactic:
simpa [hc.ne'] using mul_le_mul_of_nonneg_left h hc.le

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
theorem basicOpen_zero (X : LocallyRingedSpace.{u}) (U : Opens X.carrier) :
    X.toRingedSpace.basicOpen (0 : X.presheaf.obj <| op U) = ⊥

Proof state:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x ⋯)) 0)

Tactic:
rw [map_zero, isUnit_zero_iff]

Result:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1

Proof state:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
⊢ ∀ (x_1 : x ∈ U), ¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x ⋯)) 0)

Tactic:
intros hx

Result:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x ⋯)) 0)

Proof state:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1

Tactic:
change (0 : X.presheaf.stalk x) ≠ (1 : X.presheaf.stalk x)

Result:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ 0 ≠ 1

Proof state:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
⊢ x ∈ ↑(X.toRingedSpace.basicOpen 0) ↔ x ∈ ↑⊥

Tactic:
simp only [RingedSpace.basicOpen, Opens.coe_mk, Set.mem_image, Set.mem_setOf_eq, Subtype.exists,
  exists_and_right, exists_eq_right, Opens.coe_bot, Set.mem_empty_iff_false,
  iff_false, not_exists]

Result:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
⊢ ∀ (x_1 : x ∈ U), ¬IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x ⋯)) 0)

Proof state:
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ X.toRingedSpace.basicOpen 0 = ⊥

Tactic:
ext x

Result:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
⊢ x ∈ ↑(X.toRingedSpace.basicOpen 0) ↔ x ∈ ↑⊥

Proof state:
case h.h
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toRingedSpace.toPresheafedSpace
hx : x ∈ U
⊢ 0 ≠ 1

Tactic:
exact zero_ne_one

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range

Proof state:
G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤

Tactic:
exact (⊤ : Subgroup G).map_map g f

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g f.range = (g.comp f).range

Tactic:
rw [range_eq_map, range_eq_map]

Result:
G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem top_caratheodory : (⊤ : OuterMeasure α).caratheodory = ⊤ :=
  top_unique fun s _ =>
    (isCaratheodory_iff_le _).2 fun t =>
      t.eq_empty_or_nonempty.elim (fun ht => by simp [ht]) fun ht => by
        simp only [ht, top_apply, le_top]

Proof state:
α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : t.Nonempty
⊢ ⊤ (t ∩ s) + ⊤ (t \ s) ≤ ⊤ t

Tactic:
simp only [ht, top_apply, le_top]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : t = ∅
⊢ ⊤ (t ∩ s) + ⊤ (t \ s) ≤ ⊤ t

Tactic:
simp [ht]

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem separableClosure.map_eq_of_algEquiv (i : E ≃ₐ[F] K) :
    (separableClosure F E).map i = separableClosure F K :=
  (map_le_of_algHom i.toAlgHom).antisymm
    (fun x h ↦ ⟨_, (map_mem_separableClosure_iff i.symm).2 h, by simp⟩)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E ≃ₐ[F] K
x : K
h : x ∈ separableClosure F K
⊢ ↑↑i (↑i.symm x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Ioc_iff_integrableOn_Ioo' (hb : μ {b} ≠ ∞) :
    IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [← Ioo_union_right hab, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
by_cases hab : a < b

Result:
case pos
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : a < b
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
hb : μ {b} ≠ ⊤
hab : ¬a < b
⊢ IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [Ioo_eq_empty hab, Ioc_eq_empty hab]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Box.lean
@[simp] lemma card_box_succ (n : ℕ) :
    #(box (n + 1) : Finset (α × β)) =
      #(Icc (-n.succ : α) n.succ) * #(Icc (-n.succ : β) n.succ) -
        #(Icc (-n : α) n) * #(Icc (-n : β) n)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : OrderedRing α
inst✝⁵ : OrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
n : ℕ
⊢ #(Icc (-↑n.succ).1 (↑n.succ).1) * #(Icc (-↑n.succ).2 (↑n.succ).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : OrderedRing α
inst✝⁵ : OrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
n : ℕ
⊢ #(box (n + 1)) = #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
rw [box_succ_eq_sdiff, card_sdiff (Icc_neg_mono n.le_succ), Finset.card_Icc_prod,
  Finset.card_Icc_prod]

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : OrderedRing α
inst✝⁵ : OrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
n : ℕ
⊢ #(Icc (-↑n.succ).1 (↑n.succ).1) * #(Icc (-↑n.succ).2 (↑n.succ).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)