harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_zipWith {f : ∀ i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i}
    {g₂ : Π₀ i, β₂ i} : (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Proof state:
ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → Zero (β i)
inst✝⁴ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Tactic:
simp [zipWith_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_div_sub_norm_div_le_norm_div (u v w : E) : ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v w : E
⊢ ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

Tactic:
simpa only [div_div_div_cancel_right] using norm_sub_norm_le' (u / w) (v / w)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_left_of_neg (x y : V) {r : ℝ} (hr : r < 0) :
    o.oangle (r • x) y = o.oangle (-x) y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r < 0
⊢ o.oangle (r • x) y = o.oangle (-x) y

Tactic:
rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_left_of_pos _ _ (neg_pos_of_neg hr)]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Adjunction.lean
@[simp]
lemma adjunction_counit_app_val [HasWeakSheafify J D] [HasSheafCompose J F] (adj : G ⊣ F)
    (Y : Sheaf J D) : ((adjunction J adj).counit.app Y).val =
      sheafifyLift J (((adj.whiskerRight Cᵒᵖ).counit.app Y.val)) Y.cond

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
Y : Sheaf J D
⊢ ((adjunction J adj).counit.app Y).val = sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.val) ⋯

Tactic:
change ((𝟭 (Sheaf _ _)).map ((adjunction J adj).counit.app Y)).val = _

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
Y : Sheaf J D
⊢ ((𝟭 (Sheaf J D)).map ((adjunction J adj).counit.app Y)).val =
    sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.val) ⋯

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{u_2, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
Y : Sheaf J D
⊢ ((𝟭 (Sheaf J D)).map ((adjunction J adj).counit.app Y)).val =
    sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.val) ⋯

