harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_map_eq_pow_single [DecidableEq ι] (i : ι)
    (hf : ∀ i' ≠ i, i' ∈ m → f i' = 1) : (m.map f).prod = f i ^ m.count i

Proof state:
ι : Type u_2
α : Type u_3
inst✝¹ : CommMonoid α
m : Multiset ι
f : ι → α
inst✝ : DecidableEq ι
i : ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1
⊢ (map f m).prod = f i ^ count i m

Tactic:
induction m using Quotient.inductionOn

Result:
case h
ι : Type u_2
α : Type u_3
inst✝¹ : CommMonoid α
m : Multiset ι
f : ι → α
inst✝ : DecidableEq ι
i : ι
a✝ : List ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦a✝⟧ → f i' = 1
⊢ (map f ⟦a✝⟧).prod = f i ^ count i ⟦a✝⟧

Proof state:
case h
ι : Type u_2
α : Type u_3
inst✝¹ : CommMonoid α
m : Multiset ι
f : ι → α
inst✝ : DecidableEq ι
i : ι
a✝ : List ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦a✝⟧ → f i' = 1
⊢ (map f ⟦a✝⟧).prod = f i ^ count i ⟦a✝⟧

Tactic:
simp [List.prod_map_eq_pow_single i f hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c)

Proof state:
a b c : Int
⊢ a + (b + c) = b + (a + c)

Tactic:
rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_comp_eq {g : β → γ} : image (g ∘ f) = image g ∘ image f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ image (g ∘ f) = image g ∘ image f

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
x✝¹ : Set α
x✝ : γ
⊢ x✝ ∈ g ∘ f '' x✝¹ ↔ x✝ ∈ (image g ∘ image f) x✝¹

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
x✝¹ : Set α
x✝ : γ
⊢ x✝ ∈ g ∘ f '' x✝¹ ↔ x✝ ∈ (image g ∘ image f) x✝¹

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem Equiv.Perm.decomposeFin.symm_sign {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
    Perm.sign (Equiv.Perm.decomposeFin.symm (p, e)) = ite (p = 0) 1 (-1) * Perm.sign e

Proof state:
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ sign (decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * sign e

Tactic:
refine Fin.cases ?_ ?_ p <;> simp [Equiv.Perm.decomposeFin, Fin.succ_ne_zero]

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condExpKernel [NormedSpace ℝ F]
    (hf : AEStronglyMeasurable f μ) :
    AEStronglyMeasurable (fun ω => ∫ y, f y ∂condExpKernel μ m ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condDistrib id id μ) (id ω)) μ

Tactic:
exact AEStronglyMeasurable.integral_condDistrib
  (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
  (hf.comp_snd_map_prod_id inf_le_right)

Result:
no goals

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condExpKernel μ m) ω) μ

Tactic:
simp_rw [condExpKernel_apply_eq_condDistrib]

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
⊢ AEStronglyMeasurable (fun ω => ∫ (y : Ω), f y ∂(condDistrib id id μ) (id ω)) μ
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_factorial_mul_add {n : ℕ} (m : ℕ) [hp : Fact p.Prime] (h : n < p) :
    padicValNat p (p * m + n) ! = padicValNat p (p * m) !

Proof state:
case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + (n + 1))! = padicValNat p (p * m)!

Tactic:
rw [add_succ, factorial_succ,
  padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
  hn <| lt_of_succ_lt h, ← add_succ,
  padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
    (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
  zero_add]

Result:
no goals

Proof state:
p n m : ℕ
hp : Fact (Nat.Prime p)
h : n < p
⊢ padicValNat p (p * m + n)! = padicValNat p (p * m)!

Tactic:
induction n with
| zero => rw [add_zero]
| succ n hn =>
  rw [add_succ, factorial_succ,
    padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),
    hn <| lt_of_succ_lt h, ← add_succ,
    padicValNat_eq_zero_of_mem_Ioo ⟨(Nat.lt_add_of_pos_right <| succ_pos n),
      (Nat.mul_add _ _ _▸ Nat.mul_one _ ▸ ((add_lt_add_iff_left (p * m)).mpr h))⟩,
    zero_add]

