harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem supp_map (h : q.IsUniform) {α β : TypeVec n} (g : α ⟹ β) (x : F α) (i) :
    supp (g <$$> x) i = g i '' supp x i

Proof state:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ (g ⊚ f) i '' univ = g i ∘ f i '' univ

Tactic:
rfl

Result:
no goals

Proof state:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (g <$$> abs ⟨a, f⟩) i = g i '' supp (abs ⟨a, f⟩) i

Tactic:
rw [← abs_map, MvPFunctor.map_eq]

Result:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, g ⊚ f⟩) i = g i '' supp (abs ⟨a, f⟩) i

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i

Tactic:
obtain ⟨a, f⟩ := repr x

Result:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (g <$$> abs ⟨a, f⟩) i = g i '' supp (abs ⟨a, f⟩) i

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> x) i = g i '' supp x i

Tactic:
rw [← abs_repr x]

Result:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i

Proof state:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, g ⊚ f⟩) i = g i '' supp (abs ⟨a, f⟩) i

Tactic:
rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, ← image_comp]

Result:
case mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ (g ⊚ f) i '' univ = g i ∘ f i '' univ
-- Mathlib/Data/Set/Finite/Lattice.lean
/-- An indexed union of pairwise disjoint sets is finite iff all sets are finite, and all but
finitely many are empty. -/
lemma PairwiseDisjoint.finite_biUnion_iff {f : β → Set α} {s : Set β} (hs : s.PairwiseDisjoint f) :
    (⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i ∈ s | (f i).Nonempty}.Finite

Proof state:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (∀ (i : β), (⋃ (_ : i ∈ s), f i).Finite) ∧ {i | (⋃ (_ : i ∈ s), f i).Nonempty}.Finite ↔
    (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ Pairwise fun i j => Disjoint (⋃ (_ : i ∈ s), f i) (⋃ (_ : j ∈ s), f j)

Tactic:
aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise])

Result:
no goals

Proof state:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite

Tactic:
rw [finite_iUnion_iff (by aesop (add unfold safe [Pairwise, PairwiseDisjoint, Set.Pairwise]))]

Result:
α : Type u
β : Type v
f : β → Set α
s : Set β
hs : s.PairwiseDisjoint f
⊢ (∀ (i : β), (⋃ (_ : i ∈ s), f i).Finite) ∧ {i | (⋃ (_ : i ∈ s), f i).Nonempty}.Finite ↔
    (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem _root_.algebraMap_memℓp_infty (k : 𝕜) : Memℓp (algebraMap 𝕜 (∀ i, B i) k) ∞

Proof state:
𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst✝³ : NormedField 𝕜
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
k : 𝕜
⊢ Memℓp (k • 1) ⊤

Tactic:
exact (one_memℓp_infty.const_smul k : Memℓp (k • (1 : ∀ i, B i)) ∞)

Result:
no goals

Proof state:
𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst✝³ : NormedField 𝕜
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
k : 𝕜
⊢ Memℓp ((algebraMap 𝕜 ((i : I) → B i)) k) ⊤

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst✝³ : NormedField 𝕜
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
k : 𝕜
⊢ Memℓp (k • 1) ⊤
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma strictConcaveOn_qaryEntropy : StrictConcaveOn ℝ (Icc 0 1) (qaryEntropy q)

Proof state:
q : ℕ
p : ℝ
hp : p ∈ interior (Icc 0 1)
⊢ -1 / (p * (1 - p)) < 0

Tactic:
simp_all only [interior_Icc, mem_Ioo]

Result:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 / (p * (1 - p)) < 0

Proof state:
q : ℕ
⊢ StrictConcaveOn ℝ (Icc 0 1) (qaryEntropy q)

Tactic:
apply strictConcaveOn_of_deriv2_neg (convex_Icc 0 1) qaryEntropy_continuous.continuousOn

Result:
q : ℕ
⊢ ∀ x ∈ interior (Icc 0 1), deriv^[2] (qaryEntropy q) x < 0

Proof state:
case hb
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < p * (1 - p)

Tactic:
simp_all only [gt_iff_lt, mul_pos_iff_of_pos_left, sub_pos, hp]

Result:
no goals

Proof state:
case ha
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 < 0

Tactic:
norm_num [show 0 < log 2 by positivity]

Result:
no goals

Proof state:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < log 2

Tactic:
positivity

Result:
no goals

Proof state:
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 / (p * (1 - p)) < 0

Tactic:
apply div_neg_of_neg_of_pos

Result:
case ha
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ -1 < 0

case hb
q : ℕ
p : ℝ
hp : 0 < p ∧ p < 1
⊢ 0 < p * (1 - p)

Proof state:
q : ℕ
p : ℝ
hp : p ∈ interior (Icc 0 1)
⊢ deriv^[2] (qaryEntropy q) p < 0

Tactic:
rw [deriv2_qaryEntropy]

Result:
q : ℕ
p : ℝ
hp : p ∈ interior (Icc 0 1)
⊢ -1 / (p * (1 - p)) < 0

Proof state:
q : ℕ
⊢ ∀ x ∈ interior (Icc 0 1), deriv^[2] (qaryEntropy q) x < 0

Tactic:
intro p hp

Result:
q : ℕ
p : ℝ
hp : p ∈ interior (Icc 0 1)
⊢ deriv^[2] (qaryEntropy q) p < 0
-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
lemma toNerve₂.mk_naturality_δ1i (i : Fin 3) : toNerve₂.mk.naturalityProperty F (δ₂ i)

Proof state:
case h.«0».hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 1).op (X.map (δ 0).op x) = X.map (δ 0 ≫ δ 2).op x

