harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma le_expGrowthSup_iff {u : ℕ → ℝ≥0∞} {a : EReal} :
    a ≤ expGrowthSup u ↔ ∀ b < a, ∃ᶠ n : ℕ in atTop, exp (b * n) < u n

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b < (u n).log / ↑n ↔ (b * ↑n).exp < u n

Tactic:
rw [EReal.lt_div_iff (by norm_cast) (natCast_ne_top n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b * ↑n < (u n).log ↔ (b * ↑n).exp < u n

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b * ↑n < (u n).log ↔ (b * ↑n).exp < u n

Tactic:
nth_rw 1 [← EReal.log_exp (b * n)]

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ (b * ↑n).exp.log < (u n).log ↔ (b * ↑n).exp < u n

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ 0 < ↑n

Tactic:
norm_cast

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y < (u a).log / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp < u n

Tactic:
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Result:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ b < (u n).log / ↑n ↔ (b * ↑n).exp < u n

Proof state:
u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : n ≥ 1
⊢ (b * ↑n).exp.log < (u n).log ↔ (b * ↑n).exp < u n

Tactic:
exact logOrderIso.lt_iff_lt

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
a : EReal
⊢ a ≤ expGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp < u n

Tactic:
rw [expGrowthSup, Filter.le_limsup_iff]

Result:
u : ℕ → ℝ≥0∞
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y < (u a).log / ↑a) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp < u n
-- Mathlib/GroupTheory/Perm/List.lean
theorem mem_of_formPerm_apply_mem (h : l.formPerm x ∈ l) : x ∈ l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∉ l
⊢ l.formPerm x ∉ l

Tactic:
rwa [formPerm_apply_of_not_mem h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ∈ l
⊢ x ∈ l

Tactic:
contrapose h

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∉ l
⊢ l.formPerm x ∉ l
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.tendstoUniformlyOn' {r' : ℝ≥0} (hf : HasFPowerSeriesOnBall f p x r)
    (h : (r' : ℝ≥0∞) < r) :
    TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (Metric.ball (x : E) r')

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (Metric.ball x ↑r')

Tactic:
simpa using hf.tendstoUniformlyOn' h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesOnBall f p x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (Metric.ball x ↑r')

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑r' < r
⊢ TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (Metric.ball x ↑r')
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.exists_pow_eq (hf : IsCycle f) (hx : f x ≠ x) (hy : f y ≠ y) :
    ∃ i : ℕ, (f ^ i) x = y

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ ∃ i, (f ^ i) x = y

Tactic:
classical exact
    ⟨(n % orderOf f).toNat, by
      {have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
       rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
this : 0 ≤ n % ↑(orderOf f)
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Tactic:
rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Tactic:
have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))

Result:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
this : 0 ≤ n % ↑(orderOf f)
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ ∃ i, (f ^ i) x = y

Tactic:
exact
⟨(n % orderOf f).toNat, by
{have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
⊢ ∃ i, (f ^ i) x = y

Tactic:
let ⟨n, hn⟩ := hf.exists_zpow_eq hx hy

Result:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ ∃ i, (f ^ i) x = y
-- Mathlib/Data/Vector/Basic.lean
theorem reverse_reverse {v : Vector α n} : v.reverse.reverse = v

Proof state:
α : Type u_1
n : ℕ
v : Vector α n
⊢ v.reverse.reverse = v

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
val✝ : List α
property✝ : val✝.length = n
⊢ (reverse ⟨val✝, property✝⟩).reverse = ⟨val✝, property✝⟩

Proof state:
case mk
α : Type u_1
n : ℕ
val✝ : List α
property✝ : val✝.length = n
⊢ (reverse ⟨val✝, property✝⟩).reverse = ⟨val✝, property✝⟩

Tactic:
simp [Vector.reverse]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
theorem contDiffAt_arccos_iff {x : ℝ} {n : WithTop ℕ∞} :
    ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

Proof state:
x : ℝ
n : WithTop ℕ∞
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

Tactic:
refine Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff <;>
  simpa [arccos] using (contDiffAt_const (c := π / 2)).sub h

Result:
no goals
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G) :
    Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
  ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul c⁻¹, fun h => h.const_smul _⟩

Proof state:
α : Type u_2
β : Type u_3
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
f : β → α
l : Filter β
a : α
c : G
h : Tendsto (fun x => c • f x) l (𝓝 (c • a))
⊢ Tendsto f l (𝓝 a)

Tactic:
simpa only [inv_smul_smul] using h.const_smul c⁻¹

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma tail_cons_eq (h : G.Adj u v) (p : G.Walk v w) :
    (p.cons h).tail = p.copy (getVert_zero p).symm rfl

Proof state:
V : Type u
G : SimpleGraph V
u v w✝ : V
h✝ : G.Adj u v
p : G.Walk v w✝
w v✝ : V
h : G.Adj v v✝
q : G.Walk v✝ w
⊢ (cons h✝ (cons h q)).tail = (cons h q).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).tail = p.copy ⋯ ⋯

Tactic:
match p with
| .nil => rfl
| .cons h q => rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h nil).tail = nil.copy ⋯ ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem restrict_empty (M : Matroid α) : M ↾ (∅ : Set α) = emptyOn α

Proof state:
α : Type u_1
M : Matroid α
⊢ M ↾ ∅ = emptyOn α

Tactic:
simp [← ground_eq_empty_iff]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
theorem isBigO_asympBound : T =O[atTop] asympBound g a b

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n => (1 - ε ↑n) * asympBound g a b n) =O[atTop] fun n => 1 * asympBound g a b n

Tactic:
refine IsBigO.mul (isBigO_const_of_tendsto (y := 1) ?_ one_ne_zero)
  (isBigO_refl _ _)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto (fun n => 1 - ε ↑n) atTop (𝓝 1)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ T =O[atTop] fun n => (1 - ε ↑n) * asympBound g a b n

Tactic:
exact R.T_isBigO_smoothingFn_mul_asympBound

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto (fun n => 1 - ε ↑n) atTop (𝓝 1)

Tactic:
rw [← Function.comp_def (fun n => 1 - ε n) Nat.cast]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n => 1 - ε n) ∘ Nat.cast) atTop (𝓝 1)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n => 1 - ε n) ∘ Nat.cast) atTop (𝓝 1)

