harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- The scalar factor between two left-invariant measures is non-zero when both measures are
positive on open sets. -/
@[to_additive]
lemma haarScalarFactor_pos_of_isHaarMeasure (μ' μ : Measure G) [IsHaarMeasure μ]
    [IsHaarMeasure μ'] : 0 < haarScalarFactor μ' μ :=
  pos_iff_ne_zero.2 (fun H ↦ by simpa [H] using haarScalarFactor_eq_mul μ' μ μ')

Proof state:
G : Type u_1
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
H : μ'.haarScalarFactor μ = 0
⊢ False

Tactic:
simpa [H] using haarScalarFactor_eq_mul μ' μ μ'

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@[reassoc (attr := simp)]
lemma ι_colimitIsoOfIsLeftKanExtension_inv (i : C) :
    colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv =
    α.app i ≫ colimit.ι F' (L.obj i)

Proof state:
C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_3} H
inst✝³ : Category.{u_8, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv = α.app i ≫ colimit.ι F' (L.obj i)

Tactic:
rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]

Result:
no goals
-- Mathlib/Logic/Lemmas.lean
lemma Prop.exists {f : Prop → Prop} : (∃ p, f p) ↔ f True ∨ f False :=
  ⟨fun ⟨p, h⟩ ↦ by refine (em p).imp ?_ ?_ <;> intro H <;> convert h <;> simp [H],
    by rintro (h | h) <;> exact ⟨_, h⟩⟩

Proof state:
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False

Tactic:
refine (em p).imp ?_ ?_ <;> intro H <;> convert h <;> simp [H]

Result:
no goals

Proof state:
f : Prop → Prop
⊢ f True ∨ f False → ∃ p, f p

Tactic:
rintro (h | h) <;> exact ⟨_, h⟩

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPullback.iso_hom_fst :
    (PreservesPullback.iso G f g).hom ≫ pullback.fst _ _ = G.map (pullback.fst f g)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.fst (G.map f) (G.map g) = G.map (pullback.fst f g)

Tactic:
simp [PreservesPullback.iso]

Result:
no goals
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem gaugeRescale_smul (s t : Set E) {c : ℝ} (hc : 0 ≤ c) (x : E) :
    gaugeRescale s t (c • x) = c • gaugeRescale s t x

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ gaugeRescale s t (c • x) = c • gaugeRescale s t x

Tactic:
simp only [gaugeRescale, gauge_smul_of_nonneg hc, smul_smul, smul_eq_mul]

Result:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
c : ℝ
hc : 0 ≤ c
x : E
⊢ (c * gauge s x / (c * gauge t x) * c) • x = (c * (gauge s x / gauge t x)) • x

Tactic:
rw [mul_div_mul_comm, mul_right_comm, div_self_mul_self]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem lift'_iInf [Nonempty ι] {f : ι → Filter α} {g : Set α → Set β}
    (hg : ∀ s t, g (s ∩ t) = g s ∩ g t) : (iInf f).lift' g = ⨅ i, (f i).lift' g :=
  lift_iInf fun s t => by simp only [inf_principal, comp, hg]

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Set β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ∩ g t
s t : Set α
⊢ (𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t

Tactic:
simp only [inf_principal, comp, hg]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem Balanced.interior (hA : Balanced 𝕜 A) (h : (0 : E) ∈ interior A) :
    Balanced 𝕜 (interior A)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (interior A)

Tactic:
rw [← insert_eq_self.2 h]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (insert 0 (interior A))

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (insert 0 (interior A))

Tactic:
exact hA.zero_insert_interior

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subsemiring R} (hS : Directed (· ≤ ·) S)
    {x : R} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Result:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
let U : Subsemiring R :=
  Subsemiring.mk' (⋃ i, (S i : Set R))
    (⨆ i, (S i).toSubmonoid) (Submonoid.coe_iSup_of_directed hS)
    (⨆ i, (S i).toAddSubmonoid) (AddSubmonoid.coe_iSup_of_directed hS)

Result:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices ⨆ i, S i ≤ U by simpa [U] using @this x

Result:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ ⨆ i, S i ≤ U

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @this x

Result:
no goals

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subsemiring R := Subsemiring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) ⋯ (⨆ i, (S i).toAddSubmonoid) ⋯
⊢ ⨆ i, S i ≤ U

