harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem continuous_setToFun (hT : DominatedFinMeasAdditive μ T C) :
    Continuous fun f : α →₁[μ] E => setToFun μ T hT f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ Continuous fun f => setToFun μ T hT ↑↑f

Tactic:
simp_rw [L1.setToFun_eq_setToL1 hT]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ Continuous fun f => (L1.setToL1 hT) f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ Continuous fun f => (L1.setToL1 hT) f

Tactic:
exact ContinuousLinearMap.continuous _

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem IsSymm.zpow {A : M} (h : A.IsSymm) (k : ℤ) :
    (A ^ k).IsSymm

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : A.IsSymm
k : ℤ
⊢ (A ^ k).IsSymm

Tactic:
rw [IsSymm, transpose_zpow, h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma natDegree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : p.natDegree ≤ q.natDegree

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ p.natDegree + q.natDegree

Tactic:
exact Nat.le_add_right _ _

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
⊢ p.natDegree ≤ q.natDegree

Tactic:
obtain ⟨q, rfl⟩ := h1

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree

Tactic:
rw [mul_ne_zero_iff] at h2

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ (p * q).natDegree

Tactic:
rw [natDegree_mul h2.1 h2.2]

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ p.natDegree + q.natDegree
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_flatten {p : α → Prop} {l : Array (Array { x // p x })} :
    l.flatten.unattach = (l.map unattach).flatten

Proof state:
α : Type u_1
p : α → Prop
l : Array (Array { x // p x })
⊢ l.flatten.unattach = (map unattach l).flatten

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : Array (Array { x // p x })
⊢ map (fun x => x.val) l.flatten = (map (fun l => map (fun x => x.val) l) l).flatten

Proof state:
α : Type u_1
p : α → Prop
l : Array (Array { x // p x })
⊢ map (fun x => x.val) l.flatten = (map (fun l => map (fun x => x.val) l) l).flatten

Tactic:
cases l using array₂_induction

Result:
case of
α : Type u_1
p : α → Prop
xss✝ : List (List { x // p x })
⊢ map (fun x => x.val) (List.map List.toArray xss✝).toArray.flatten =
    (map (fun l => map (fun x => x.val) l) (List.map List.toArray xss✝).toArray).flatten

Proof state:
case of
α : Type u_1
p : α → Prop
xss✝ : List (List { x // p x })
⊢ (List.map (List.map fun x => x.val) xss✝).flatten = (List.map (fun x => x.unattach) xss✝).flatten

Tactic:
simp only [List.unattach]

Result:
no goals

Proof state:
case of
α : Type u_1
p : α → Prop
xss✝ : List (List { x // p x })
⊢ map (fun x => x.val) (List.map List.toArray xss✝).toArray.flatten =
    (map (fun l => map (fun x => x.val) l) (List.map List.toArray xss✝).toArray).flatten

Tactic:
simp only [flatten_toArray, List.map_map, Function.comp_def, List.map_id_fun', id_eq,
  List.map_toArray, List.map_flatten, map_subtype, map_id_fun', List.unattach_toArray, mk.injEq]

Result:
case of
α : Type u_1
p : α → Prop
xss✝ : List (List { x // p x })
⊢ (List.map (List.map fun x => x.val) xss✝).flatten = (List.map (fun x => x.unattach) xss✝).flatten
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem sin_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y ≠ 0) :
    Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖

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

Tactic:
rw [sub_eq_add_neg, sin_angle_add_of_inner_eq_zero h h0, norm_neg]

Result:
no goals

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

Tactic:
rw [or_comm, ← neg_ne_zero, or_comm] at h0

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y ≠ 0
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖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
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.mul_right [CommMonoid M] {a b : M} (h : a ~ᵤ b) (c : M) : a * c ~ᵤ b * c

Proof state:
case intro
M : Type u_1
inst✝ : CommMonoid M
a c : M
d : Mˣ
⊢ a * c ~ᵤ a * ↑d * c

Tactic:
exact ⟨d, mul_right_comm _ _ _⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
c : M
⊢ a * c ~ᵤ b * c

Tactic:
obtain ⟨d, rfl⟩ := h

Result:
case intro
M : Type u_1
inst✝ : CommMonoid M
a c : M
d : Mˣ
⊢ a * c ~ᵤ a * ↑d * c
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_comp_smul_deriv_Ioi {f f' : ℝ → ℝ} {g : ℝ → E} {a : ℝ}
    (hf : ContinuousOn f <| Ici a) (hft : Tendsto f atTop atTop)
    (hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x)
    (hg_cont : ContinuousOn g <| f '' Ioi a) (hg1 : IntegrableOn g <| f '' Ici a)
    (hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)) :
    (∫ x in Ioi a, f' x • (g ∘ f) x) = ∫ u in Ioi (f a), g u

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (a ⊓ b) (a ⊔ b) ⊆ Ioi a
⊢ [[a, b]] ⊆ Ici a

Tactic:
rw [uIcc_of_le hb.le]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (a ⊓ b) (a ⊔ b) ⊆ Ioi a
⊢ Icc a b ⊆ Ici a

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
⊢ Ioo a (a ⊔ b) ⊆ Ioi a

Tactic:
exact Ioo_subset_Ioi_self

Result:
no goals
-- Mathlib/Order/Cover.lean
@[simp] lemma sdiff_singleton_wcovBy (s : Set α) (a : α) : s \ {a} ⩿ s

Proof state:
case neg
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s \ {a} ⩿ s

Tactic:
simp [ha]

Result:
no goals

Proof state:
case h.e'_4.h
α : Type u_1
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ insert a (s \ {a})

Tactic:
simp [ha]

Result:
no goals

Proof state:
case h.e'_4
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s = insert a (s \ {a})

Tactic:
ext

Result:
case h.e'_4.h
α : Type u_1
s : Set α
a : α
ha : a ∈ s
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ insert a (s \ {a})

Proof state:
case pos
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s \ {a} ⩿ s

Tactic:
convert wcovBy_insert a _

Result:
case h.e'_4
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s = insert a (s \ {a})

Proof state:
α : Type u_1
s : Set α
a : α
⊢ s \ {a} ⩿ s

Tactic:
by_cases ha : a ∈ s

Result:
case pos
α : Type u_1
s : Set α
a : α
ha : a ∈ s
⊢ s \ {a} ⩿ s

case neg
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ s \ {a} ⩿ s
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma eventually_atTop_le_nat {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * n) n, f u ≤ c * f n

Proof state:
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n

Tactic:
obtain ⟨c, hc_mem, hc⟩ := hf.eventually_atTop_le hb

Result:
case intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n

Proof state:
case intro.intro
f : ℝ → ℝ
b : ℝ
hb : b ∈ Set.Ioo 0 1
hf : GrowsPolynomially f
c : ℝ
hc_mem : c > 0
hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
⊢ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n

Tactic:
exact ⟨c, hc_mem, hc.natCast_atTop⟩

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_update (f : Π₀ i, β i) (i : ι) (b : β i) [Decidable (b = 0)] :
    support (f.update i b) = if b = 0 then support (f.erase i) else insert i f.support

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ if b = 0 then (erase i f).support else insert i f.support

Tactic:
split_ifs with hb

Result:
case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ (erase i f).support

case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : ¬b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
rw [support_update_ne_zero f _ hb]

Result:
no goals

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
hb : b = 0
⊢ j ∈ (f.update i b).support ↔ j ∈ (erase i f).support

Tactic:
subst hb

Result:
case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i j : ι
inst✝ : Decidable (0 = 0)
⊢ j ∈ (f.update i 0).support ↔ j ∈ (erase i f).support

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
⊢ (f.update i b).support = if b = 0 then (erase i f).support else insert i f.support

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
inst✝ : Decidable (b = 0)
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ if b = 0 then (erase i f).support else insert i f.support

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i j : ι
inst✝ : Decidable (0 = 0)
⊢ j ∈ (f.update i 0).support ↔ j ∈ (erase i f).support

Tactic:
simp [update_eq_erase, support_erase]

Result:
no goals
-- Mathlib/Algebra/Lie/Abelian.lean
theorem mem_ker (x : L) : x ∈ LieModule.ker R L M ↔ ∀ m : M, ⁅x, m⁆ = 0

Proof state:
R : Type u
L : Type v
M : Type w
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
x : L
⊢ x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0

Tactic:
simp only [LieModule.ker, LieHom.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply,
  toEnd_apply_apply]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem le_einfsep_pi_of_le {π : β → Type*} [Fintype β] [∀ b, PseudoEMetricSpace (π b)]
    {s : ∀ b : β, Set (π b)} {c : ℝ≥0∞} (h : ∀ b, c ≤ einfsep (s b)) :
    c ≤ einfsep (Set.pi univ s)

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y

Tactic:
rcases Function.ne_iff.mp hxy with ⟨i, hi⟩

Result:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
⊢ c ≤ (univ.pi s).einfsep

Tactic:
refine le_einfsep fun x hx y hy hxy => ?_

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → π i
hx : x ∈ univ.pi s
y : (i : β) → π i
hy : y ∈ univ.pi s
hxy : x ≠ y
⊢ c ≤ edist x y

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → π i
hx : x ∈ univ.pi s
y : (i : β) → π i
hy : y ∈ univ.pi s
hxy : x ≠ y
⊢ c ≤ edist x y

Tactic:
rw [mem_univ_pi] at hx hy

Result:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y

Proof state:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y

Tactic:
exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem snd_pow_of_smul_comm' [Monoid R] [AddMonoid M] [DistribMulAction R M]
    [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (x : tsze R M) (n : ℕ)
    (h : x.snd <• x.fst = x.fst •> x.snd) : snd (x ^ n) = n • (x.snd <• x.fst ^ n.pred)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (x ^ n).snd = n •> (x.snd <• x.fst ^ n.pred)

Tactic:
rw [snd_pow_of_smul_comm _ _ h, snd_pow_of_smul_comm.aux _ h]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem self_add_star : a + star a = 2 * a.re + c₂ * a.imI

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a + star a = 2 * ↑a.re + ↑c₂ * ↑a.imI

Tactic:
simp [self_add_star']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
    l.mapFinIdx f = l' ↔ ∃ h : l'.size = l.size, ∀ (i : Nat) (h : i < l.size), l'[i] = f i l[i] h

Proof state:
α : Type u_1
β : Type u_2
l' : Array β
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ l.mapFinIdx f = l' ↔ ∃ h, ∀ (i : Nat) (h_1 : i < l.size), l'[i] = f i l[i] h_1

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
l' : Array β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ { toList := l }.mapFinIdx f = l' ↔
    ∃ h, ∀ (i : Nat) (h_1 : i < { toList := l }.size), l'[i] = f i { toList := l }[i] h_1

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l' : List β
⊢ { toList := l }.mapFinIdx f = { toList := l' } ↔
    ∃ h, ∀ (i : Nat) (h_1 : i < { toList := l }.size), { toList := l' }[i] = f i { toList := l }[i] h_1

Tactic:
simpa using List.mapFinIdx_eq_iff

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
l' : Array β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
⊢ { toList := l }.mapFinIdx f = l' ↔
    ∃ h, ∀ (i : Nat) (h_1 : i < { toList := l }.size), l'[i] = f i { toList := l }[i] h_1

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
l' : List β
⊢ { toList := l }.mapFinIdx f = { toList := l' } ↔
    ∃ h, ∀ (i : Nat) (h_1 : i < { toList := l }.size), { toList := l' }[i] = f i { toList := l }[i] h_1
-- Mathlib/Analysis/PSeries.lean
theorem sum_condensed_le (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) :
    (∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k)) ≤ f 1 + 2 • ∑ k ∈ Ico 2 (2 ^ n + 1), f k

Proof state:
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k ∈ Ico 2 (2 ^ n + 1), f k

Tactic:
convert add_le_add_left (nsmul_le_nsmul_right (sum_condensed_le' hf n) 2) (f 1)

Result:
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) = f 1 + 2 • ∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1))

Proof state:
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) = f 1 + 2 • ∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1))

Tactic:
simp [sum_range_succ', add_comm, pow_succ', mul_nsmul', sum_nsmul]

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem mem_neLocus {f g : α →₀ N} {a : α} : a ∈ f.neLocus g ↔ f a ≠ g a

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
a : α
⊢ a ∈ f.neLocus g ↔ f a ≠ g a

Tactic:
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
  and_iff_right_iff_imp] using Ne.ne_or_ne _

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :
    (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ x ∈ s ×ˢ ⋂ i, t i ↔ x ∈ ⋂ i, s ×ˢ t i

Tactic:
simp only [mem_prod, mem_iInter]

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ (x.1 ∈ s ∧ ∀ (i : ι), x.2 ∈ t i) ↔ ∀ (i : ι), x.1 ∈ s ∧ x.2 ∈ t i

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
⊢ s ×ˢ ⋂ i, t i = ⋂ i, s ×ˢ t i

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ x ∈ s ×ˢ ⋂ i, t i ↔ x ∈ ⋂ i, s ×ˢ t i

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
hι : Nonempty ι
x : α × β
⊢ (x.1 ∈ s ∧ ∀ (i : ι), x.2 ∈ t i) ↔ ∀ (i : ι), x.1 ∈ s ∧ x.2 ∈ t i

Tactic:
exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem fstIdx_cons {i} (m : M i) (w : Word M) (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1) :
    fstIdx (cons m w hmw h1) = some i

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
m : M i
w : Word M
hmw : w.fstIdx ≠ some i
h1 : m ≠ 1
⊢ (cons m w hmw h1).fstIdx = some i

Tactic:
simp [cons, fstIdx]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Equidecomp.lean
theorem IsDecompOn.of_leftInvOn {f g : X → X} {A : Set X} {S : Finset G}
    (hf : IsDecompOn f A S) (h : LeftInvOn g f A) : IsDecompOn g (f '' A) S⁻¹

Proof state:
case intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a

Tactic:
rcases hf a ha with ⟨γ, γ_mem, hγ⟩

Result:
case intro.intro.intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a

Proof state:
case right
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ g (f a) = γ⁻¹ • f a

Tactic:
rw [hγ, inv_smul_smul, ← hγ, h ha]

Result:
no goals

Proof state:
case intro.intro.intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a

Tactic:
use γ⁻¹, Finset.inv_mem_inv γ_mem

Result:
case right
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
γ : G
γ_mem : γ ∈ S
hγ : f a = γ • a
⊢ g (f a) = γ⁻¹ • f a

Proof state:
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
⊢ IsDecompOn g (f '' A) S⁻¹

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
X : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
f g : X → X
A : Set X
S : Finset G
hf : IsDecompOn f A S
h : LeftInvOn g f A
a : X
ha : a ∈ A
⊢ ∃ g_1 ∈ S⁻¹, g (f a) = g_1 • f a