harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
theorem HigherFacesVanish.inclusionOfMooreComplexMap (n : ℕ) :
    HigherFacesVanish (n + 1) ((inclusionOfMooreComplexMap X).f (n + 1)) := fun j _ => by
  dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
  rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp only [Finset.mem_univ])), assoc, kernelSubobject_arrow_comp, comp_zero]

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ j ∈ Finset.univ

Tactic:
simp only [Finset.mem_univ]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (AlgebraicTopology.inclusionOfMooreComplexMap X).f (n + 1) ≫ X.δ j.succ = 0

Tactic:
dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]

Result:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ j.succ = 0

Proof state:
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ j.succ = 0

Tactic:
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
  (by simp only [Finset.mem_univ])), assoc, kernelSubobject_arrow_comp, comp_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_zero_left [HasKernels V] [HasZeroObject V] {w} :
    imageToKernel (0 : A ⟶ B) g w = 0

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w = 0

Tactic:
ext

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w ≫ (kernelSubobject g).arrow = 0 ≫ (kernelSubobject g).arrow

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w ≫ (kernelSubobject g).arrow = 0 ≫ (kernelSubobject g).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubring R} : (↑(⨅ i, S i) : Set R) = ⋂ i, S i

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
S : ι → NonUnitalSubring R
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem lmap_injective : Function.Injective (lmap f) ↔ ∀ i, Function.Injective (f i)

Proof state:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M i →ₗ[R] N i
⊢ Function.Injective ⇑(lmap f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)

Tactic:
classical exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M i →ₗ[R] N i
⊢ Function.Injective ⇑(lmap f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)

