harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.exists_partsEquiv (hP : P.IsEquipartition) :
    ∃ f : P.parts ≃ Fin #P.parts, ∀ t, #t.1 = #s / #P.parts + 1 ↔ f t < #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
replace es : { x : P.parts // ¬#x.1 = #s / #P.parts + 1 } ≃
    Fin (#P.parts - #s % #P.parts) := (Equiv.Set.sep ..).symm.trans (sneg.trans es)

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
sneg : { x // x ∈ P.parts ∧ ¬#x = #s / #P.parts + 1 } ≃ { x // x ∈ P.parts ∧ #x = #s / #P.parts } :=
  (Equiv.refl (Finset α)).subtypeEquiv ⋯
el : { x // #↑x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // ¬#↑x = #s / #P.parts + 1 } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∃ f, ∀ (t : { x // x ∈ P.parts }), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts
-- Mathlib/LinearAlgebra/Semisimple.lean
protected lemma _root_.LinearEquiv.isSemisimple_iff {M₂ : Type*} [AddCommGroup M₂] [Module R M₂]
    (g : End R M₂) (e : M ≃ₗ[R] M₂) (he : e ∘ₗ f = g ∘ₗ e) :
    f.IsSemisimple ↔ g.IsSemisimple

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e✝ : M ≃ₗ[R] M₂
he : ↑e✝ ∘ₗ f = g ∘ₗ ↑e✝
e : AEval' f ≃ₗ[R[X]] AEval' g := LinearEquiv.ofAEval f (e✝ ≪≫ₗ AEval'.of g) ⋯
⊢ f.IsSemisimple ↔ g.IsSemisimple

Tactic:
exact (Submodule.orderIsoMapComap e).complementedLattice_iff

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e : M ≃ₗ[R] M₂
he : ↑e ∘ₗ f = g ∘ₗ ↑e
x : M
⊢ (e ≪≫ₗ AEval'.of g) (f • x) = X • (e ≪≫ₗ AEval'.of g) x

Tactic:
simpa [AEval'.X_smul_of] using LinearMap.congr_fun he x

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e : M ≃ₗ[R] M₂
he : ↑e ∘ₗ f = g ∘ₗ ↑e
⊢ f.IsSemisimple ↔ g.IsSemisimple

Tactic:
let e : AEval' f ≃ₗ[R[X]] AEval' g := LinearEquiv.ofAEval _ (e.trans (AEval'.of g)) fun x ↦ by
  simpa [AEval'.X_smul_of] using LinearMap.congr_fun he x

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
M₂ : Type u_3
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
g : End R M₂
e✝ : M ≃ₗ[R] M₂
he : ↑e✝ ∘ₗ f = g ∘ₗ ↑e✝
e : AEval' f ≃ₗ[R[X]] AEval' g := LinearEquiv.ofAEval f (e✝ ≪≫ₗ AEval'.of g) ⋯
⊢ f.IsSemisimple ↔ g.IsSemisimple
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_smul {a : ℤ√d} {n : ℕ} (ha : Nonneg a) : Nonneg ((n : ℤ√d) * a)

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ { re := ↑n * -↑x, im := ↑n * ↑y }.Nonneg

Tactic:
simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
x y : ℕ
x✝ : { re := ↑x, im := ↑y }.Nonneg
⊢ { re := ↑n * ↑x, im := ↑n * ↑y }.Nonneg

Tactic:
trivial

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
⊢ (↑↑n * a).Nonneg

Tactic:
exact
  match a, nonneg_cases ha, ha with
  | _, ⟨x, y, Or.inl rfl⟩, _ => by rw [smul_val]; trivial
  | _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by
    rw [smul_val]; simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)
  | _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by
    rw [smul_val]; simpa using nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
x y : ℕ
x✝ : { re := ↑x, im := ↑y }.Nonneg
⊢ (↑↑n * { re := ↑x, im := ↑y }).Nonneg

Tactic:
rw [smul_val]

Result:
d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
x y : ℕ
x✝ : { re := ↑x, im := ↑y }.Nonneg
⊢ { re := ↑n * ↑x, im := ↑n * ↑y }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ (↑↑n * { re := ↑x, im := -↑y }).Nonneg

Tactic:
rw [smul_val]

Result:
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ { re := ↑n * ↑x, im := ↑n * -↑y }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ { re := ↑n * ↑x, im := ↑n * -↑y }.Nonneg

Tactic:
simpa using nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ (↑↑n * { re := -↑x, im := ↑y }).Nonneg

Tactic:
rw [smul_val]

Result:
d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ { re := ↑n * -↑x, im := ↑n * ↑y }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
⊢ (↑n * a).Nonneg

Tactic:
rw [← Int.cast_natCast n]

Result:
d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
⊢ (↑↑n * a).Nonneg
-- Mathlib/Data/Set/Pairwise/Basic.lean
lemma exists_ne_mem_inter_of_not_pairwise_disjoint
    {f : ι → Set α} (h : ¬ Pairwise (Disjoint on f)) :
    ∃ i j : ι, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_4
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_4
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨i, j, h⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
rw [← pairwise_univ] at h

Result:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
-- Mathlib/Order/CompleteLattice.lean
lemma disjoint_of_sSup_disjoint_of_le_of_le {a b : α} {c d : Set α} (hs : ∀ e ∈ c, e ≤ a)
    (ht : ∀ e ∈ d, e ≤ b) (hd : Disjoint a b) (he : ⊥ ∉ c ∨ ⊥ ∉ d) : Disjoint c d

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
x : α
hx : x ∈ c
y : α
hy : y ∈ d
⊢ x ≠ y

Tactic:
rw [Disjoint.ne_iff]

Result:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
x : α
hx : x ∈ c
y : α
hy : y ∈ d
⊢ x ≠ ⊥ ∨ y ≠ ⊥

α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
x : α
hx : x ∈ c
y : α
hy : y ∈ d
⊢ Disjoint x y

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
⊢ ∀ ⦃a : α⦄, a ∈ c → ∀ ⦃b : α⦄, b ∈ d → a ≠ b

Tactic:
intros x hx y hy

Result:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
x : α
hx : x ∈ c
y : α
hy : y ∈ d
⊢ x ≠ y

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
x : α
hx : x ∈ c
y : α
hy : y ∈ d
⊢ x ≠ ⊥ ∨ y ≠ ⊥

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
x : α
hx : x ∈ c
y : α
hy : y ∈ d
⊢ Disjoint x y

Tactic:
exact Disjoint.mono (hs x hx) (ht y hy) hd

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
⊢ Disjoint c d

Tactic:
rw [disjoint_iff_forall_ne]

Result:
α : Type u_1
inst✝ : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
⊢ ∀ ⦃a : α⦄, a ∈ c → ∀ ⦃b : α⦄, b ∈ d → a ≠ b
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem coeff_eq_zero : p.coeff n = 0 ↔ p n = 0

Proof state:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ p.coeff n = 0 ↔ p n = 0

Tactic:
rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_injective : Injective (image f) ↔ Injective f

Proof state:
case a
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ f '' {x} = f '' {x'}

Tactic:
rw [image_singleton, image_singleton, hx]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {x} = {x'}

Tactic:
apply h

Result:
case a
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ f '' {x} = f '' {x'}

Proof state:
α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f

Tactic:
refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩

Result:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ x = x'

Proof state:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ x = x'

Tactic:
rw [← singleton_eq_singleton_iff]

Result:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {x} = {x'}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
    (m.erase k).getKey? k = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
⊢ (m.erase k).getKey? k = none

Tactic:
simp_to_model [erase] using List.getKey?_eraseKey_self

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_iff_of_model_completeTheory [N ⊨ L.completeTheory M] (φ : L.Sentence) :
    N ⊨ φ ↔ M ⊨ φ

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
⊢ N ⊨ φ ↔ M ⊨ φ

Tactic:
refine ⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩

Result:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : N ⊨ φ
⊢ M ⊨ φ

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : M ⊨ Formula.not φ
⊢ N ⊨ Formula.not φ

Tactic:
exact (L.completeTheory M).realize_sentence_of_mem (mem_completeTheory.2 h)

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : N ⊨ φ
⊢ M ⊨ φ

Tactic:
contrapose! h

Result:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : ¬M ⊨ φ
⊢ ¬N ⊨ φ

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : ¬M ⊨ φ
⊢ ¬N ⊨ φ

Tactic:
rw [← Sentence.realize_not] at *

Result:
L : Language
M : Type w
N : Type u_1
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : N ⊨ L.completeTheory M
φ : L.Sentence
h : M ⊨ Formula.not φ
⊢ N ⊨ Formula.not φ
-- Mathlib/Computability/Primrec.lean
theorem list_getElem? : Primrec₂ (fun (l : List α) (n : ℕ) => l[n]?)

Proof state:
α : Type u_1
inst✝ : Primcodable α
⊢ Primrec₂ fun l n => l[n]?

Tactic:
convert list_get?

Result:
case h.e'_7.h.h.h.e
α : Type u_1
inst✝ : Primcodable α
x✝¹ : List α
x✝ : ℕ
⊢ getElem? = List.get?

Proof state:
case h.e'_7.h.h.h.e
α : Type u_1
inst✝ : Primcodable α
x✝¹ : List α
x✝ : ℕ
⊢ getElem? = List.get?

Tactic:
ext

Result:
case h.e'_7.h.h.h.e.h.h.a
α : Type u_1
inst✝ : Primcodable α
x✝³ : List α
x✝² : ℕ
x✝¹ : List α
x✝ : ℕ
a✝ : α
⊢ a✝ ∈ x✝¹[x✝]? ↔ a✝ ∈ x✝¹.get? x✝

Proof state:
case h.e'_7.h.h.h.e.h.h.a
α : Type u_1
inst✝ : Primcodable α
x✝³ : List α
x✝² : ℕ
x✝¹ : List α
x✝ : ℕ
a✝ : α
⊢ a✝ ∈ x✝¹[x✝]? ↔ a✝ ∈ x✝¹.get? x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Box.lean
lemma card_box : ∀ {n}, n ≠ 0 → #(box n : Finset (ℤ × ℤ)) = 8 * n
  | n + 1, _ => by
    simp_rw [Prod.card_box_succ, card_Icc, sub_neg_eq_add]
    norm_cast
    refine tsub_eq_of_eq_add ?_
    zify
    ring

Proof state:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ #(box (n + 1)) = 8 * (n + 1)

Tactic:
simp_rw [Prod.card_box_succ, card_Icc, sub_neg_eq_add]

Result:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (↑n.succ + 1 + ↑n.succ).toNat * (↑n.succ + 1 + ↑n.succ).toNat - (↑n + 1 + ↑n).toNat * (↑n + 1 + ↑n).toNat =
    8 * (n + 1)

Proof state:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (↑n + 1 + 1 + (↑n + 1)) * (↑n + 1 + 1 + (↑n + 1)) = 8 * (↑n + 1) + (↑n + 1 + ↑n) * (↑n + 1 + ↑n)

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)

Tactic:
zify

Result:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (↑n + 1 + 1 + (↑n + 1)) * (↑n + 1 + 1 + (↑n + 1)) = 8 * (↑n + 1) + (↑n + 1 + ↑n) * (↑n + 1 + ↑n)

Proof state:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) - (n + 1 + n) * (n + 1 + n) = 8 * (n + 1)

Tactic:
refine tsub_eq_of_eq_add ?_

Result:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) = 8 * (n + 1) + (n + 1 + n) * (n + 1 + n)

Proof state:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (↑n.succ + 1 + ↑n.succ).toNat * (↑n.succ + 1 + ↑n.succ).toNat - (↑n + 1 + ↑n).toNat * (↑n + 1 + ↑n).toNat =
    8 * (n + 1)

Tactic:
norm_cast

Result:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ (n.succ + 1 + n.succ) * (n.succ + 1 + n.succ) - (n + 1 + n) * (n + 1 + n) = 8 * (n + 1)
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
lemma IsEverywherePos.smul_measure_nnreal (hs : IsEverywherePos μ s) {c : ℝ≥0} (hc : c ≠ 0) :
    IsEverywherePos (c • μ) s :=
  hs.smul_measure (by simpa using hc)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ.IsEverywherePos s
c : ℝ≥0
hc : c ≠ 0
⊢ ↑ENNReal.ofNNRealHom.toMonoidWithZeroHom c ≠ 0

Tactic:
simpa using hc

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_succ_iterate_of_not_isMax (i : α) (n : ℕ) (hin : ¬IsMax (succ^[n - 1] i)) :
    pred^[n] (succ^[n] i) = i

Proof state:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hin : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (succ^[n] i) = i

Tactic:
induction' n with n hn

Result:
case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
hin : ¬IsMax (succ^[0 - 1] i)
⊢ pred^[0] (succ^[0] i) = i

case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n + 1 - 1] i)
⊢ pred^[n + 1] (succ^[n + 1] i) = i
-- Mathlib/CategoryTheory/EpiMono.lean
theorem SplitMono.mono {X Y : C} {f : X ⟶ Y} (sm : SplitMono f) : Mono f :=
  { right_cancellation := fun g h w => by replace w := w =≫ sm.retraction; simpa using w }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : (g ≫ f) ≫ sm.retraction = (h ≫ f) ≫ sm.retraction
⊢ g = h

Tactic:
simpa using w

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : g ≫ f = h ≫ f
⊢ g = h

Tactic:
replace w := w =≫ sm.retraction

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
sm : SplitMono f
Z✝ : C
g h : Z✝ ⟶ X
w : (g ≫ f) ≫ sm.retraction = (h ≫ f) ≫ sm.retraction
⊢ g = h
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasSubgroupToLpTrim_neg (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :
    lpMeasSubgroupToLpTrim F p μ hm (-f) = -lpMeasSubgroupToLpTrim F p μ hm f

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᶠ[ae (μ.trim hm)] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)

Tactic:
refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _).neg
  <| (lpMeasSubgroupToLpTrim_ae_eq hm _).trans <|
  ((Lp.coeFn_neg _).trans ?_).trans  (lpMeasSubgroupToLpTrim_ae_eq hm f).symm.neg

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ -↑↑↑f =ᶠ[ae μ] fun x => -↑↑↑f x

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ lpMeasSubgroupToLpTrim F p μ hm (-f) = -lpMeasSubgroupToLpTrim F p μ hm f

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᶠ[ae (μ.trim hm)] ↑↑(-lpMeasSubgroupToLpTrim F p μ hm f)

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ -↑↑↑f =ᶠ[ae μ] fun x => -↑↑↑f x

Tactic:
exact Eventually.of_forall fun x => by rfl

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᶠ[ae (μ.trim hm)] ↑↑(-lpMeasSubgroupToLpTrim F p μ hm f)

Tactic:
refine EventuallyEq.trans ?_ (Lp.coeFn_neg _).symm

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
⊢ ↑↑(lpMeasSubgroupToLpTrim F p μ hm (-f)) =ᶠ[ae (μ.trim hm)] -↑↑(lpMeasSubgroupToLpTrim F p μ hm f)

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(lpMeasSubgroup F m p μ)
x : α
⊢ (-↑↑↑f) x = (fun x => -↑↑↑f x) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/OpenSubgroup.lean
@[to_additive]
lemma discreteTopology [ContinuousMul G] (U : Subgroup G) (h : IsOpen (U : Set G)) :
    DiscreteTopology (G ⧸ U)

Proof state:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g : G
⊢ IsOpen {⟦g⟧}

Tactic:
show IsOpen (QuotientGroup.mk ⁻¹' {QuotientGroup.mk g})

Result:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g : G
⊢ IsOpen (QuotientGroup.mk ⁻¹' {↑g})

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
⊢ DiscreteTopology (G ⧸ U)

Tactic:
refine singletons_open_iff_discrete.mp (fun g ↦ ?_)

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g : G ⧸ U
⊢ IsOpen {g}

Proof state:
case h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g g' : G
⊢ (g'⁻¹ * g)⁻¹ ∈ U ↔ g⁻¹ * g' ∈ ↑U

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g : G
⊢ QuotientGroup.mk ⁻¹' {↑g} = (fun x => g * x) '' ↑U

Tactic:
ext g'

Result:
case h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g g' : G
⊢ g' ∈ QuotientGroup.mk ⁻¹' {↑g} ↔ g' ∈ (fun x => g * x) '' ↑U

Proof state:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g : G
⊢ IsOpen ((fun x => g * x) '' ↑U)

Tactic:
exact Homeomorph.mulLeft g |>.isOpen_image |>.mpr h

Result:
no goals

Proof state:
case h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g g' : G
⊢ g' ∈ QuotientGroup.mk ⁻¹' {↑g} ↔ g' ∈ (fun x => g * x) '' ↑U

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff, QuotientGroup.eq, Set.image_mul_left]

Result:
case h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g g' : G
⊢ g'⁻¹ * g ∈ U ↔ g⁻¹ * g' ∈ ↑U

Proof state:
case h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g g' : G
⊢ g'⁻¹ * g ∈ U ↔ g⁻¹ * g' ∈ ↑U

Tactic:
rw [← U.inv_mem_iff]

Result:
case h.e'_3.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
U : Subgroup G
h : IsOpen ↑U
g g' : G
⊢ (g'⁻¹ * g)⁻¹ ∈ U ↔ g⁻¹ * g' ∈ ↑U
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftProp_subtype_val {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q)
    (hQ : ∀ y, Q id univ y) (U : Opens M) :
    LiftProp Q (Subtype.val : U → M)

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q (id ∘ Subtype.val) x

Tactic:
rw [← hG.liftPropAt_iff_comp_subtype_val]

Result:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q id ↑x

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
⊢ LiftProp Q Subtype.val

Tactic:
intro x

Result:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q Subtype.val x

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q Subtype.val x

Tactic:
show LiftPropAt Q (id ∘ Subtype.val) x

Result:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q (id ∘ Subtype.val) x

Proof state:
H : Type u_1
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
G : StructureGroupoid H
Q : (H → H) → Set H → H → Prop
hG : G.LocalInvariantProp G Q
hQ : ∀ (y : H), Q id univ y
U : Opens M
x : ↥U
⊢ LiftPropAt Q id ↑x

Tactic:
apply hG.liftProp_id hQ

Result:
no goals