Tactic:
simp only [← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
case h.«0».hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
⊢ X.map (δ 1 ≫ δ 0).op x = X.map (δ 0 ≫ δ 2).op x

Proof state:
case h.«0».hx
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
x : X.obj (op { obj := [1 + 1], property := ⋯ })
this : δ 0 ≫ δ 2 = δ 1 ≫ δ 0
⊢ X.map (δ 1 ≫ δ 0).op x = X.map (δ 0 ≫ δ 2).op x

Tactic:
exact congrFun (congrArg X.map (congrArg Quiver.Hom.op this.symm)) x

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem liftOn'_mk {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ p, f p 0 = f 0 1)
    (H : ∀ {p q a} (_hq : q ≠ 0) (_ha : a ≠ 0), f (a * p) (a * q) = f p q) :
    (RatFunc.mk p q).liftOn' f @H = f p q

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ (RatFunc.mk p q).liftOn' f H = f p q

Tactic:
rw [RatFunc.liftOn', RatFunc.liftOn_mk _ _ _ f0]

Result:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
P : Sort v
p q : K[X]
f : K[X] → K[X] → P
f0 : ∀ (p : K[X]), f p 0 = f 0 1
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
⊢ ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q'

Tactic:
apply liftOn_condition_of_liftOn'_condition H

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_swap_mul_ge_support_diff (f : Perm α) (x y : α) :
    f.support \ {x, y} ≤ (swap x y * f).support

Proof state:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
ha : f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : (swap x y) (f a✝) = a✝
⊢ False

Tactic:
rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H

Result:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
ha : f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : f a✝ = a✝
⊢ False

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
⊢ ¬f a✝ = a✝ → ¬(a✝ = x ∨ a✝ = y) → ¬(swap x y) (f a✝) = a✝

Tactic:
push_neg

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
⊢ f a✝ ≠ a✝ → a✝ ≠ x ∧ a✝ ≠ y → (swap x y) (f a✝) ≠ a✝

Proof state:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
ha : f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : f a✝ = a✝
⊢ False

Tactic:
exact ha H

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ f.support \ {x, y} ≤ (swap x y * f).support

Tactic:
intro

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
⊢ a✝ ∈ f.support \ {x, y} → a✝ ∈ (swap x y * f).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
⊢ a✝ ∈ f.support \ {x, y} → a✝ ∈ (swap x y * f).support

Tactic:
simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne, mem_support, mem_insert, mem_sdiff,
  mem_singleton]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
⊢ ¬f a✝ = a✝ → ¬(a✝ = x ∨ a✝ = y) → ¬(swap x y) (f a✝) = a✝

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
⊢ f a✝ ≠ a✝ → a✝ ≠ x ∧ a✝ ≠ y → (swap x y) (f a✝) ≠ a✝

Tactic:
rintro ha ⟨hx, hy⟩ H

Result:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y a✝ : α
ha : f a✝ ≠ a✝
hx : a✝ ≠ x
hy : a✝ ≠ y
H : (swap x y) (f a✝) = a✝
⊢ False
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma isCompl_genWeightSpaceOf_zero_posFittingCompOf (x : L) :
    IsCompl (genWeightSpaceOf M 0 x) (posFittingCompOf R M x)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieAlgebra R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : LieRingModule L M
inst✝³ : LieModule R L M
inst✝² : LieRing.IsNilpotent L
inst✝¹ : IsNoetherian R M
inst✝ : IsArtinian R M
x : L
⊢ IsCompl (genWeightSpaceOf M 0 x) (posFittingCompOf R M x)

Tactic:
simpa only [isCompl_iff, codisjoint_iff, disjoint_iff, ← LieSubmodule.toSubmodule_inj,
  LieSubmodule.sup_toSubmodule, LieSubmodule.inf_toSubmodule,
  LieSubmodule.top_toSubmodule, LieSubmodule.bot_toSubmodule, coe_genWeightSpaceOf_zero] using
  (toEnd R L M x).isCompl_iSup_ker_pow_iInf_range_pow

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.sin (o.oangle (x + y) y) * ‖x + y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).sin * ‖x + y‖ = ‖x‖

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).sin * ‖y + x‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).sin * ‖x + y‖ = ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).sin * ‖x + y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).sin * ‖y + x‖ = ‖x‖