Tactic:
exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_mul (a m n : Nat) : a ^ (m * n) = (a ^ m) ^ n

Proof state:
case zero
a m : Nat
⊢ a ^ (m * 0) = (a ^ m) ^ 0

Tactic:
rw [Nat.mul_zero, Nat.pow_zero, Nat.pow_zero]

Result:
no goals

Proof state:
case succ
a m n✝ : Nat
ih : a ^ (m * n✝) = (a ^ m) ^ n✝
⊢ a ^ (m * (n✝ + 1)) = (a ^ m) ^ (n✝ + 1)

Tactic:
rw [Nat.mul_succ, Nat.pow_add, Nat.pow_succ, ih]

Result:
no goals

Proof state:
a m n : Nat
⊢ a ^ (m * n) = (a ^ m) ^ n

Tactic:
induction n with
| zero => rw [Nat.mul_zero, Nat.pow_zero, Nat.pow_zero]
| succ _ ih => rw [Nat.mul_succ, Nat.pow_add, Nat.pow_succ, ih]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_injective (n : ℕ) [NeZero n] : Function.Injective (val : ZMod n → ℕ)

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ a = b

Tactic:
ext

Result:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ ↑a = ↑b

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ Injective val

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
⊢ Injective val

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Injective val

Proof state:
case succ.h
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ ↑a = ↑b

Tactic:
exact h

Result:
no goals

Proof state:
case zero
inst✝ : NeZero 0
⊢ Injective val

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ Injective val

Tactic:
intro a b h

Result:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a b : ZMod (n✝ + 1)
h : a.val = b.val
⊢ a = b
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_ground (M : Matroid α) : M.cRk M.E = M.cRank

Proof state:
α : Type u
M : Matroid α
⊢ M.cRk M.E = M.cRank