Result:
no goals

Proof state:
case zero
p m : ℕ
hp : Fact (Nat.Prime p)
h : 0 < p
⊢ padicValNat p (p * m + 0)! = padicValNat p (p * m)!

Tactic:
rw [add_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem neg_v_mul_e0 (m : M) : -(v Q m * e0 Q) = e0 Q * v Q m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (v Q) m * e0 Q = -(e0 Q * (v Q) m)

Tactic:
exact (neg_e0_mul_v _ m).symm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ -((v Q) m * e0 Q) = e0 Q * (v Q) m

Tactic:
rw [neg_eq_iff_eq_neg]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (v Q) m * e0 Q = -(e0 Q * (v Q) m)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_comp_neg (hf : ContinuousOn f ((- ·) '' (spectrum R (a : A)))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁰ : CommRing R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : ContinuousStar R
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra R A
inst✝¹ : ContinuousFunctionalCalculus R p
f : R → R
a : A
inst✝ : UniqueHom R A
hf : autoParam (ContinuousOn f ((fun x => -x) '' spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfc (fun x => f (-x)) a = cfc f (-a)

Tactic:
rw [cfc_comp' .., cfc_neg_id _]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_strictMono : StrictMono ((↑) : ℚ → K) := fun p q => by
  simpa only [sub_pos, cast_sub] using cast_pos_of_pos (K := K) (q := q - p)

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
p q : ℚ
⊢ p < q → ↑p < ↑q

Tactic:
simpa only [sub_pos, cast_sub] using cast_pos_of_pos (K := K) (q := q - p)

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma tendsto_eulerMascheroniSeq :
    Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Proof state:
case refine_1

⊢ BddAbove (Set.range eulerMascheroniSeq)

Tactic:
exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩

Result:
no goals

Proof state:
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
have := tendsto_atTop_ciSup strictMono_eulerMascheroniSeq.monotone ?_

Result:
case refine_2
this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ i, eulerMascheroniSeq i))
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

case refine_1

⊢ BddAbove (Set.range eulerMascheroniSeq)

Proof state:
case refine_2
this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ i, eulerMascheroniSeq i))
⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
rwa [eulerMascheroniConstant, this.limUnder_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_matrix'' (m n : Type u) [Finite m] [Finite n] :
    Module.rank R (Matrix m n R) = #m * #n

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m n : Type u
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = #m * #n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
@[simp, norm_cast] lemma nonZeroDivisors.associated_coe : Associated (a : M₀) b ↔ Associated a b :=
  unitsNonZeroDivisorsEquiv.symm.exists_congr_left.trans <| by simp [Associated]; norm_cast

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑(unitsNonZeroDivisorsEquiv.symm.symm b_1) = ↑b) ↔ Associated a b

Tactic:
simp [Associated]

Result:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑↑b_1 = ↑b) ↔ ∃ u, a * ↑u = b

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : ↥M₀⁰
⊢ (∃ b_1, ↑a * ↑↑b_1 = ↑b) ↔ ∃ u, a * ↑u = b

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_mapIdx (f : Nat → α → β) (a : Vector α n) :
    (a.mapIdx f).toList = a.toList.mapIdx f

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : Nat → α → β
a : Vector α n
⊢ (mapIdx f a).toList = List.mapIdx f a.toList

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_C_mul_X_sq (a : R) : derivative (C a * X ^ 2) = C (a * 2) * X

Proof state:
R : Type u
inst✝ : Semiring R
a : R
⊢ derivative (C a * X ^ 2) = C (a * 2) * X