Tactic:
exact Tendsto.comp isEquivalent_one_sub_smoothingFn_one.tendsto_const
  tendsto_natCast_atTop_atTop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n => 1 * asympBound g a b n) = asympBound g a b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ T =O[atTop] asympBound g a b

Tactic:
calc T =O[atTop] (fun n => (1 - ε n) * asympBound g a b n) := by
            exact R.T_isBigO_smoothingFn_mul_asympBound
       _ =O[atTop] (fun n => 1 * asympBound g a b n) := by
            refine IsBigO.mul (isBigO_const_of_tendsto (y := 1) ?_ one_ne_zero)
              (isBigO_refl _ _)
            rw [← Function.comp_def (fun n => 1 - ε n) Nat.cast]
            exact Tendsto.comp isEquivalent_one_sub_smoothingFn_one.tendsto_const
              tendsto_natCast_atTop_atTop
       _ = asympBound g a b := by simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem _root_.normalizerCondition_iff_only_full_group_self_normalizing :
    NormalizerCondition G ↔ ∀ H : Subgroup G, H.normalizer = H → H = ⊤

Proof state:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H < ⊤ → H < H.normalizer ↔ H.normalizer = H → H = ⊤

Tactic:
simp only [lt_iff_le_and_ne, le_normalizer, le_top, Ne]

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ True ∧ ¬H = ⊤ → True ∧ ¬H = H.normalizer ↔ H.normalizer = H → H = ⊤

Proof state:
case h
G : Type u_1
inst✝ : Group G
⊢ ∀ (a : Subgroup G), a < ⊤ → a < a.normalizer ↔ a.normalizer = a → a = ⊤

Tactic:
intro H

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H < ⊤ → H < H.normalizer ↔ H.normalizer = H → H = ⊤

Proof state:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ True ∧ ¬H = ⊤ → True ∧ ¬H = H.normalizer ↔ H.normalizer = H → H = ⊤

Tactic:
tauto

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
⊢ NormalizerCondition G ↔ ∀ (H : Subgroup G), H.normalizer = H → H = ⊤