Tactic:
rw [cRk, restrict_ground_eq_self]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_one_left' [GCDMonoid α] (a : α) : Associated (gcd 1 a) 1

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd 1 a) 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem eta (s : Stream' α) : head s :: tail s = s :=
  funext fun i => by cases i <;> rfl

Proof state:
α : Type u
s : Stream' α
i : ℕ
⊢ (s.head :: s.tail) i = s i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem singleton_perm_singleton {a b : α} : [a] ~ [b] ↔ a = b

Proof state:
α : Type u_1
a b : α
⊢ [a] ~ [b] ↔ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem deriv_lt_ord {f : Ordinal.{u} → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀)
    (hf : ∀ i < c.ord, f i < c.ord) {a} : a < c.ord → deriv f a < c.ord :=
  derivFamily_lt_ord_lift hc
    (by simpa using Cardinal.one_lt_aleph0.trans (lt_of_le_of_ne hc.1 hc'.symm)) hc' fun _ => hf

Proof state:
f : Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u}
⊢ lift.{u, 0} #Unit < c

Tactic:
simpa using Cardinal.one_lt_aleph0.trans (lt_of_le_of_ne hc.1 hc'.symm)

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiable_iff :
    MDifferentiable I I' f ↔
      Continuous f ∧
        ∀ (x : M) (y : M'),
          DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
            ((extChartAt I x).target ∩
              (extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ MDifferentiable I I' f ↔
    Continuous f ∧
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))

Tactic:
simp [← mdifferentiableOn_univ, mdifferentiableOn_iff, continuous_iff_continuousOn_univ]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem sameCycle_iff_cycleOf_eq_of_mem_support [DecidableEq α] [Fintype α]
    {g : Perm α} {x y : α} (hx : x ∈ g.support) (hy : y ∈ g.support) :
    g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
⊢ g.SameCycle x y

Tactic:
rw [← mem_support_cycleOf_iff' (mem_support.mp hx), h,
  mem_support_cycleOf_iff' (mem_support.mp hy)]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
⊢ g.SameCycle x y ↔ g.cycleOf x = g.cycleOf y

Tactic:
refine ⟨SameCycle.cycleOf_eq, fun h ↦ ?_⟩

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x y : α
hx : x ∈ g.support
hy : y ∈ g.support
h : g.cycleOf x = g.cycleOf y
⊢ g.SameCycle x y
-- Mathlib/Probability/Kernel/Invariance.lean
theorem Invariant.comp_const (hκ : Invariant κ μ) : κ ∘ₖ const α μ = const α μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
⊢ κ ∘ₖ const α μ = const α μ

Tactic:
rw [← const_bind_eq_comp_const κ μ, hκ.def]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/DList/Lemmas.lean
theorem toList_cons (x : α) (l : DList α) : toList (cons x l) = x :: toList l

Proof state:
α : Type u_1
x : α
l : DList α
⊢ (cons x l).toList = x :: l.toList

Tactic:
cases l

Result:
case mk
α : Type u_1
x : α
apply✝ : List α → List α
invariant✝ : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ (cons x { apply := apply✝, invariant := invariant✝ }).toList =
    x :: { apply := apply✝, invariant := invariant✝ }.toList

Proof state:
case mk
α : Type u_1
x : α
apply✝ : List α → List α
invariant✝ : ∀ (l : List α), apply✝ l = apply✝ [] ++ l
⊢ (cons x { apply := apply✝, invariant := invariant✝ }).toList =
    x :: { apply := apply✝, invariant := invariant✝ }.toList

Tactic:
simp [cons]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem support_single_mul_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
    (hr : ∀ y, r * y = 0 ↔ y = 0) {x : G} (lx : IsLeftRegular x) :
    (single x r * f : MonoidAlgebra k G).support = Finset.image (x * ·) f.support

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
⊢ (single x r * f).support = image (fun x_1 => x * x_1) f.support

Tactic:
refine subset_antisymm (support_single_mul_subset f _ _) fun y hy => ?_

Result:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image (fun x_1 => x * x_1) f.support
⊢ y ∈ (single x r * f).support

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image (fun x_1 => x * x_1) f.support
⊢ y ∈ (single x r * f).support

Tactic:
obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
  simpa only [Finset.mem_image, exists_prop] using hy

Result:
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
yf : y ∈ f.support
hy : x * y ∈ image (fun x_1 => x * x_1) f.support
⊢ x * y ∈ (single x r * f).support

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
hy : y ∈ image (fun x_1 => x * x_1) f.support
⊢ ∃ a ∈ f.support, x * a = y

Tactic:
simpa only [Finset.mem_image, exists_prop] using hy

Result:
no goals

Proof state:
case intro.intro
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
yf : y ∈ f.support
hy : x * y ∈ image (fun x_1 => x * x_1) f.support
⊢ x * y ∈ (single x r * f).support

Tactic:
simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index,
  Finsupp.sum_ite_eq', Ne, not_false_iff, if_true, zero_mul, ite_self, sum_zero, lx.eq_iff]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem insertIdx_comm (a b : α) (i j : Fin (n + 1)) (h : i ≤ j) :
    ∀ v : Vector α n,
      (v.insertIdx a i).insertIdx b j.succ = (v.insertIdx b j).insertIdx a (Fin.castSucc i)
  | ⟨l, hl⟩ => by
    refine Subtype.eq ?_
    simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.coe_castAdd]
    apply List.insertIdx_comm
    · assumption
    · rw [hl]
      exact Nat.le_of_succ_le_succ j.2

Proof state:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑i ≤ ↑j

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑(insertIdx b j.succ (insertIdx a i ⟨l, hl⟩)) = ↑(insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩))

Tactic:
simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.coe_castAdd]

Result:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ List.insertIdx (↑j + 1) b (List.insertIdx (↑i) a l) = List.insertIdx (↑i) a (List.insertIdx (↑j) b l)

Proof state:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ n

Tactic:
exact Nat.le_of_succ_le_succ j.2

Result:
no goals

Proof state:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ l.length

Tactic:
rw [hl]

Result:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ n

Proof state:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ List.insertIdx (↑j + 1) b (List.insertIdx (↑i) a l) = List.insertIdx (↑i) a (List.insertIdx (↑j) b l)

Tactic:
apply List.insertIdx_comm

Result:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑i ≤ ↑j

case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ l.length

Proof state:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ insertIdx b j.succ (insertIdx a i ⟨l, hl⟩) = insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩)

Tactic:
refine Subtype.eq ?_

Result:
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑(insertIdx b j.succ (insertIdx a i ⟨l, hl⟩)) = ↑(insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩))
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem coe_smul (r : ℝ≥0) : (r : ℝ) • j = r • j

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ ↑r • j = r • j

