harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/FixedPointFree.lean
theorem prod_pow_eq_one (hφ : FixedPointFree φ) {n : ℕ} (hn : φ^[n] = _root_.id) (g : G) :
    ((List.range n).map (fun k ↦ φ^[k] g)).prod = 1

Proof state:
case intro
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ (List.map (fun k => (⇑φ)^[k] (commutatorMap (⇑φ) g)) (List.range n)).prod = 1

Tactic:
simp only [commutatorMap_apply, iterate_map_div, ← Function.iterate_succ_apply]

Result:
case intro
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ (List.map (fun k => (⇑φ)^[k] g / (⇑φ)^[k.succ] g) (List.range n)).prod = 1

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ (List.map (fun k => (⇑φ)^[k] g) (List.range n)).prod = 1

Tactic:
obtain ⟨g, rfl⟩ := commutatorMap_surjective hφ g

Result:
case intro
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ (List.map (fun k => (⇑φ)^[k] (commutatorMap (⇑φ) g)) (List.range n)).prod = 1

Proof state:
case intro
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ (List.map (fun k => (⇑φ)^[k] g / (⇑φ)^[k.succ] g) (List.range n)).prod = 1

Tactic:
rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.preimage_add_left (hs : StarConvex 𝕜 (x + z) s) :
    StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (x + z) s
⊢ StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)

Tactic:
rw [add_comm] at hs

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
⊢ StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
⊢ StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)

Tactic:
simpa only [add_comm] using hs.preimage_add_right

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem nonneg_iff [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
    0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s)

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ 0 ≤ x ↔ x ∈ AddSubmonoid.closure (range fun s => star s * s)