Tactic:
simp only [Functor.comp_obj, sheafToPresheaf_obj, sheafCompose_obj_val, whiskeringRight_obj_obj,
  adjunction, Adjunction.map_restrictFullyFaithful_counit_app, Iso.refl_inv, NatTrans.id_app,
  Functor.comp_map, whiskeringRight_obj_map, Adjunction.comp_counit_app,
  instCategorySheaf_comp_val, instCategorySheaf_id_val, sheafificationAdjunction_counit_app_val,
  sheafifyMap_sheafifyLift, Functor.id_obj, whiskerRight_id', Category.comp_id, Category.id_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem map_preimage (f : α →ₛ β) (g : β → γ) (s : Set γ) :
    f.map g ⁻¹' s = f ⁻¹' ↑{b ∈ f.range | g b ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ ⇑(map g f) ⁻¹' s = ⇑f ⁻¹' ↑(Finset.filter (fun b => g b ∈ s) f.range)

Tactic:
simp only [coe_range, sep_mem_eq, coe_map, Finset.coe_filter,
  ← mem_preimage, inter_comm, preimage_inter_range, ← Finset.mem_coe]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ g ∘ ⇑f ⁻¹' s = ⇑f ⁻¹' (g ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : MeasurableSpace α
f : α →ₛ β
g : β → γ
s : Set γ
⊢ g ∘ ⇑f ⁻¹' s = ⇑f ⁻¹' (g ⁻¹' s)

Tactic:
exact preimage_comp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_sub_uIcc : (fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ Icc (a - b ⊔ c) (a - b ⊓ c) = Icc ((a - b) ⊓ (a - c)) ((a - b) ⊔ (a - c))

Tactic:
simp only [sub_eq_add_neg, min_add_add_left, max_add_add_left, min_neg_neg, max_neg_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' [[b, c]] = [[a - b, a - c]]

Tactic:
simp_rw [← Icc_min_max, preimage_const_sub_Icc]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ Icc (a - b ⊔ c) (a - b ⊓ c) = Icc ((a - b) ⊓ (a - c)) ((a - b) ⊔ (a - c))
-- Mathlib/Algebra/Divisibility/Basic.lean
lemma pow_dvd_pow (a : α) (h : m ≤ n) : a ^ m ∣ a ^ n :=
  ⟨a ^ (n - m), by rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]⟩

Proof state:
α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ m * a ^ (n - m)

Tactic:
rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.unsat_le_lo (u v k : Nat) : isLt 0 k = true → u ≤ v → v + k ≤ u → False

Proof state:
u v k : Nat
⊢ isLt 0 k = true → u ≤ v → v + k ≤ u → False

Tactic:
simp [isLt]

Result:
u v k : Nat
⊢ 0 < k → u ≤ v → u < v + k

Proof state:
u v k : Nat
⊢ 0 < k → u ≤ v → u < v + k

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
@[simp]
lemma algebraMap_comp_intCast (R A : Type*) [CommRing R] [Ring A] [Algebra R A] :
    algebraMap R A ∘ Int.cast = Int.cast

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x✝ : ℤ
⊢ (⇑(algebraMap R A) ∘ Int.cast) x✝ = ↑x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ ⇑(algebraMap R A) ∘ Int.cast = Int.cast

Tactic:
ext

Result:
case h
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x✝ : ℤ
⊢ (⇑(algebraMap R A) ∘ Int.cast) x✝ = ↑x✝
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_mul_intCast (x : ℝ≥0∞) (y : ℝ) (n : ℤ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x : ℝ≥0∞
y : ℝ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_intCast]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem sum_filter_pairs_eq_sum_powersetCard_sum (k : ℕ)
    (f : Finset σ × σ → MvPolynomial σ R) :
    ∑ t ∈ pairs σ k with #t.1 = k, f t = ∑ A ∈ powersetCard k univ, ∑ j ∈ A, f (A, j)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∑ t ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k), f t =
    ∑ A ∈ powersetCard k univ, ∑ j ∈ A, f (A, j)

Tactic:
apply sum_finset_product

Result:
case h
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ (p : Finset σ × σ),
    p ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k) ↔ p.1 ∈ powersetCard k univ ∧ p.2 ∈ p.1

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ (p : Finset σ × σ),
    p ∈ filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k) ↔ p.1 ∈ powersetCard k univ ∧ p.2 ∈ p.1

Tactic:
aesop

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_le_image_iff (f : X ⟶ Y) [IsOpenImmersion f] (U U' : X.Opens) :
    f ''ᵁ U ≤ f ''ᵁ U' ↔ U ≤ U'

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'

Tactic:
apply preimage_le_preimage_of_le f h

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
⊢ f ''ᵁ U ≤ f ''ᵁ U' ↔ U ≤ U'

Tactic:
refine ⟨fun h ↦ ?_, image_le_image_of_le f⟩

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ U ≤ U'

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ U ≤ U'

Tactic:
rw [← preimage_image_eq f U, ← preimage_image_eq f U']

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'
-- Mathlib/Order/Filter/Prod.lean
theorem map_pure_prod (f : α → β → γ) (a : α) (B : Filter β) :
    map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B

Tactic:
rw [Filter.pure_prod]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_left_monotone (a : Ordinal) : Monotone (veblenWith f · a)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ a

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ Monotone fun x => veblenWith f x a

Tactic:
rw [monotone_iff_forall_lt]

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ ∀ ⦃a_1 b : Ordinal.{u}⦄, a_1 < b → veblenWith f a_1 a ≤ veblenWith f b a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)

Tactic:
exact (veblenWith_right_strictMono hf o₁).monotone (right_le_veblenWith hf o₂ a)

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a : Ordinal.{u}
⊢ ∀ ⦃a_1 b : Ordinal.{u}⦄, a_1 < b → veblenWith f a_1 a ≤ veblenWith f b a

Tactic:
intro o₁ o₂ h

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ a
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_iff_exact_coimage_π :
    S.Exact ↔ (ShortComplex.mk S.f (Abelian.coimage.π S.g)
      (Abelian.comp_coimage_π_eq_zero S.zero)).Exact

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ (mk S.f (Abelian.coimage.π S.g) ⋯).Exact

Tactic:
symm

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (mk S.f (Abelian.coimage.π S.g) ⋯).Exact ↔ S.Exact

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (mk S.f (Abelian.coimage.π S.g) ⋯).Exact ↔ S.Exact

Tactic:
exact ShortComplex.exact_iff_of_epi_of_isIso_of_mono
  { τ₁ := 𝟙 _
    τ₂ := 𝟙 _
    τ₃ := Abelian.factorThruCoimage S.g }

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem detAux_def' (b : Basis ι A M) (f : M →ₗ[A] M) :
    LinearMap.detAux (Trunc.mk b) f = Matrix.det (LinearMap.toMatrix b b f)

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ (detAux (Trunc.mk b)) f = ((toMatrix b b) f).det

Tactic:
rw [detAux]

Result:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ (Trunc.lift (fun b => detMonoidHom.comp ↑(toMatrixAlgEquiv b)) ⋯ (Trunc.mk b)) f = ((toMatrix b b) f).det

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ (Trunc.lift (fun b => detMonoidHom.comp ↑(toMatrixAlgEquiv b)) ⋯ (Trunc.mk b)) f = ((toMatrix b b) f).det

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem mem_iSup_iff_exists_dfinsupp' (p : ι → Submodule R N) [∀ (i) (x : p i), Decidable (x ≠ 0)]
    (x : N) : x ∈ iSup p ↔ ∃ f : Π₀ i, p i, (f.sum fun _ xi => ↑xi) = x

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, ((lsum ℕ) fun i => (p i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi => ↑xi) = x

Tactic:
simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
  LinearMap.toAddMonoidHom_coe, coe_subtype]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ x ∈ iSup p ↔ ∃ f, (f.sum fun x xi => ↑xi) = x

Tactic:
rw [mem_iSup_iff_exists_dfinsupp]

Result:
ι : Type u_1
R : Type u_2
N : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, ((lsum ℕ) fun i => (p i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi => ↑xi) = x
-- Mathlib/RingTheory/Int/Basic.lean
theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two {m : ℤ} {p : ℕ} (hp : Nat.Prime p)
    (h : (p : ℤ) ∣ 2 * m ^ 2) : p = 2 ∨ p ∣ Int.natAbs m

Proof state:
case inl.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2

Tactic:
exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)

Result:
no goals

Proof state:
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ m.natAbs * m.natAbs
⊢ p ∣ m.natAbs

Tactic:
exact or_self_iff.mp ((Nat.Prime.dvd_mul hp).mp hpp)

Result:
no goals

Proof state:
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
apply Or.intro_right

Result:
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p ∣ m.natAbs

Proof state:
case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
apply Or.intro_left

Result:
case inl.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2

Proof state:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
⊢ p = 2 ∨ p ∣ m.natAbs

Tactic:
rcases Int.Prime.dvd_mul hp h with hp2 | hpp

Result:
case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ m.natAbs

case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs

Proof state:
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ (m ^ 2).natAbs
⊢ p ∣ m.natAbs

Tactic:
rw [sq, Int.natAbs_mul] at hpp

Result:
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ m.natAbs * m.natAbs
⊢ p ∣ m.natAbs
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem frobenius_zmodp (x : 𝕎 (ZMod p)) : frobenius x = x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ frobenius x = x

Tactic:
simp only [WittVector.ext_iff, coeff_frobenius_charP, ZMod.pow_card, eq_self_iff_true,
  forall_const]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Filter.Eventually.intCast_atTop [StrictOrderedRing R] [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atTop, p x) : ∀ᶠ (n : ℤ) in atTop, p n

Proof state:
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in atTop, p ↑n

Tactic:
rw [← Int.comap_cast_atTop (R := R)]

Result:
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n

Proof state:
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n

Tactic:
exact h.comap _

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
theorem support_tsub {f1 f2 : ι →₀ α} : (f1 - f2).support ⊆ f1.support

Proof state:
ι : Type u_1
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f1 f2 : ι →₀ α
⊢ (f1 - f2).support ⊆ f1.support

Tactic:
simp +contextual only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff,
  Ne, coe_tsub, Pi.sub_apply, not_imp_not, zero_le, imp_true_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
theorem isFiniteMeasure_toFiniteAux [SFinite μ] : IsFiniteMeasure μ.toFiniteAux

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : ¬IsFiniteMeasure μ
⊢ IsFiniteMeasure ⋯.choose

Tactic:
exact (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec.1

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : IsFiniteMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure (if IsFiniteMeasure μ then μ else ⋯.choose)

Tactic:
split_ifs

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : IsFiniteMeasure μ
⊢ IsFiniteMeasure μ

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
h✝ : ¬IsFiniteMeasure μ
⊢ IsFiniteMeasure ⋯.choose

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure μ.toFiniteAux

Tactic:
rw [Measure.toFiniteAux]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ IsFiniteMeasure (if IsFiniteMeasure μ then μ else ⋯.choose)
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma orthogonal_eq_top_iff (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) :
    B.orthogonal W = ⊤ ↔ W = ⊥

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : W = ⊥
⊢ B.orthogonal W = ⊤

Tactic:
simp [h]

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ B.orthogonal W = ⊤ ↔ W = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : B.orthogonal W = ⊤
⊢ W = ⊥

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : B.orthogonal W = ⊤
this : W ⊓ B.orthogonal W = ⊥
⊢ W = ⊥

Tactic:
rwa [h, inf_top_eq] at this

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : B.orthogonal W = ⊤
⊢ W = ⊥

Tactic:
have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).inf_eq_bot

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : B.orthogonal W = ⊤
this : W ⊓ B.orthogonal W = ⊥
⊢ W = ⊥
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_two_power (a : Cardinal) : lift.{v} (2 ^ a) = 2 ^ lift.{v} a

Proof state:
a : Cardinal.{u_1}
⊢ lift.{v, u_1} (2 ^ a) = 2 ^ lift.{v, u_1} a

Tactic:
simp [← one_add_one_eq_two]

Result:
no goals
-- Mathlib/Data/Sigma/Order.lean
theorem le_def [∀ i, LE (α i)] {a b : Σi, α i} : a ≤ b ↔ ∃ h : a.1 = b.1, h.rec a.2 ≤ b.2

Proof state:
case mpr.mk.mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : ⋯ ▸ ⟨i, a⟩.snd ≤ ⟨i, b⟩.snd
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩

Tactic:
exact le.fiber _ _ _ h

Result:
no goals

Proof state:
case mp.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ h, h ▸ ⟨i, a⟩.snd ≤ ⟨i, b⟩.snd

Tactic:
exact ⟨rfl, h⟩

Result:
no goals

Proof state:
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ ⟨i, a⟩.snd ≤ ⟨j, b⟩.snd) → ⟨i, a⟩ ≤ ⟨j, b⟩

Tactic:
rintro ⟨rfl : i = j, h⟩

Result:
case mpr.mk.mk.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : ⋯ ▸ ⟨i, a⟩.snd ≤ ⟨i, b⟩.snd
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩

Proof state:
case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b

Tactic:
obtain ⟨i, a⟩ := a

Result:
case mpr.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ ⟨i, a⟩.snd ≤ b.snd) → ⟨i, a⟩ ≤ b

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b ↔ ∃ h, h ▸ a.snd ≤ b.snd

Tactic:
constructor

Result:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd

case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b

Proof state:
case mpr.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
b : (i : ι) × α i
i : ι
a : α i
⊢ (∃ h, h ▸ ⟨i, a⟩.snd ≤ b.snd) → ⟨i, a⟩ ≤ b

Tactic:
obtain ⟨j, b⟩ := b

Result:
case mpr.mk.mk
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a : α i
j : ι
b : α j
⊢ (∃ h, h ▸ ⟨i, a⟩.snd ≤ ⟨j, b⟩.snd) → ⟨i, a⟩ ≤ ⟨j, b⟩

Proof state:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ a ≤ b → ∃ h, h ▸ a.snd ≤ b.snd

Tactic:
rintro ⟨i, a, b, h⟩

Result:
case mp.fiber
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
i : ι
a b : α i
h : a ≤ b
⊢ ∃ h, h ▸ ⟨i, a⟩.snd ≤ ⟨i, b⟩.snd
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem join_map_map {f : α → β} (hf : Measurable f) (μ : Measure (Measure α)) :
    join (map (map f) μ) = map f (join μ)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ (map (map f) μ).join s = (map f μ.join) s

Tactic:
rw [join_apply hs, map_apply hf hs, join_apply (hf hs),
  lintegral_map (measurable_coe hs) (measurable_map f hf)]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), (map f a) s ∂μ = ∫⁻ (μ : Measure α), μ (f ⁻¹' s) ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
⊢ (map (map f) μ).join = map f μ.join

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ (map (map f) μ).join s = (map f μ.join) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), (map f a) s ∂μ = ∫⁻ (μ : Measure α), μ (f ⁻¹' s) ∂μ

Tactic:
simp_rw [map_apply hf hs]

Result:
no goals