Tactic:
apply forall_congr'

Result:
case h
G : Type u_1
inst✝ : Group G
⊢ ∀ (a : Subgroup G), a < ⊤ → a < a.normalizer ↔ a.normalizer = a → a = ⊤
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfpFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (a) :
    f i (nfpFamily f a) = nfpFamily f a

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i_1, f i (List.foldr f a i_1) = ⨆ i, List.foldr f a i

Tactic:
apply le_antisymm <;> refine Ordinal.iSup_le fun l => ?_

Result:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i

case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)

Proof state:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ f i (nfpFamily f a) = nfpFamily f a

Tactic:
rw [nfpFamily, H.map_iSup]

Result:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i_1, f i (List.foldr f a i_1) = ⨆ i, List.foldr f a i

Proof state:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i

Tactic:
exact Ordinal.le_iSup _ (i::l)

Result:
no goals

Proof state:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ List.foldr f a l ≤ ⨆ i_1, f i (List.foldr f a i_1)

Tactic:
exact H.le_apply.trans (Ordinal.le_iSup _ _)

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Pi.lean
theorem piFamily_single [Fintype ι] [∀ i, DecidableEq (κ i)]
    (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p))
    (p : ∀ i, κ i) (m : ∀ i, M i (p i)) :
    piFamily f (fun i => Pi.single (p i) (m i)) = Pi.single p (f p m)

Proof state:
case h.inr.intro
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
⊢ (piFamily f) (fun i => Pi.single (p i) (m i)) q = 0

Tactic:
apply (f q).map_coord_zero i

Result:
case h.inr.intro
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
⊢ (fun i => Pi.single (p i) (m i)) i (q i) = 0

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
⊢ ((piFamily f) fun i => Pi.single (p i) (m i)) = Pi.single p ((f p) m)

Tactic:
ext q

Result:
case h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
⊢ (piFamily f) (fun i => Pi.single (p i) (m i)) q = Pi.single p ((f p) m) q
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem CliqueFree.comap {H : SimpleGraph β} (f : H ↪g G) : G.CliqueFree n → H.CliqueFree n

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
f : H ↪g G
h : ¬H.CliqueFree n
⊢ ¬G.CliqueFree n

Tactic:
exact not_cliqueFree_of_top_embedding <| f.comp (topEmbeddingOfNotCliqueFree h)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
f : H ↪g G
⊢ G.CliqueFree n → H.CliqueFree n

Tactic:
intro h

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
f : H ↪g G
h : G.CliqueFree n
⊢ H.CliqueFree n

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
f : H ↪g G
h : G.CliqueFree n
⊢ H.CliqueFree n

Tactic:
contrapose h

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
H : SimpleGraph β
f : H ↪g G
h : ¬H.CliqueFree n
⊢ ¬G.CliqueFree n
-- Mathlib/Data/Matrix/RowCol.lean
theorem submatrix_updateRow_equiv [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m)
    (r : n → α) (e : l ≃ m) (f : o ≃ n) :
    (A.updateRow i r).submatrix e f = updateRow (A.submatrix e f) (e.symm i) fun i => r (f i) :=
  Eq.trans (by simp_rw [Equiv.apply_symm_apply]) (updateRow_submatrix_equiv A _ _ e f).symm

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : m
r : n → α
e : l ≃ m
f : o ≃ n
⊢ (A.updateRow i r).submatrix ⇑e ⇑f = (A.updateRow (e (e.symm i)) fun j => r (f (f.symm j))).submatrix ⇑e ⇑f

Tactic:
simp_rw [Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Topology/Homotopy/Path.lean
theorem eval_zero (F : Homotopy p₀ p₁) : F.eval 0 = p₀

Proof state:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 0) t = p₀ t

Tactic:
simp [eval]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 0 = p₀

Tactic:
ext t

Result:
case a.h
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 0) t = p₀ t
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem mk_mem_localTrivAt_source : (⟨b, a⟩ : Z.TotalSpace) ∈ (Z.localTrivAt b).source

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
a : F
⊢ { proj := b, snd := a } ∈ (Z.localTrivAt b).source