Tactic:
simp only [le_iff, zero_add, exists_eq_right']

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem nontrivial_of_hasRankNullity : Nontrivial R

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : HasRankNullity.{u, u_1} R
H : Subsingleton R
⊢ False

Tactic:
have := rank_quotient_add_rank (R := R) (M := PUnit) ⊥

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : HasRankNullity.{u, u_1} R
H : Subsingleton R
this : Module.rank R (PUnit.{u + 1} ⧸ ⊥) + Module.rank R ↥⊥ = Module.rank R PUnit.{u + 1}
⊢ False

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : HasRankNullity.{u, u_1} R
H : Subsingleton R
this : Module.rank R (PUnit.{u + 1} ⧸ ⊥) + Module.rank R ↥⊥ = Module.rank R PUnit.{u + 1}
⊢ False

Tactic:
simp [one_add_one_eq_two] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : HasRankNullity.{u, u_1} R
⊢ Nontrivial R

Tactic:
refine (subsingleton_or_nontrivial R).resolve_left fun H ↦ ?_

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : HasRankNullity.{u, u_1} R
H : Subsingleton R
⊢ False
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem LinearIsometry.inner_map_map (f : E →ₗᵢ[𝕜] E') (x y : E) : ⟪f x, f y⟫ = ⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
x y : E
⊢ ⟪f x, f y⟫_𝕜 = ⟪x, y⟫_𝕜

Tactic:
simp [inner_eq_sum_norm_sq_div_four, ← f.norm_map]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem eval_whiskerLeft
    {f : a ⟶ b} {g h : b ⟶ c}
    {η η' : g ⟶ h} {θ : f ≫ g ⟶ f ≫ h}
    (e_η : η = η') (e_θ : f ◁ η' = θ) :
    f ◁ η = θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η η' : g ⟶ h
θ : f ≫ g ⟶ f ≫ h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
simp [e_η, e_θ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lex_empty
    [BEq α] {lt : α → α → Bool} (l₁ : Vector α 0) : l₁.lex #v[] lt = false

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 0
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.lex { toArray := #[], size_toArray := ⋯ } lt = false

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
l₁ : Vector α 0
⊢ l₁.lex { toArray := #[], size_toArray := ⋯ } lt = false

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 0
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.lex { toArray := #[], size_toArray := ⋯ } lt = false
-- Mathlib/Data/Matrix/Invertible.lean
theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
    A * ⅟ B * B = A

Proof state:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * ⅟B * B = A

Tactic:
rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma polyCharpoly_coeff_eval (x : L) (i : ℕ) :
    MvPolynomial.eval (b.repr x) ((polyCharpoly φ b).coeff i) = (φ x).charpoly.coeff i

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
i : ℕ
⊢ (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpoly b).coeff i) = (charpoly (φ x)).coeff i

Tactic:
rw [polyCharpoly, polyCharpolyAux_coeff_eval]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_sub_left (x y z : F) : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ ⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜

Tactic:
simp [sub_eq_add_neg, inner_add_left, inner_neg_left]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem compl_union_self (s : Set α) : sᶜ ∪ s = univ

Proof state:
α : Type u
s : Set α
⊢ sᶜ ∪ s = univ

Tactic:
rw [union_comm, union_compl_self]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_left_cancel {x y} {c : S} (h : f.toMap (x * c) = f.toMap (y * c)) :
    f.toMap x = f.toMap y :=
  f.map_right_cancel (c := c) <| by rw [mul_comm _ x, mul_comm _ y, h]

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f.toMap (x * ↑c) = f.toMap (y * ↑c)
⊢ f.toMap (↑c * x) = f.toMap (↑c * y)

Tactic:
rw [mul_comm _ x, mul_comm _ y, h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean
theorem not_IntegrableOn_Ioi_inv {a : ℝ} :
    ¬ IntegrableOn (·⁻¹) (Ioi a)

Proof state:
a : ℝ
⊢ ¬IntegrableOn (fun x => x⁻¹) (Ioi a) volume

Tactic:
simpa only [IntegrableOn, restrict_Ioi_eq_restrict_Ici] using not_IntegrableOn_Ici_inv

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem cylinder_empty (s : Finset ι) : cylinder s (∅ : Set (∀ i : s, α i)) = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
⊢ cylinder s ∅ = ∅

Tactic:
rw [cylinder, preimage_empty]

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
lemma fwdDiff_iter_choose (j k : ℕ) :
    Δ_[1]^[k] (fun x ↦ x.choose (k + j) : ℕ → ℤ) = fun x ↦ x.choose j

Proof state:
case succ
k : ℕ
IH : ∀ (j : ℕ), (Δ_[1]^[k] fun x => ↑(x.choose (k + j))) = fun x => ↑(x.choose j)
j : ℕ
⊢ (Δ_[1]^[k + 1] fun x => ↑(x.choose (k + 1 + j))) = fun x => ↑(x.choose j)

Tactic:
simp only [Function.iterate_succ_apply', add_assoc, add_comm 1 j, IH, fwdDiff_choose]

Result:
no goals

Proof state:
j k : ℕ
⊢ (Δ_[1]^[k] fun x => ↑(x.choose (k + j))) = fun x => ↑(x.choose j)

Tactic:
induction' k with k IH generalizing j

Result:
case zero
j : ℕ
⊢ (Δ_[1]^[0] fun x => ↑(x.choose (0 + j))) = fun x => ↑(x.choose j)

case succ
k : ℕ
IH : ∀ (j : ℕ), (Δ_[1]^[k] fun x => ↑(x.choose (k + j))) = fun x => ↑(x.choose j)
j : ℕ
⊢ (Δ_[1]^[k + 1] fun x => ↑(x.choose (k + 1 + j))) = fun x => ↑(x.choose j)

Proof state:
case zero
j : ℕ
⊢ (Δ_[1]^[0] fun x => ↑(x.choose (0 + j))) = fun x => ↑(x.choose j)

Tactic:
simp only [zero_add, iterate_zero, id_eq]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_eq_natCast [DecidableEq n] [Semiring α] [StarRing α]
    {M : Matrix n n α} {d : ℕ} :
    Mᴴ = d ↔ M = d :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [conjTranspose_natCast]

Proof state:
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Semiring α
inst✝ : StarRing α
M : Matrix n n α
d : ℕ
⊢ M = (↑d)ᴴ ↔ M = ↑d

Tactic:
rw [conjTranspose_natCast]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_two : lift.{u, v} 2 = 2

Proof state:
⊢ lift.{u, v} 2 = 2

Tactic:
simp [← one_add_one_eq_two]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_one_iff_isSquare {a : F} (ha : a ≠ 0) :
    quadraticChar F a = 1 ↔ IsSquare a

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ (quadraticChar F) a = 1 ↔ IsSquare a

Tactic:
simp only [quadraticChar_apply, quadraticCharFun, ha, if_false, ite_eq_left_iff,
  (by omega : (-1 : ℤ) ≠ 1), imp_false, not_not, reduceCtorEq]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ -1 ≠ 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/DirectSum/Decomposition.lean
theorem decompose_of_mem_same {x : M} {i : ι} (hx : x ∈ ℳ i) : (decompose ℳ x i : M) = x

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i : ι
hx : x ∈ ℳ i
⊢ ↑(((decompose ℳ) x) i) = x

Tactic:
rw [decompose_of_mem _ hx, DirectSum.of_eq_same, Subtype.coe_mk]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
@[simp]
lemma card_Ico : #(Ico a b) = b - a

Proof state:
n : ℕ
a b : Fin n
⊢ #(Ico a b) = ↑b - ↑a

Tactic:
rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem coe_direction_eq_vsub_set_left {s : AffineSubspace k P} {p : P} (hp : p ∈ s) :
    (s.direction : Set V) = (p -ᵥ ·) '' s

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ (∃ x ∈ ↑s, x -ᵥ p = -v) ↔ ∃ x ∈ ↑s, p -ᵥ x = v

Tactic:
conv_lhs =>
  congr
  ext
  rw [← neg_vsub_eq_vsub_rev, neg_inj]

Result:
no goals

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ ↑s.direction ↔ v ∈ (fun x => p -ᵥ x) '' ↑s

Tactic:
rw [SetLike.mem_coe, ← Submodule.neg_mem_iff, ← SetLike.mem_coe,
  coe_direction_eq_vsub_set_right hp, Set.mem_image, Set.mem_image]

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ (∃ x ∈ ↑s, x -ᵥ p = -v) ↔ ∃ x ∈ ↑s, p -ᵥ x = v

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s.direction = (fun x => p -ᵥ x) '' ↑s

Tactic:
ext v

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ ↑s.direction ↔ v ∈ (fun x => p -ᵥ x) '' ↑s
-- Mathlib/Order/SymmDiff.lean
theorem himp_bihimp : a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)

Tactic:
rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem option_isSome : Primrec (@Option.isSome α) :=
  (option_casesOn .id (const false) (const true).to₂).of_eq fun o => by cases o <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
o : Option α
⊢ (Option.casesOn (id o) false fun b => true) = o.isSome

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonpos_iff : a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff, neg_nonneg, neg_nonpos]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer preservation of colimits along a natural isomorphism in the shape. -/
lemma preservesColimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂)
    [PreservesColimit K₁ F] :
    PreservesColimit K₂ F where
  preserves {c} t := ⟨by
    apply IsColimit.precomposeHomEquiv (isoWhiskerRight h F :) _ _
    have := (IsColimit.precomposeHomEquiv h c).symm t
    apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
    exact Cocones.ext (Iso.refl _)⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))

Tactic:
have := (IsColimit.precomposeHomEquiv h c).symm t

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocones.precompose h.hom).obj c)
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocones.precompose h.hom).obj c)
⊢ F.mapCocone ((Cocones.precompose h.hom).obj c) ≅ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c)

