harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_reverse {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs.reverse → P a) :
    xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse

Proof state:
α : Type ?u.76926
β : Type ?u.76968
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs.reverse → P a
a : α
h : a ∈ xs
⊢ a ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs.reverse → P a
⊢ pmap f xs.reverse H = (pmap f xs ⋯).reverse

Tactic:
induction xs <;> simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_withDensity_eq_setIntegral_smul₀' [SFinite μ] {f : X → ℝ≥0} (s : Set X)
    (hf : AEMeasurable f (μ.restrict s)) (g : X → E)  :
    ∫ x in s, g x ∂μ.withDensity (fun x => f x) = ∫ x in s, f x • g x ∂μ

Proof state:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : X → ℝ≥0
s : Set X
hf : AEMeasurable f (μ.restrict s)
g : X → E
⊢ (∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

Tactic:
rw [restrict_withDensity' s, integral_withDensity_eq_integral_smul₀ hf]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_mul_denom_add_denom_mul_num_ne_zero {x y : RatFunc K} (hxy : x + y ≠ 0) :
    x.num * y.denom + x.denom * y.num ≠ 0

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
⊢ x.num * y.denom + x.denom * y.num ≠ 0

Tactic:
intro h_zero

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
⊢ False

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
⊢ False

Tactic:
rw [h_zero, zero_mul] at h

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = 0
⊢ False

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
⊢ False

Tactic:
have h := num_denom_add x y

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
⊢ False

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hxy : x + y ≠ 0
h_zero : x.num * y.denom + x.denom * y.num = 0
h : (x + y).num * (x.denom * y.denom) = 0
⊢ False

Tactic:
exact (mul_ne_zero (num_ne_zero hxy) (mul_ne_zero x.denom_ne_zero y.denom_ne_zero)) h

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem exists_mem_target {p : β → Prop} : (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (e x)

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (↑e x)

Tactic:
rw [← image_source_eq_target, exists_mem_image]

Result:
no goals
-- Mathlib/Topology/FiberBundle/IsHomeomorphicTrivialBundle.lean
theorem continuous_proj (h : IsHomeomorphicTrivialFiberBundle F proj) :
    Continuous proj

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Continuous proj

Tactic:
obtain ⟨e, rfl⟩ := h.proj_eq

Result:
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)
⊢ Continuous (Prod.fst ∘ ⇑e)

Proof state:
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)
⊢ Continuous (Prod.fst ∘ ⇑e)

Tactic:
exact continuous_fst.comp e.continuous

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_singleton (x : PSet) : rank {x} = succ (rank x) :=
  (rank_insert _ _).trans (by simp)

Proof state:
x : PSet.{u_1}
⊢ succ x.rank ⊔ ∅.rank = succ x.rank

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Union.lean
theorem sup_biUnion [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
    (s.biUnion t).sup f = s.sup fun x => (t x).sup f :=
  eq_of_forall_ge_iff fun c => by simp [@forall_swap _ β]

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
f : β → α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq β
s : Finset γ
t : γ → Finset β
c : α
⊢ (s.biUnion t).sup f ≤ c ↔ (s.sup fun x => (t x).sup f) ≤ c

Tactic:
simp [@forall_swap _ β]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem one_fin_three : (1 : Matrix (Fin 3) (Fin 3) α) = !![1, 0, 0; 0, 1, 0; 0, 0, 1]

Proof state:
case a
α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 3
⊢ 1 i j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = !![1, 0, 0; 0, 1, 0; 0, 0, 1]

Tactic:
ext i j

Result:
case a
α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 3
⊢ 1 i j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] i j
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_smul_one (p : R[X]) :
    matPolyEquiv (p • (1 : Matrix n n R[X])) = p.map (algebraMap R (Matrix n n R))

Proof state:
case a.a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ (matPolyEquiv (p • 1)).coeff m i j = (Polynomial.map (algebraMap R (Matrix n n R)) p).coeff m i j

Tactic:
simp only [matPolyEquiv_coeff_apply, smul_apply, one_apply, smul_eq_mul, mul_ite, mul_one,
  mul_zero, coeff_map, algebraMap_matrix_apply, Algebra.id.map_eq_id, RingHom.id_apply]

Result:
case a.a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
⊢ matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p

Tactic:
ext m i j

Result:
case a.a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ (matPolyEquiv (p • 1)).coeff m i j = (Polynomial.map (algebraMap R (Matrix n n R)) p).coeff m i j

Proof state:
case a.a
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ (if i = j then p else 0).coeff m = if i = j then p.coeff m else 0

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_of_not_mem [LawfulBEq α] {a : α} {l : Array α} (h : a ∉ l) : l.erase a = l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : ¬a ∈ l
⊢ l.erase a = l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ { toList := l }
⊢ { toList := l }.erase a = { toList := l }

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ { toList := l }
⊢ ¬?m.30621 ∈ ?m.30622

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ { toList := l }
⊢ { toList := l }.erase a = { toList := l }

Tactic:
simp [List.erase_of_not_mem (by simpa using h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_set (a b : α) (v : Vector α n) (i : Nat) (hi : i < n) :
    (v.set i a hi).set i b hi = v.set i b hi

Proof state:
case mk
α : Type u_1
n : Nat
a b : α
i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a hi).set i b hi =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.set i b hi

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a b : α
v : Vector α n
i : Nat
hi : i < n
⊢ (v.set i a hi).set i b hi = v.set i b hi

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
a b : α
i : Nat
hi : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i a hi).set i b hi =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.set i b hi
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasStrictDerivAt_const_rpow_of_neg {a x : ℝ} (ha : a < 0) :
    HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a - exp (log a * x) * sin (x * π) * π) x