Tactic:
rw [real_smul_def, if_pos (NNReal.coe_nonneg r), Real.toNNReal_coe]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_one (L : List ℕ) : ofDigits 1 L = L.sum

Proof state:
case nil

⊢ ofDigits 1 [] = [].sum

Tactic:
rfl

Result:
no goals

Proof state:
L : List ℕ
⊢ ofDigits 1 L = L.sum

Tactic:
induction L with
| nil => rfl
| cons _ _ ih => simp [ofDigits, List.sum_cons, ih]

Result:
no goals

Proof state:
case cons
head✝ : ℕ
tail✝ : List ℕ
ih : ofDigits 1 tail✝ = tail✝.sum
⊢ ofDigits 1 (head✝ :: tail✝) = (head✝ :: tail✝).sum

Tactic:
simp [ofDigits, List.sum_cons, ih]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem orderOf_r [NeZero n] (i : ZMod n) : orderOf (r i) = n / Nat.gcd n i.val

Proof state:
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r ↑i.val) = n / n.gcd i.val

Tactic:
rw [← r_one_pow, orderOf_pow, orderOf_r_one]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r i) = n / n.gcd i.val

Tactic:
conv_lhs => rw [← ZMod.natCast_zmod_val i]

Result:
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r ↑i.val) = n / n.gcd i.val
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@[fun_prop]
lemma continuous_toNNReal : Continuous (toNNReal (X := X))

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (ContinuousMap.toNNReal ∘ _root_.toContinuousMap)

Tactic:
exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (_root_.toContinuousMap ∘ toNNReal)

Tactic:
convert_to Continuous (ContinuousMap.toNNReal ∘ ((↑) : C(X, ℝ)₀ → C(X, ℝ))) using 1

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (ContinuousMap.toNNReal ∘ _root_.toContinuousMap)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous toNNReal

Tactic:
rw [continuous_induced_rng]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
⊢ Continuous (_root_.toContinuousMap ∘ toNNReal)
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma derives_reverse_comm : g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse

Proof state:
T : Type u_1
g : ContextFreeGrammar T
u v : List (Symbol T g.NT)
⊢ g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse

Tactic:
rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem Filter.EventuallyEq.iteratedFDerivWithin' (h : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t

Proof state:
case zero
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ iteratedFDerivWithin 𝕜 0 f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 0 f t

Tactic:
exact h.mono fun y hy => DFunLike.ext _ _ fun _ => hy

Result:
no goals

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 (n + 1) f t

Tactic:
have : fderivWithin 𝕜 _ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 _ t := ihn.fderivWithin' ht

Result:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
this : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t =ᶠ[𝓝[s] x] fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 (n + 1) f t

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
this : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t =ᶠ[𝓝[s] x] fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 (n + 1) f t

Tactic:
refine this.mono fun y hy => ?_

Result:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
n : ℕ
ihn : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
this : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t =ᶠ[𝓝[s] x] fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t
y : E
hy : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f₁ t) t y = fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f t) t y
⊢ iteratedFDerivWithin 𝕜 (n + 1) f₁ t y = iteratedFDerivWithin 𝕜 (n + 1) f t y