Tactic:
exact Cocones.ext (Iso.refl _)

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
apply IsColimit.precomposeHomEquiv (isoWhiskerRight h F :) _ _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocones.precompose h.hom).obj c)
⊢ IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c))

Tactic:
apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocones.precompose h.hom).obj c)
⊢ F.mapCocone ((Cocones.precompose h.hom).obj c) ≅ (Cocones.precompose (isoWhiskerRight h F).hom).obj (F.mapCocone c)
-- Mathlib/Algebra/Group/Center.lean
theorem right_comm (h : IsMulCentral c) (a b) : a * b * c = a * c * b

Proof state:
M : Type u_1
c : M
inst✝ : Mul M
h : IsMulCentral c
a b : M
⊢ a * b * c = a * c * b

Tactic:
simp only [h.right_assoc, h.mid_assoc, h.comm]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma map_prod_eq (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
    {f : β → δ} (hf : Measurable f) : (κ.map f) ×ₖ η = (κ ×ₖ η).map (Prod.map f id)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
f : β → δ
hf : Measurable f
⊢ κ.map f ×ₖ η = (κ ×ₖ η).map (Prod.map f id)

Tactic:
rw [← map_prod_map _ _ hf measurable_id, map_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Equation.map {P : Fin 3 → R} (h : W'.Equation P) :
    (W'.map f).toJacobian.Equation (f ∘ P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ f ((eval P) W'.polynomial) = f 0

Tactic:
exact congr_arg f h

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ (WeierstrassCurve.map W' f).toJacobian.Equation (⇑f ∘ P)

Tactic:
rw [Equation, map_polynomial, eval_map, ← eval₂_comp, ← map_zero f]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
h : W'.Equation P
⊢ f ((eval P) W'.polynomial) = f 0
-- Mathlib/Order/Filter/Defs.lean
theorem mem_top {s : Set α} : s ∈ (⊤ : Filter α) ↔ s = univ

Proof state:
α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ s = univ

Tactic:
rw [mem_top_iff_forall, eq_univ_iff_forall]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_const_smul (w : ι → k) (p : ι → P) (b : P) (c : k) :
    s.weightedVSubOfPoint p b (c • w) = c • s.weightedVSubOfPoint p b w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
c : k
⊢ (s.weightedVSubOfPoint p b) (c • w) = c • (s.weightedVSubOfPoint p b) w

Tactic:
simp_rw [weightedVSubOfPoint_apply, smul_sum, Pi.smul_apply, smul_smul, smul_eq_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_sub (f g : N →ₗ[R] P) : (f - g).rTensor M = f.rTensor M - g.rTensor M

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ (rTensorHom M) (f - g) = (rTensorHom M) f - (rTensorHom M) g

Tactic:
exact (rTensorHom (R := R) (N := N) (P := P) M).map_sub f g

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ rTensor M (f - g) = rTensor M f - rTensor M g

Tactic:
simp only [← coe_rTensorHom]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
⊢ (rTensorHom M) (f - g) = (rTensorHom M) f - (rTensorHom M) g
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_eq_zero_iff (s : ℂ) : Gamma s = 0 ↔ ∃ m : ℕ, s = -m

Proof state:
case mpr.intro
m : ℕ
⊢ Gamma (-↑m) = 0

Tactic:
exact Gamma_neg_nat_eq_zero m

Result:
no goals

Proof state:
s : ℂ
⊢ Gamma s = 0 ↔ ∃ m, s = -↑m

Tactic:
constructor

Result:
case mp
s : ℂ
⊢ Gamma s = 0 → ∃ m, s = -↑m

case mpr
s : ℂ
⊢ (∃ m, s = -↑m) → Gamma s = 0

Proof state:
case mp
s : ℂ
⊢ Gamma s = 0 → ∃ m, s = -↑m

Tactic:
contrapose!

Result:
case mp
s : ℂ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0

Proof state:
case mp
s : ℂ
⊢ (∀ (m : ℕ), s ≠ -↑m) → Gamma s ≠ 0

Tactic:
exact Gamma_ne_zero

Result:
no goals

Proof state:
case mpr
s : ℂ
⊢ (∃ m, s = -↑m) → Gamma s = 0

Tactic:
rintro ⟨m, rfl⟩

Result:
case mpr.intro
m : ℕ
⊢ Gamma (-↑m) = 0
-- Mathlib/Algebra/Order/Ring/WithTop.lean
@[simp] lemma top_mul (hb : b ≠ 0) : ⊤ * b = ⊤

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ ⊤ * b = ⊤

Tactic:
rw [top_mul', if_neg hb]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem hasSum_norm (hp : 0 < p.toReal) (f : lp E p) :
    HasSum (fun i => ‖f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i => ‖↑f i‖ ^ p.toReal) (∑' (i : α), ‖↑f i‖ ^ p.toReal)

Tactic:
exact ((lp.memℓp f).summable hp).hasSum

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
rw [norm_rpow_eq_tsum hp]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i => ‖↑f i‖ ^ p.toReal) (∑' (i : α), ‖↑f i‖ ^ p.toReal)
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sizeUpTo_zero : c.sizeUpTo 0 = 0

Proof state:
n : ℕ
c : Composition n
⊢ c.sizeUpTo 0 = 0

Tactic:
simp [sizeUpTo]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem sum_map_singleton (s : Multiset α) : (s.map fun a => ({a} : Multiset α)).sum = s :=
  Multiset.induction_on s (by simp) (by simp)

Proof state:
α : Type u_3
s : Multiset α
⊢ (map (fun a => {a}) 0).sum = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
s : Multiset α
⊢ ∀ (a : α) (s : Multiset α), (map (fun a => {a}) s).sum = s → (map (fun a => {a}) (a ::ₘ s)).sum = a ::ₘ s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma isIso_iCycles : IsIso (K.iCycles i)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst✝ : K.HasHomology i
⊢ IsIso (K.iCycles i)

Tactic:
subst hj

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
h : K.d i (c.next i) = 0
⊢ IsIso (K.iCycles i)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
h : K.d i (c.next i) = 0
⊢ IsIso (K.iCycles i)

Tactic:
exact ShortComplex.isIso_iCycles _ h

Result:
no goals