Proof state:
a x : ℝ
ha : a < 0
⊢ HasStrictDerivAt (fun x => a ^ x) (a ^ x * log a - rexp (log a * x) * sin (x * π) * π) x

Tactic:
simpa using (hasStrictFDerivAt_rpow_of_neg (a, x) ha).comp_hasStrictDerivAt x
  ((hasStrictDerivAt_const _ _).prod (hasStrictDerivAt_id _))

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem edist_inv_inv [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G]
    (a b : G) : edist a⁻¹ b⁻¹ = edist a b

Proof state:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
⊢ edist a⁻¹ b⁻¹ = edist a b

Tactic:
rw [← edist_mul_left a, ← edist_mul_right _ _ b, mul_inv_cancel, one_mul, inv_mul_cancel_right,
  edist_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_add_of_nonpos {A : M} {m n : ℤ} (hm : m ≤ 0) (hn : n ≤ 0) :
    A ^ (m + n) = A ^ m * A ^ n

Proof state:
case inr.intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)

Tactic:
simp_rw [← neg_add, ← Int.ofNat_add, zpow_neg_natCast, ← inv_pow', h, pow_add]

Result:
no goals

Proof state:
case inr.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : n ≤ 0
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
⊢ A ^ (-↑k + n) = A ^ (-↑k) * A ^ n

Tactic:
obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn

Result:
case inr.intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
l : ℕ
hn : -↑l ≤ 0
⊢ A ^ (-↑k + -↑l) = A ^ (-↑k) * A ^ (-↑l)

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h)

Result:
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (m + n) = A ^ m * A ^ n

case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ = 0
⊢ A ^ (m + n) = A ^ m * A ^ n

Proof state:
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
exact zpow_add (isUnit_det_of_left_inverse h) m n

Result:
no goals

Proof state:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ = 0
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm

Result:
case inr.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : n ≤ 0
h : A⁻¹ = 0
k : ℕ
hm : -↑k ≤ 0
⊢ A ^ (-↑k + n) = A ^ (-↑k) * A ^ n
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma integrable_llr_tilted_left [IsFiniteMeasure μ] [SigmaFinite ν]
    (hμν : μ ≪ ν) (hf : Integrable f μ) (h_int : Integrable (llr μ ν) μ)
    (hfμ : Integrable (fun x ↦ exp (f x)) μ) (hfν : AEMeasurable f ν) :
    Integrable (llr (μ.tilted f) ν) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (llr (μ.tilted f) ν) μ

Tactic:
rw [integrable_congr (llr_tilted_left hμν hfμ hfν)]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (fun x => f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (fun x => f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ

Tactic:
exact Integrable.add (hf.sub (integrable_const _)) h_int

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
lemma IsInitial.isZero {X : C} (hX : IsInitial X) : IsZero X

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsInitial X
⊢ 𝟙 X = 0

Tactic:
apply hX.hom_ext

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsInitial X
⊢ IsZero X

Tactic:
rw [IsZero.iff_id_eq_zero]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsInitial X
⊢ 𝟙 X = 0
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem toFinset_sum_count_eq (s : Multiset α) : ∑ a ∈ s.toFinset, s.count a = card s

Proof state:
α : Type u_3
inst✝ : DecidableEq α
s : Multiset α
⊢ ∑ a ∈ s.toFinset, count a s = s.card

Tactic:
simpa using (Finset.sum_multiset_map_count s (fun _ => (1 : ℕ))).symm

Result:
no goals
-- Mathlib/Analysis/Complex/IntegerCompl.lean
lemma integerComplement.ne_zero {x : ℂ} (hx : x ∈ ℂ_ℤ) : x ≠ 0 :=
  fun hx' ↦ hx ⟨0, by exact_mod_cast hx'.symm⟩

Proof state:
x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 0
⊢ ↑0 = x

Tactic:
exact_mod_cast hx'.symm

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_Ioi_of_hasDerivAt_of_tendsto' (hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x)
    (f'int : IntegrableOn f' (Ioi a)) (hf : Tendsto f atTop (𝓝 m)) :
    ∫ x in Ioi a, f' x = m - f a

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
⊢ ∫ (x : ℝ) in Ioi a, f' x = m - f a

Tactic:
refine integral_Ioi_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le)
  f'int hf

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
⊢ ContinuousWithinAt f (Ici a) a

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
exact (hderiv a left_mem_Ici).continuousAt.continuousWithinAt

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma eq_of_dvd_of_div_eq_one (hab : a ∣ b) (h : b / a = 1) : a = b

Proof state:
a b : ℕ
hab : a ∣ b
h : b / a = 1
⊢ a = b

Tactic:
rw [← Nat.div_mul_cancel hab, h, Nat.one_mul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isCharThreeJNeZeroNF : W.c₆ = -64 * W.a₂ ^ 3 - 864 * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.c₆ = -64 * W.a₂ ^ 3 - 864 * W.a₆

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs

Proof state:
case mk.mk
α : Type u
toList✝¹ toList✝ : List α
h : toList✝¹ = toList✝
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Tactic:
rw [h]

Result:
no goals

Proof state:
case mk.mk
α : Type u
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.toList = { toList := toList✝ }.toList
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Tactic:
simp at h

Result:
case mk.mk
α : Type u
toList✝¹ toList✝ : List α
h : toList✝¹ = toList✝
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Proof state:
case mk
α : Type u
bs : Array α
toList✝ : List α
h : { toList := toList✝ }.toList = bs.toList
⊢ { toList := toList✝ } = bs

Tactic:
cases bs

Result:
case mk.mk
α : Type u
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.toList = { toList := toList✝ }.toList
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Proof state:
α : Type u
as bs : Array α
h : as.toList = bs.toList
⊢ as = bs

Tactic:
cases as

Result:
case mk
α : Type u
bs : Array α
toList✝ : List α
h : { toList := toList✝ }.toList = bs.toList
⊢ { toList := toList✝ } = bs
-- Mathlib/Data/Finset/Card.lean
theorem card_inter_add_card_union (s t : Finset α) :
    #(s ∩ t) + #(s ∪ t) = #s + #t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s ∪ t) = #s + #t

Tactic:
rw [Nat.add_comm, card_union_add_card_inter]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem separatingLeft_of_anisotropic [Invertible (2 : R)] (Q : QuadraticMap R M R)
    (hB : Q.Anisotropic) :
    -- Porting note: added implicit argument
    (QuadraticMap.associated' (R := R) (N := R) Q).SeparatingLeft := fun x hx ↦ hB _ <| by
  rw [← hx x]
  exact (associated_eq_self_apply _ _ x).symm

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = ((associated' Q) x) x

Tactic:
exact (associated_eq_self_apply _ _ x).symm

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = 0

Tactic:
rw [← hx x]

Result:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticMap R M R
hB : Q.Anisotropic
x : M
hx : ∀ (y : M), ((associated' Q) x) y = 0
⊢ Q x = ((associated' Q) x) x
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma toReal_klDiv (h : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    (klDiv μ ν).toReal = ∫ a, llr μ ν a ∂μ + (ν univ).toReal - (μ univ).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ + (ν univ).toReal - (μ univ).toReal

Tactic:
rw [klDiv_of_ac_of_integrable h h_int, ENNReal.toReal_ofReal]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Tactic:
exact integral_llr_add_sub_measure_univ_nonneg h h_int

Result:
no goals
-- Mathlib/Algebra/Group/NatPowAssoc.lean
theorem Int.cast_npow (R : Type*) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R]
    (n : ℤ) : ∀(m : ℕ), @Int.cast R NonAssocRing.toIntCast (n ^ m) = (n : R) ^ m
  | 0 => by
    rw [pow_zero, npow_zero, Int.cast_one]
  | m + 1 => by
    rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
⊢ ↑(n ^ 0) = ↑n ^ 0

Tactic:
rw [pow_zero, npow_zero, Int.cast_one]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
m : ℕ
⊢ ↑(n ^ (m + 1)) = ↑n ^ (m + 1)

Tactic:
rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem sum_restrict_disjointed_spanningSets (μ ν : Measure α) [SigmaFinite ν] :
    sum (fun n ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite ν
⊢ (sum fun n => μ.restrict (disjointed (spanningSets ν) n)) = μ

Tactic:
rw [← restrict_iUnion (disjoint_disjointed _)
    (MeasurableSet.disjointed (measurableSet_spanningSets _)),
  iUnion_disjointed, iUnion_spanningSets, restrict_univ]

Result:
no goals
-- Mathlib/Algebra/Lie/Engel.lean
theorem LieAlgebra.isEngelian_of_subsingleton [Subsingleton L] : LieAlgebra.IsEngelian R L

Proof state:
case h
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
⊢ lowerCentralSeries ℤ L M 1 = ⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
⊢ IsEngelian R L

Tactic:
intro M _i1 _i2 _i3 _i4 _h

Result:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
⊢ LieModule.IsNilpotent L M

Proof state:
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
⊢ LieModule.IsNilpotent L M

Tactic:
use 1

Result:
case h
R : Type u₁
L : Type u₂
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : Subsingleton L
M : Type u_1
_i1 : AddCommGroup M
_i2 : Module R M
_i3 : LieRingModule L M
_i4 : LieModule R L M
_h : ∀ (x : L), IsNilpotent ((toEnd R L M) x)
⊢ lowerCentralSeries ℤ L M 1 = ⊥
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem map_one_of_isLeftRegular (h : IsLeftRegular (abv 1)) : abv 1 = 1 :=
  h <| by simp [← abv.map_mul]

Proof state:
R : Type u_5
S : Type u_6
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
h : IsLeftRegular (abv 1)
⊢ (fun x => abv 1 * x) (abv 1) = (fun x => abv 1 * x) 1

Tactic:
simp [← abv.map_mul]

Result:
no goals