Tactic:
exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
lemma isLoop_iff_closure_eq_loops (he : e ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
e : α
he : autoParam (e ∈ M.E) _auto✝
⊢ M.IsLoop e ↔ M.closure {e} = M.loops

Tactic:
rw [isLoop_iff_closure_eq_loops_and_mem_ground, and_iff_left he]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem ModelWithCorners.range_prod : range (I.prod J) = range I ×ˢ range J

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹ : TopologicalSpace H
G : Type u_7
inst✝ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ range ↑(I.prod J) = range ↑I ×ˢ range ↑J

Tactic:
simp_rw [← ModelWithCorners.target_eq]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹ : TopologicalSpace H
G : Type u_7
inst✝ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ (I.prod J).target = I.target ×ˢ J.target

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
H : Type u_5
inst✝¹ : TopologicalSpace H
G : Type u_7
inst✝ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ (I.prod J).target = I.target ×ˢ J.target

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem fst_map_fst : (Submodule.fst R M M₂).map (LinearMap.fst R M M₂) = ⊤

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
⊢ x ∈ map (LinearMap.fst R M M₂) (fst R M M₂)

Tactic:
simp only [fst, comap_bot, mem_map, mem_ker, snd_apply, fst_apply,
  Prod.exists, exists_eq_left, exists_eq]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ map (LinearMap.fst R M M₂) (fst R M M₂) = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ map (LinearMap.fst R M M₂) (fst R M M₂)

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ map (LinearMap.fst R M M₂) (fst R M M₂)

Tactic:
rintro x -

Result:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
⊢ x ∈ map (LinearMap.fst R M M₂) (fst R M M₂)
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.pair_iffₛ {R} [CommSemiring R] {x y : R} :
    CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1

Proof state:
R : Type u_4
inst✝ : CommSemiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1

Tactic:
rw [pair_iff'ₛ, and_left_comm, and_iff_right_of_imp]

Result:
R : Type u_4
inst✝ : CommSemiring R
x y : R
⊢ x * y = 0 ∧ x + y = 1 → y * x = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_filter_le (p : α → Bool) (l : List α) :
    (l.filter p).length ≤ l.length

Proof state:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
⊢ (if p a = true then a :: filter p l else filter p l).length ≤ l.length + 1

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
h✝ : p a = true
⊢ (a :: filter p l).length ≤ l.length + 1

case cons.isFalse
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
h✝ : ¬p a = true
⊢ (filter p l).length ≤ l.length + 1

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ (filter p []).length ≤ [].length

Tactic:
simp

Result:
no goals

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
h✝ : p a = true
⊢ (a :: filter p l).length ≤ l.length + 1

Tactic:
simp only [length_cons, succ_eq_add_one]

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
h✝ : p a = true
⊢ (filter p l).length + 1 ≤ l.length + 1

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
h✝ : p a = true
⊢ (filter p l).length + 1 ≤ l.length + 1

Tactic:
exact Nat.succ_le_succ ih

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
h✝ : ¬p a = true
⊢ (filter p l).length ≤ l.length + 1

Tactic:
exact Nat.le_trans ih (Nat.le_add_right _ _)

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
⊢ (filter p (a :: l)).length ≤ (a :: l).length

Tactic:
simp only [filter_cons, length_cons, succ_eq_add_one]

Result:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : (filter p l).length ≤ l.length
⊢ (if p a = true then a :: filter p l else filter p l).length ≤ l.length + 1
-- Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean
theorem nums_recurrence {gp : Pair K} {ppredA predA : K}
    (succ_nth_s_eq : g.s.get? (n + 1) = some gp) (nth_num_eq : g.nums n = ppredA)
    (succ_nth_num_eq : g.nums (n + 1) = predA) :
    g.nums (n + 2) = gp.b * predA + gp.a * ppredA

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_num_eq : g.nums n = ppredA
succ_nth_num_eq : g.nums (n + 1) = predA
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredA

Tactic:
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.a = ppredA :=
  exists_conts_a_of_num nth_num_eq

Result:
case intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_num_eq : g.nums (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredConts.a

Proof state:
case intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_num_eq : g.nums (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredConts.a

Tactic:
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
    ∃ conts, g.conts (n + 1) = conts ∧ conts.a = predA :=
  exists_conts_a_of_num succ_nth_num_eq

Result:
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_num_eq : g.nums (n + 1) = predConts.a
⊢ g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a

Proof state:
case intro.intro.refl.intro.intro.refl
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_num_eq : g.nums (n + 1) = predConts.a
⊢ g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a

Tactic:
rw [num_eq_conts_a, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_iff_norm [SeminormedAddCommGroup E] {l : Filter ι} {f : ι → α → E}
    {g : α → E} :
    TendstoInMeasure μ f l g ↔
      ∀ ε, 0 < ε → Tendsto (fun i => μ { x | ε ≤ ‖f i x - g x‖ }) l (𝓝 0)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔ ∀ (ε : ℝ), 0 < ε → Tendsto (fun i => μ {x | ε ≤ ‖f i x - g x‖}) l (𝓝 0)

Tactic:
simp_rw [TendstoInMeasure, dist_eq_norm]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Algebra.lean
theorem Subalgebra.separatesPoints_monotone :
    Monotone fun s : Subalgebra R C(α, A) => s.SeparatesPoints := fun s s' r h x y n => by
  obtain ⟨f, m, w⟩ := h n
  rcases m with ⟨f, ⟨m, rfl⟩⟩
  exact ⟨_, ⟨f, ⟨r m, rfl⟩⟩, w⟩

Proof state:
case intro.intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => s.SeparatesPoints) s
x y : α
n : x ≠ y
f : α → A
m : f ∈ (fun f => ⇑f) '' ↑s
w : f x ≠ f y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑s', f x ≠ f y

Tactic:
rcases m with ⟨f, ⟨m, rfl⟩⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => s.SeparatesPoints) s
x y : α
n : x ≠ y
f : C(α, A)
m : f ∈ ↑s
w : (fun f => ⇑f) f x ≠ (fun f => ⇑f) f y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑s', f x ≠ f y

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => s.SeparatesPoints) s
x y : α
n : x ≠ y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑s', f x ≠ f y

Tactic:
obtain ⟨f, m, w⟩ := h n

Result:
case intro.intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => s.SeparatesPoints) s
x y : α
n : x ≠ y
f : α → A
m : f ∈ (fun f => ⇑f) '' ↑s
w : f x ≠ f y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑s', f x ≠ f y

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝⁵ : TopologicalSpace α
R : Type u_2
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsTopologicalSemiring A
s s' : Subalgebra R C(α, A)
r : s ≤ s'
h : (fun s => s.SeparatesPoints) s
x y : α
n : x ≠ y
f : C(α, A)
m : f ∈ ↑s
w : (fun f => ⇑f) f x ≠ (fun f => ⇑f) f y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑s', f x ≠ f y

Tactic:
exact ⟨_, ⟨f, ⟨r m, rfl⟩⟩, w⟩

Result:
no goals
-- Mathlib/Order/Filter/ENNReal.lean
theorem limsup_liminf_le_liminf_limsup {β} [Countable β] {f : Filter α} [CountableInterFilter f]
    {g : Filter β} (u : α → β → ℝ≥0∞) :
    (f.limsup fun a : α => g.liminf fun b : β => u a b) ≤
      g.liminf fun b => f.limsup fun a => u a b :=
  have h1 : ∀ᶠ a in f, ∀ b, u a b ≤ f.limsup fun a' => u a' b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun a' => u a' i) f

Tactic:
exact fun b => ENNReal.eventually_le_limsup fun a => u a b

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ᶠ (a : α) in f, ∀ (b : β), u a b ≤ limsup (fun a' => u a' b) f

Tactic:
rw [eventually_countable_forall]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Countable β
f : Filter α
inst✝ : CountableInterFilter f
g : Filter β
u : α → β → ℝ≥0∞
⊢ ∀ (i : β), ∀ᶠ (x : α) in f, u x i ≤ limsup (fun a' => u a' i) f
-- Mathlib/Data/Nat/Bitwise.lean
theorem xor_mod_two_eq {m n : ℕ} : (m ^^^ n) % 2 = (m + n) % 2

Proof state:
case neg
m n : ℕ
h : (m + n) % 2 = 1
⊢ ¬(m % 2 = 1 ↔ n % 2 = 1)

Tactic:
omega

Result:
no goals