Tactic:
exact (-o).sin_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem Nat.emultiplicity_pow_add_pow {x y : ℕ} (hxy : p ∣ x + y) (hx : ¬p ∣ x)
    {n : ℕ} (hn : Odd n) :
    emultiplicity p (x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n

Proof state:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
hxy : ↑p ∣ ↑x + ↑y
⊢ emultiplicity (↑p) (↑x ^ n + ↑y ^ n) = emultiplicity (↑p) (↑x + ↑y) + emultiplicity p n

Tactic:
exact Int.emultiplicity_pow_add_pow hp hp1 hxy hx hn

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity p (x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n

Tactic:
iterate 2 rw [← Int.natCast_emultiplicity]

Result:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity ↑p ↑(x ^ n + y ^ n) = emultiplicity ↑p ↑(x + y) + emultiplicity p n

Proof state:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity ↑p ↑(x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n

Tactic:
rw [← Int.natCast_emultiplicity]

Result:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity ↑p ↑(x ^ n + y ^ n) = emultiplicity ↑p ↑(x + y) + emultiplicity p n

Proof state:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity ↑p ↑(x ^ n + y ^ n) = emultiplicity ↑p ↑(x + y) + emultiplicity p n

Tactic:
rw [← Int.natCast_dvd_natCast] at hxy hx

Result:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x + y)
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
⊢ emultiplicity ↑p ↑(x ^ n + y ^ n) = emultiplicity ↑p ↑(x + y) + emultiplicity p n

Proof state:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : ↑p ∣ ↑(x + y)
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
⊢ emultiplicity ↑p ↑(x ^ n + y ^ n) = emultiplicity ↑p ↑(x + y) + emultiplicity p n

Tactic:
push_cast at *

Result:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hx : ¬↑p ∣ ↑x
n : ℕ
hn : Odd n
hxy : ↑p ∣ ↑x + ↑y
⊢ emultiplicity (↑p) (↑x ^ n + ↑y ^ n) = emultiplicity (↑p) (↑x + ↑y) + emultiplicity p n
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem mem_compl_zeroLocus_iff_not_mem {f : A} {I : ProjectiveSpectrum 𝒜} :
    I ∈ (zeroLocus 𝒜 {f} : Set (ProjectiveSpectrum 𝒜))ᶜ ↔ f ∉ I.asHomogeneousIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ I ∈ (zeroLocus 𝒜 {f})ᶜ ↔ f ∉ I.asHomogeneousIdeal

Tactic:
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ f ∉ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ f ∉ ↑I.asHomogeneousIdeal ↔ f ∉ I.asHomogeneousIdeal

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem sum_sum_index {α β M N P : Type*} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
    {f : SkewMonoidAlgebra M α} {g : α → M → SkewMonoidAlgebra N β} {h : β → N → P}
    (h_zero : ∀ (a : β), h a 0 = 0)
    (h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) :
    sum (sum f g) h = sum f fun a b ↦ sum (g a b) h

Proof state:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.sum g).sum h = f.sum fun a b => (g a b).sum h

Tactic:
rw [sum_def, toFinsupp_sum' f g, Finsupp.sum_sum_index h_zero h_add]

Result:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.toFinsupp.sum fun a b => (g a b).toFinsupp.sum h) = f.sum fun a b => (g a b).sum h

Proof state:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.toFinsupp.sum fun a b => (g a b).toFinsupp.sum h) = f.sum fun a b => (g a b).sum h

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
private lemma XYIdeal'_mul_inv {x y : F} (h : W.Nonsingular x y) :
    XYIdeal W x (C y) * (XYIdeal W x (C <| W.negY x y) *
        (XIdeal W x : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹) = 1

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ ↑(XYIdeal W x (C y)) * (↑(XYIdeal W x (C (W.negY x y))) * (↑(XIdeal W x))⁻¹) = 1

Tactic:
rw [← mul_assoc, ← FractionalIdeal.coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h,
  XIdeal, FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero W x]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Tower.lean
theorem restrictScalars_injective :
    Function.Injective (restrictScalars R : Subalgebra S A → Subalgebra R A) := fun U V H ↦
  ext fun x ↦ by rw [← mem_restrictScalars R, H, mem_restrictScalars]

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ U ↔ x ∈ V

Tactic:
rw [← mem_restrictScalars R, H, mem_restrictScalars]

Result:
no goals
-- Mathlib/Algebra/Order/Quantale.lean
theorem rightMulResiduation_le_iff_mul_le : x ≤ y ⇨ᵣ z ↔ y * x ≤ z where
  mp h1

Proof state:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * (y ⇨ᵣ z) ≤ z

Tactic:
simp_all only [rightMulResiduation, mul_sSup_distrib, Set.mem_setOf_eq,
  iSup_le_iff, implies_true]

Result:
no goals

Proof state:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * x ≤ z

Tactic:
apply le_trans (mul_le_mul_left' h1 _)

Result:
α : Type u_1
x y z : α
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
h1 : x ≤ y ⇨ᵣ z
⊢ y * (y ⇨ᵣ z) ≤ z
-- Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
lemma projectiveFamilyContent_ne_top [∀ J, IsFiniteMeasure (P J)]
    (hP : IsProjectiveMeasureFamily P) :
    projectiveFamilyContent hP s ≠ ∞

Proof state:
case pos
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
inst✝ : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
⊢ (P (measurableCylinders.finset hs)) (measurableCylinders.set hs) ≠ ⊤

Tactic:
exact measure_ne_top _ _

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
inst✝ : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily P
hs : s ∉ measurableCylinders α
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
inst✝ : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily P
⊢ (projectiveFamilyContent hP) s ≠ ⊤

Tactic:
rw [projectiveFamilyContent_eq hP, projectiveFamilyFun]

Result:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
inst✝ : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily P
⊢ (if hs : s ∈ measurableCylinders α then (P (measurableCylinders.finset hs)) (measurableCylinders.set hs) else 0) ≠ ⊤

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
inst✝ : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily P
⊢ (if hs : s ∈ measurableCylinders α then (P (measurableCylinders.finset hs)) (measurableCylinders.set hs) else 0) ≠ ⊤

Tactic:
split_ifs with hs

Result:
case pos
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
inst✝ : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily P
hs : s ∈ measurableCylinders α
⊢ (P (measurableCylinders.finset hs)) (measurableCylinders.set hs) ≠ ⊤

case neg
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
s : Set ((i : ι) → α i)
inst✝ : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily P
hs : s ∉ measurableCylinders α
⊢ 0 ≠ ⊤
-- Mathlib/Data/Setoid/Basic.lean
theorem sInf_def {s : Set (Setoid α)} : ⇑(sInf s) = sInf ((⇑) '' s)

Proof state:
case h.h.a
α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ sInf (@r α '' s) x✝¹ x✝

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Result:
case h.h.a
α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ ∀ i ∈ s, i x✝¹ x✝

Proof state:
α : Type u_1
s : Set (Setoid α)
⊢ ⇑(sInf s) = sInf (@r α '' s)

Tactic:
ext

Result:
case h.h.a
α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ sInf (@r α '' s) x✝¹ x✝

Proof state:
case h.h.a
α : Type u_1
s : Set (Setoid α)
x✝¹ x✝ : α
⊢ (sInf s) x✝¹ x✝ ↔ ∀ i ∈ s, i x✝¹ x✝

Tactic:
rfl

Result:
no goals