Tactic:
rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem tendsto_lift {m : γ → β} {l : Filter γ} :
    Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Tendsto m l (g s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Tendsto m l (g s)

Tactic:
simp only [Filter.lift, tendsto_iInf]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isCoatom_iff [OrderTop A] {K : A} :
    IsCoatom K ↔ K ≠ ⊤ ∧ ∀ H g, K ≤ H → g ∉ K → g ∈ H → H = ⊤

Proof state:
A : Type u_4
B : Type u_5
inst✝¹ : SetLike A B
inst✝ : OrderTop A
K : A
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

Tactic:
simp_rw [IsCoatom, lt_iff_le_not_le, SetLike.not_le_iff_exists,
  and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem MonotoneOn.intervalIntegrable {u : ℝ → E} {a b : ℝ} (hu : MonotoneOn u (uIcc a b)) :
    IntervalIntegrable u μ a b

Proof state:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
μ : Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntegrableOn u (Ι a b) μ

Tactic:
exact (hu.integrableOn_isCompact isCompact_uIcc).mono_set Ioc_subset_Icc_self

Result:
no goals

Proof state:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
μ : Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntervalIntegrable u μ a b

Tactic:
rw [intervalIntegrable_iff]

Result:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
μ : Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntegrableOn u (Ι a b) μ
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ball_half_subset (y) (h : y ∈ ball x (ε / 2)) : ball y (ε / 2) ⊆ ball x ε :=
  ball_subset <| by rw [sub_self_div_two]; exact le_of_lt h

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε - ε / 2

Tactic:
rw [sub_self_div_two]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2

Tactic:
exact le_of_lt h

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_abs : cos |x| = cos x

Proof state:
x : ℝ
⊢ cos |x| = cos x

Tactic:
cases le_total x 0 <;> simp only [*, abs_of_nonneg, abs_of_nonpos, cos_neg]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem le_iff_compact_le_imp {a b : α} :
    a ≤ b ↔ ∀ c : α, CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b :=
  ⟨fun ab _ _ ca => le_trans ca ab, fun h => by
    rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]
    exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩⟩

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ a} ≤ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ b}

Tactic:
exact sSup_le_sSup fun c hc => ⟨hc.1, h c hc.1 hc.2⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b
⊢ a ≤ b

Tactic:
rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b
⊢ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ a} ≤ sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ b}
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem cos_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖

Tactic:
rw [sub_eq_add_neg, cos_angle_add_of_inner_eq_zero h]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem GroupWithZero.mul_left_injective (h : x ≠ 0) :
    Function.Injective fun y => y * x := fun y y' w => by
  simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
x : G₀
h : x ≠ 0
y y' : G₀
w : (fun y => y * x) y = (fun y => y * x) y'
⊢ y = y'

Tactic:
simpa only [mul_assoc, mul_inv_cancel₀ h, mul_one] using congr_arg (fun y => y * x⁻¹) w

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp]
lemma decreasingInduction_self {n} {motive : (m : ℕ) → m ≤ n → Sort*} (of_succ self) :
    (decreasingInduction (motive := motive) of_succ self (Nat.le_refl _)) = self

Proof state:
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction of_succ self ⋯ = self

Tactic:
dsimp only [decreasingInduction]