Proof state:
case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ m % 2 = 1 ↔ n % 2 = 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
simp only [h, mod_two_eq_zero_iff_testBit_zero, testBit_zero, xor_mod_two_eq_one, decide_not,
  Bool.decide_iff_dist, Bool.not_eq_false', beq_iff_eq, decide_eq_decide]

Result:
case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ m % 2 = 1 ↔ n % 2 = 1

Proof state:
case neg
m n : ℕ
h : (m + n) % 2 = 1
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
simp only [h, xor_mod_two_eq_one]

Result:
case neg
m n : ℕ
h : (m + n) % 2 = 1
⊢ ¬(m % 2 = 1 ↔ n % 2 = 1)

Proof state:
case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
simp only [mod_two_ne_zero] at h

Result:
case neg
m n : ℕ
h : (m + n) % 2 = 1
⊢ (m ^^^ n) % 2 = (m + n) % 2

Proof state:
m n : ℕ
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
by_cases h : (m + n) % 2 = 0

Result:
case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem oadd_lt_oadd_3 {e n a₁ a₂} (h : a₁ < a₂) : oadd e n a₁ < oadd e n a₂

Proof state:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ (e.oadd n a₁).repr < (e.oadd n a₂).repr

Tactic:
unfold repr

Result:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ ω ^ e.repr * ↑↑n + a₁.repr < ω ^ e.repr * ↑↑n + a₂.repr

Proof state:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ ω ^ e.repr * ↑↑n + a₁.repr < ω ^ e.repr * ↑↑n + a₂.repr

Tactic:
exact @add_lt_add_left _ _ _ _ (repr a₁) _ h _

Result:
no goals

Proof state:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ e.oadd n a₁ < e.oadd n a₂

Tactic:
rw [lt_def]

Result:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ (e.oadd n a₁).repr < (e.oadd n a₂).repr
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrixAlgEquiv'_apply (f : (n → R) →ₗ[R] n → R) (i j) :
    LinearMap.toMatrixAlgEquiv' f i j = f (fun j' ↦ if j' = j then 1 else 0) i

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] n → R
i j : n
⊢ toMatrixAlgEquiv' f i j = f (fun j' => if j' = j then 1 else 0) i

Tactic:
simp [LinearMap.toMatrixAlgEquiv']

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_negY (P : Fin 3 → A) :
    (W'.baseChange B).toProjective.negY (f ∘ P) = f ((W'.baseChange A).toProjective.negY P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.negY (⇑f ∘ P) = f ((baseChange W' A).toProjective.negY P)

Tactic:
rw [← RingHom.coe_coe, ← map_negY, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
  suffices n + m - (0 + m) = n by rw [Nat.zero_add] at this; assumption
  by rw [Nat.add_sub_add_right, Nat.sub_zero]

Proof state:
n m : Nat
this : n + m - m = n
⊢ n + m - m = n

Tactic:
assumption

Result:
no goals

Proof state:
n m : Nat
⊢ n + m - (0 + m) = n

Tactic:
rw [Nat.add_sub_add_right, Nat.sub_zero]

Result:
no goals

Proof state:
n m : Nat
this : n + m - (0 + m) = n
⊢ n + m - m = n

Tactic:
rw [Nat.zero_add] at this

Result:
n m : Nat
this : n + m - m = n
⊢ n + m - m = n
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem tensor_add {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z) : f ⊗ (g + h) = f ⊗ g + f ⊗ h

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : W ⟶ X
g h : Y ⟶ Z
⊢ f ⊗ (g + h) = f ⊗ g + f ⊗ h

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem IsPreconnected.constant_of_mapsTo {S : Set α} (hS : IsPreconnected S)
    {β} [TopologicalSpace β] {T : Set β} [DiscreteTopology T] {f : α → β} (hc : ContinuousOn f S)
    (hTm : MapsTo f S T) {x y : α} (hx : x ∈ S) (hy : y ∈ S) : f x = f y

Proof state:
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ F ⟨x, hx⟩ = F ⟨y, hy⟩

Tactic:
exact (isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.restrict_mapsTo _)

Result:
no goals

Proof state:
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
⊢ f x = f y

Tactic:
let F : S → T := hTm.restrict f S T

Result:
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ f x = f y

Proof state:
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
this : F ⟨x, hx⟩ = F ⟨y, hy⟩
⊢ f x = f y

Tactic:
rwa [← Subtype.coe_inj] at this

Result:
no goals

Proof state:
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ f x = f y

Tactic:
suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this

Result:
α : Type u
inst✝² : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝¹ : TopologicalSpace β
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ F ⟨x, hx⟩ = F ⟨y, hy⟩
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem Nat.Prime.sq_add_sq {p : ℕ} [Fact p.Prime] (hp : p % 4 ≠ 3) :
    ∃ a b : ℕ, a ^ 2 + b ^ 2 = p

Proof state:
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ∃ a b, a ^ 2 + b ^ 2 = p

Tactic:
apply sq_add_sq_of_nat_prime_of_not_irreducible p

Result:
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬Irreducible ↑p

Proof state:
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬Irreducible ↑p

Tactic:
rwa [_root_.irreducible_iff_prime, prime_iff_mod_four_eq_three_of_nat_prime p]

Result:
no goals