Tactic:
simp only [mfld_simps]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem neg_mul {R} [Ring R] (a₁ : R) (a₂) {a₃ b : R}
    (_ : -a₃ = b) : -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Proof state:
R : Type u_2
inst✝ : Ring R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
a₁ : R
a₂ : ℕ
a₃ b : R
x✝ : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : Ring R
a₁ : R
a₂ : ℕ
a₃ : R
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * -a₃
-- Mathlib/Probability/Independence/Conditional.lean
lemma condIndep_iff_condIndepSets (m' m₁ m₂ : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω}
    [StandardBorelSpace Ω] (hm' : m' ≤ mΩ) (μ : Measure Ω ) [IsFiniteMeasure μ] :
    CondIndep m' m₁ m₂ hm' μ
      ↔ CondIndepSets m' hm' {s | MeasurableSet[m₁] s} {s | MeasurableSet[m₂] s} μ

Proof state:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔ CondIndepSets m' hm' {s | MeasurableSet s} {s | MeasurableSet s} μ

Tactic:
simp only [CondIndep, CondIndepSets, Kernel.Indep]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_union_le (s s' : Set α) : μ.restrict (s ∪ s') ≤ μ.restrict s + μ.restrict s' :=
  le_iff.2 fun t ht ↦ by
    simpa [ht, inter_union_distrib_left] using measure_union_le (t ∩ s) (t ∩ s')

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s s' t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (s ∪ s')) t ≤ (μ.restrict s + μ.restrict s') t

Tactic:
simpa [ht, inter_union_distrib_left] using measure_union_le (t ∩ s) (t ∩ s')

Result:
no goals
-- Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean
theorem IsLocalRing.of_nilradical_isMaximal [h : (nilradical R).IsMaximal] :
    IsLocalRing R

Proof state:
R : Type u_4
inst✝ : CommSemiring R
h : (nilradical R).IsMaximal
I : Ideal R
hI : (fun I => I.IsMaximal) I
⊢ I = nilradical R

Tactic:
rw [nilradical_eq_sInf] at h ⊢

Result:
R : Type u_4
inst✝ : CommSemiring R
h : (sInf {J | J.IsPrime}).IsMaximal
I : Ideal R
hI : I.IsMaximal
⊢ I = sInf {J | J.IsPrime}

Proof state:
R : Type u_4
inst✝ : CommSemiring R
h : (nilradical R).IsMaximal
⊢ IsLocalRing R

Tactic:
refine IsLocalRing.of_unique_max_ideal ⟨nilradical R, h, fun I hI ↦ ?_⟩

Result:
R : Type u_4
inst✝ : CommSemiring R
h : (nilradical R).IsMaximal
I : Ideal R
hI : (fun I => I.IsMaximal) I
⊢ I = nilradical R

Proof state:
R : Type u_4
inst✝ : CommSemiring R
h : (sInf {J | J.IsPrime}).IsMaximal
I : Ideal R
hI : I.IsMaximal
⊢ I = sInf {J | J.IsPrime}

Tactic:
exact (IsMaximal.eq_of_le h hI.ne_top (sInf_le hI.isPrime)).symm

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem top_eq [IsWellOrder γ t] (e : r ≃r s) (f : r ≺i t) (g : s ≺i t) : f.top = g.top

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ f.top = g.top

Tactic:
rw [Subsingleton.elim f (PrincipalSeg.relIsoTrans e g)]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsRefl.nondegenerate_iff_separatingLeft {B : M →ₗ[R] M →ₗ[R] M₁} (hB : B.IsRefl) :
    B.Nondegenerate ↔ B.SeparatingLeft

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
⊢ B.Nondegenerate ↔ B.SeparatingLeft

Tactic:
refine ⟨fun h ↦ h.1, fun hB' ↦ ⟨hB', ?_⟩⟩

Result:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingLeft
⊢ B.SeparatingRight

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingLeft
⊢ ker B = ⊥

Tactic:
rwa [← separatingLeft_iff_ker_eq_bot]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingLeft
⊢ B.SeparatingRight

Tactic:
rw [separatingRight_iff_flip_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mp]

Result:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingLeft
⊢ ker B = ⊥