Result:
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ leRec (motive := fun {n_1} mn =>
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    self

Proof state:
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ leRec (motive := fun {n_1} mn =>
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    self

Tactic:
rw [leRec_self]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem trans_source (e f : Pretrivialization F proj) :
    (f.toPartialEquiv.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ univ

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e f : Pretrivialization F proj
⊢ (f.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ univ

Tactic:
rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommFold_coe (l : List α) (comm) (a : α) :
    noncommFold op (l : Multiset α) comm a = l.foldr op a

Proof state:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y => op x y = op y x
a : α
⊢ noncommFold op (↑l) comm a = List.foldr op a l

Tactic:
simp [noncommFold]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem cancel_right_of_respectsIso
    (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso]
    {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] [IsAffine Z] [IsAffine Y] :
    P (f ≫ g) ↔ P f

Proof state:
P : AffineTargetMorphismProperty
inst✝³ : P.toProperty.RespectsIso
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : IsIso g
inst✝¹ : IsAffine Z
inst✝ : IsAffine Y
⊢ P (f ≫ g) ↔ P f

Tactic:
rw [← P.toProperty_apply, ← P.toProperty_apply,
P.toProperty.cancel_right_of_respectsIso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_map (f : α → β) (g : β → Vector γ k) (l : Vector α n) :
     (map f l).flatMap g = l.flatMap (fun a => g (f a))

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
k : Nat
f : α → β
g : β → Vector γ k
l : Array α
⊢ (map f { toArray := l, size_toArray := ⋯ }).flatMap g = { toArray := l, size_toArray := ⋯ }.flatMap fun a => g (f a)

Tactic:
simp [Array.flatMap_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
k n : Nat
f : α → β
g : β → Vector γ k
l : Vector α n
⊢ (map f l).flatMap g = l.flatMap fun a => g (f a)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
k : Nat
f : α → β
g : β → Vector γ k
l : Array α
⊢ (map f { toArray := l, size_toArray := ⋯ }).flatMap g = { toArray := l, size_toArray := ⋯ }.flatMap fun a => g (f a)
-- Mathlib/Data/Set/Image.lean
theorem range_eq_iff (f : α → β) (s : Set β) :
    range f = s ↔ (∀ a, f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b

Tactic:
rw [← range_subset_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f = s ↔ range f ⊆ s ∧ ∀ b ∈ s, ∃ a, f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f = s ↔ range f ⊆ s ∧ ∀ b ∈ s, ∃ a, f a = b

Tactic:
exact le_antisymm_iff

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem map_eq (f : Char → Char) (s) : map f s = ⟨s.1.map f⟩

Proof state:
f : Char → Char
s : String
⊢ map f s = { data := List.map f s.data }

Tactic:
simpa using mapAux_of_valid f [] s.1

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalHom.lean
theorem mk_coe (f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) : (⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) = f

Proof state:
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
⊢ { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive Even.nsmul_right] lemma IsSquare.pow (n : ℕ) : IsSquare a → IsSquare (a ^ n)

Proof state:
case intro
α : Type u_2
inst✝ : Monoid α
n : ℕ
r : α
⊢ IsSquare ((r * r) ^ n)

Tactic:
exact ⟨r ^ n, (Commute.refl _).mul_pow _⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Monoid α
a : α
n : ℕ
⊢ IsSquare a → IsSquare (a ^ n)

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
α : Type u_2
inst✝ : Monoid α
n : ℕ
r : α
⊢ IsSquare ((r * r) ^ n)
-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
lemma extendScalarsId_hom_app_one_tmul (M : ModuleCat R) (m : M) :
    (extendScalarsId R).hom.app M ((1 : R) ⊗ₜ m) = m

Proof state:
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).hom.app M)) (1 ⊗ₜ[R] m) = m

Tactic:
rw [← extendRestrictScalarsAdj_homEquiv_apply,
  homEquiv_extendScalarsId]

Result:
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((restrictScalarsId R).inv.app M)) m = m

Proof state:
R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((restrictScalarsId R).inv.app M)) m = m

Tactic:
dsimp

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
theorem le_normalizer : N ≤ N.normalizer

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
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
N : LieSubmodule R L M
⊢ N ≤ N.normalizer

Tactic:
intro m hm

Result:
R : Type u_1
L : Type u_2
M : Type u_3
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
N : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ m ∈ N.normalizer

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
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
N : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ m ∈ N.normalizer

Tactic:
rw [mem_normalizer]

Result:
R : Type u_1
L : Type u_2
M : Type u_3
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
N : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
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
N : LieSubmodule R L M
m : M
hm : m ∈ N
⊢ ∀ (x : L), ⁅x, m⁆ ∈ N

Tactic:
exact fun x => N.lie_mem hm

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma map_le_iff (f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
    x.map f ≤ y.map f ↔ x ≤ y

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : WithBot α
f : α → β
mono_iff : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
⊢ map f x ≤ map f y ↔ x ≤ y

Tactic:
cases x <;> cases y <;> simp [mono_iff]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_re (x y : ℤ) : ((⟨x, y⟩ : ℤ[i]) : ℂ).re = x

Proof state:
x y : ℤ
⊢ (toComplex { re := x, im := y }).re = ↑x

Tactic:
simp [toComplex_def]

Result:
no goals