harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/ZMod/QuotientGroup.lean
theorem _root_.AddAction.orbitZMultiplesEquiv_symm_apply' {α β : Type*} [AddGroup α] (a : α)
    [AddAction α β] (b : β) (k : ℤ) :
    (AddAction.orbitZMultiplesEquiv a b).symm k =
      k • (⟨a, mem_zmultiples a⟩ : zmultiples a) +ᵥ ⟨b, AddAction.mem_orbit_self b⟩

Proof state:
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (orbitZMultiplesEquiv a b).symm ↑k = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Tactic:
rw [AddAction.orbitZMultiplesEquiv_symm_apply, ZMod.coe_intCast]

Result:
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod (fun x => a +ᵥ x) b)) • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Proof state:
α : Type u_5
β : Type u_6
inst✝¹ : AddGroup α
a : α
inst✝ : AddAction α β
b : β
k : ℤ
⊢ (k % ↑(minimalPeriod (fun x => a +ᵥ x) b)) • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩ = k • ⟨a, ⋯⟩ +ᵥ ⟨b, ⋯⟩

Tactic:
exact Subtype.ext (zsmul_vadd_mod_minimalPeriod a b k)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_rpow (hx : 0 ≤ x) (hxy : x < y) (hz : 0 < z) : x ^ z < y ^ z

Proof state:
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z

Tactic:
rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]

Result:
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z

Proof state:
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z

Tactic:
rcases hx with hx | hx

Result:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z

case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z

Proof state:
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y

Tactic:
rwa [← hx] at hxy

Result:
no goals

Proof state:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z

Tactic:
rw [← hx, zero_rpow (ne_of_gt hz)]

Result:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z

Proof state:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z

Tactic:
exact rpow_pos_of_pos (by rwa [← hx] at hxy) _

Result:
no goals

Proof state:
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z

Tactic:
exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 ≤ x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z

Tactic:
rw [le_iff_eq_or_lt] at hx

Result:
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
-- Mathlib/Order/BoundedOrder/Basic.lean
theorem OrderBot.ext_bot {α} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α}
    (B : OrderBot α) (H : ∀ x y : α, (haveI := hA; x ≤ y) ↔ x ≤ y) :
    (@Bot.bot α (@OrderBot.toBot α hA.toLE A)) = (@Bot.bot α (@OrderBot.toBot α hB.toLE B))

Proof state:
α : Type u_1
hA : PartialOrder α
A : OrderBot α
hB : PartialOrder α
B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥

Tactic:
cases PartialOrder.ext H

Result:
case refl
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥

Proof state:
case refl.h
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ ≤ ⊥

Tactic:
exact @bot_le _ _ A _

Result:
no goals

Proof state:
case refl
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ = ⊥

Tactic:
apply bot_unique

Result:
case refl.h
α : Type u_1
hA : PartialOrder α
A B : OrderBot α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊥ ≤ ⊥
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem Fintype.linearCombination_apply_single [DecidableEq α] (i : α) (r : R) :
    Fintype.linearCombination R S v (Pi.single i r) = r • v i

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁷ : Fintype α
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : SMulCommClass R S M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ ((Fintype.linearCombination R S) v) (Pi.single i r) = r • v i

Tactic:
simp_rw [Fintype.linearCombination_apply, Pi.single_apply, ite_smul, zero_smul]

Result:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁷ : Fintype α
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : SMulCommClass R S M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (∑ x : α, if x = i then r • v x else 0) = r • v i

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁷ : Fintype α
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : SMulCommClass R S M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (∑ x : α, if x = i then r • v x else 0) = r • v i

Tactic:
rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_equivMapOfInjective_symm_apply (f : F) (i : Injective f) (p : Submodule R M)
    (x : p.map f) : f ((equivMapOfInjective f i p).symm x) = x

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
F : Type u_9
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F σ₁₂ M M₂
f : F
i : Injective ⇑f
p : Submodule R M
x : ↥(map f p)
⊢ f ↑((equivMapOfInjective f i p).symm x) = ↑x

Tactic:
rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
  i.eq_iff, LinearEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_eq_iff_natDegree_eq_of_pos {p : R[X]} {n : ℕ} (hn : 0 < n) :
    p.degree = n ↔ p.natDegree = n

Proof state:
case inl
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
⊢ degree 0 = ↑n ↔ natDegree 0 = n

Tactic:
simp [hn.ne]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
exact degree_eq_iff_natDegree_eq h

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
⊢ p.degree = ↑n ↔ p.natDegree = n

Tactic:
obtain rfl|h := eq_or_ne p 0

Result:
case inl
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
⊢ degree 0 = ↑n ↔ natDegree 0 = n

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : 0 < n
h : p ≠ 0
⊢ p.degree = ↑n ↔ p.natDegree = n
-- Mathlib/GroupTheory/Perm/Support.lean
theorem set_support_zpow_subset (n : ℤ) : { x | (p ^ n) x ≠ x } ⊆ { x | p x ≠ x }

Proof state:
α : Type u_1
p : Perm α
n : ℤ
⊢ {x | (p ^ n) x ≠ x} ⊆ {x | p x ≠ x}

Tactic:
intro x

Result:
α : Type u_1
p : Perm α
n : ℤ
x : α
⊢ x ∈ {x | (p ^ n) x ≠ x} → x ∈ {x | p x ≠ x}

Proof state:
α : Type u_1
p : Perm α
n : ℤ
x : α
hx : ¬(p ^ n) x = x
H : p x = x
⊢ False

Tactic:
simp [zpow_apply_eq_self_of_apply_eq_self H] at hx

Result:
no goals

Proof state:
α : Type u_1
p : Perm α
n : ℤ
x : α
⊢ x ∈ {x | (p ^ n) x ≠ x} → x ∈ {x | p x ≠ x}

Tactic:
simp only [Set.mem_setOf_eq, Ne]

Result:
α : Type u_1
p : Perm α
n : ℤ
x : α
⊢ ¬(p ^ n) x = x → ¬p x = x

Proof state:
α : Type u_1
p : Perm α
n : ℤ
x : α
⊢ ¬(p ^ n) x = x → ¬p x = x

Tactic:
intro hx H

Result:
α : Type u_1
p : Perm α
n : ℤ
x : α
hx : ¬(p ^ n) x = x
H : p x = x
⊢ False
-- Mathlib/Data/Multiset/Dedup.lean
theorem le_dedup_self {s : Multiset α} : s ≤ dedup s ↔ Nodup s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s ≤ s.dedup ↔ s.Nodup

Tactic:
rw [le_dedup, and_iff_right le_rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem lt_of_lt_of_le : ∀ {x y z : Bool}, x < y → y ≤ z → x < z

Proof state:
⊢ ∀ {x y z : Bool}, x < y → y ≤ z → x < z

Tactic:
decide

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_add {P Q : Fin 3 → F} (hP : (W'.baseChange F).toProjective.Nonsingular P)
    (hQ : (W'.baseChange F).toProjective.Nonsingular Q) :
    (W'.baseChange K).toProjective.add (f ∘ P) (f ∘ Q) =
      f ∘ (W'.baseChange F).toProjective.add P Q

Proof state:
F : Type u
inst✝¹⁰ : Field F
R : Type r
inst✝⁹ : CommRing R
W' : Projective R
S : Type s
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra S F
inst✝⁴ : IsScalarTower R S F
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (baseChange W' F).toProjective.Nonsingular P
hQ : (baseChange W' F).toProjective.Nonsingular Q
⊢ (baseChange W' K).toProjective.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (baseChange W' F).toProjective.add P Q

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_add f hP hQ (K := K), map_baseChange]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem prod.ext_iff {I I' : Ideal R} {J J' : Ideal S} :
    prod I J = prod I' J' ↔ I = I' ∧ J = J'

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I I' : Ideal R
J J' : Ideal S
⊢ I.prod J = I'.prod J' ↔ I = I' ∧ J = J'

Tactic:
simp only [← idealProdEquiv_symm_apply, idealProdEquiv.symm.injective.eq_iff, Prod.mk.inj_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)}
    (hc : (m.alter k f).contains k') :
    (m.alter k f).get k' hc =
      if heq : k == k' then
        haveI h' : (f (m.get? k)).isSome

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : Option (β k) → Option (β k)
hc : (m.alter k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_alter _ h, if_neg heq] at hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : Option (β k) → Option (β k)
hc : (m.alter k f).contains k' = true
heq : (k == k') = true
⊢ (f (m.get? k)).isSome = true

Tactic:
rwa [contains_alter _ h, if_pos heq] at hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
f : Option (β k) → Option (β k)
hc : (m.alter k f).contains k' = true
⊢ (m.alter k f).get k' hc = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯

Tactic:
simp_to_model [alter] using List.getValueCast_alterKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_9 :
    (coordinate 9).eval
      (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9

Proof state:
a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 : Int
t : List Int
⊢ (coordinate 9).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: a9 :: t)) = a9

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_or_nonempty_inter (s t : Finset α) : Disjoint s t ∨ (s ∩ t).Nonempty

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ ¬Disjoint s t

Tactic:
exact em _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ (s ∩ t).Nonempty

Tactic:
rw [← not_disjoint_iff_nonempty_inter]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ ¬Disjoint s t
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Iic_pred_eq_Iio_of_not_isMin (hb : ¬ IsMin b) : Iic (pred b) = Iio b :=
  coe_injective <| by simpa using Set.Iic_pred_eq_Iio_of_not_isMin hb

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
⊢ ↑(Iic (pred b)) = ↑(Iio b)

Tactic:
simpa using Set.Iic_pred_eq_Iio_of_not_isMin hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_filter {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
    Perm (toListModel (m.filter f).1.buckets)
      ((toListModel m.1.buckets).filter fun p => f p.1 p.2)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
f : (a : α) → β a → Bool
⊢ toListModel (m.filterₘ f).val.buckets ~ List.filter (fun p => f p.fst p.snd) (toListModel m.val.buckets)

Tactic:
exact toListModel_filterₘ

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
f : (a : α) → β a → Bool
⊢ toListModel (filter f m).val.buckets ~ List.filter (fun p => f p.fst p.snd) (toListModel m.val.buckets)

Tactic:
rw [filter_eq_filterₘ]

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
f : (a : α) → β a → Bool
⊢ toListModel (m.filterₘ f).val.buckets ~ List.filter (fun p => f p.fst p.snd) (toListModel m.val.buckets)
-- Mathlib/Topology/UniformSpace/Compact.lean
theorem unique_uniformity_of_compact [t : TopologicalSpace γ] [CompactSpace γ]
    {u u' : UniformSpace γ} (h : u.toTopologicalSpace = t) (h' : u'.toTopologicalSpace = t) :
    u = u'

Proof state:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ CompactSpace γ

Tactic:
rwa [h]

Result:
no goals

Proof state:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ

Tactic:
rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']

Result:
no goals

Proof state:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
⊢ CompactSpace γ

Tactic:
rwa [h']

Result:
no goals

Proof state:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ 𝓤 γ = 𝓤 γ

Tactic:
have : @CompactSpace γ u.toTopologicalSpace := by rwa [h]

Result:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ

Proof state:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ

Tactic:
have : @CompactSpace γ u'.toTopologicalSpace := by rwa [h']

Result:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ

Proof state:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ u = u'

Tactic:
refine UniformSpace.ext ?_

Result:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ 𝓤 γ = 𝓤 γ
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_mapAccumr_right (f₁ : α → γ → σ₁ → σ₁ × ζ) (f₂ : β → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).snd s₁)
    = let m := (mapAccumr₂ (fun x y s =>
          let r₂ := f₂ y s.snd
          let r₁ := f₁ x r₂.snd s.fst
          ((r₁.fst, r₂.fst), r₁.snd)
        ) xs ys (s₁, s₂))
      (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × ζ
f₂ : β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ y s.2;
          let r₁ := f₁ x r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem orthogonalComplement_iSup_eigenspaces_eq_bot (hT : T.IsSymmetric) :
    (⨆ μ, eigenspace T μ)ᗮ = ⊥

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
hT' : (T.restrict ⋯).IsSymmetric
this : Subsingleton ↥(⨆ μ, eigenspace T μ)ᗮ
⊢ (⨆ μ, eigenspace T μ)ᗮ = ⊥

Tactic:
exact Submodule.eq_bot_of_subsingleton

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
hT' : (T.restrict ⋯).IsSymmetric
⊢ (⨆ μ, eigenspace T μ)ᗮ = ⊥

Tactic:
haveI :=
  hT'.subsingleton_of_no_eigenvalue_finiteDimensional hT.orthogonalComplement_iSup_eigenspaces

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
hT' : (T.restrict ⋯).IsSymmetric
this : Subsingleton ↥(⨆ μ, eigenspace T μ)ᗮ
⊢ (⨆ μ, eigenspace T μ)ᗮ = ⊥

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
⊢ (⨆ μ, eigenspace T μ)ᗮ = ⊥

Tactic:
have hT' : IsSymmetric _ :=
  hT.restrict_invariant hT.orthogonalComplement_iSup_eigenspaces_invariant

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
hT' : (T.restrict ⋯).IsSymmetric
⊢ (⨆ μ, eigenspace T μ)ᗮ = ⊥
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
lemma HasFiniteIntegral.restrict (h : HasFiniteIntegral f μ) {s : Set α} :
    HasFiniteIntegral f (μ.restrict s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f : α → E
h : HasFiniteIntegral f μ
s : Set α
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
simpa [Measure.restrict_univ] using lintegral_mono_set (subset_univ s)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f : α → E
h : HasFiniteIntegral f μ
s : Set α
⊢ HasFiniteIntegral f (μ.restrict s)

Tactic:
refine lt_of_le_of_lt ?_ h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f : α → E
h : HasFiniteIntegral f μ
s : Set α
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
-- Mathlib/Data/Matroid/Constructions.lean
theorem loopyOn_isBase_iff : (loopyOn E).IsBase B ↔ B = ∅

Proof state:
α : Type u_1
E B : Set α
⊢ (loopyOn E).IsBase B ↔ B = ∅

Tactic:
simp [Maximal, isBase_iff_maximal_indep]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma opcyclesMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃)
    (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) :
    opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq,
  RightHomologyMapData.comp_φQ]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃

Tactic:
let γ₁ := rightHomologyMapData φ₁ h₁ h₂

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃

Tactic:
let γ₂ := rightHomologyMapData φ₂ h₂ h₃

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_apply_apply_pow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℕ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℕ
⊢ (f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x

Tactic:
convert cycleOf_apply_apply_zpow_self f x k using 1

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
theorem preserves_desc_mapCocone (c₁ c₂ : Cocone F) (t : IsColimit c₁) :
    (isColimitOfPreserves G t).desc (G.mapCocone _) = G.map (t.desc c₂) :=
  ((isColimitOfPreserves G t).uniq (G.mapCocone _) _ (by simp [← G.map_comp])).symm

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesColimit F G
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), (G.mapCocone c₁).ι.app j ≫ G.map (t.desc c₂) = (G.mapCocone c₂).ι.app j

Tactic:
simp [← G.map_comp]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma rightHomologyIso_inv_naturality :
    S₁.rightHomologyIso.inv ≫ rightHomologyMap φ =
      homologyMap φ ≫ S₂.rightHomologyIso.inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.rightHomologyIso.inv ≫ rightHomologyMap φ = homologyMap φ ≫ S₂.rightHomologyIso.inv

Tactic:
simpa only [RightHomologyData.homologyIso_rightHomologyData, Iso.symm_inv] using
  RightHomologyData.rightHomologyIso_hom_naturality φ S₁.rightHomologyData S₂.rightHomologyData

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : v ᵥ* (-A) = - (v ᵥ* A)

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ (v ᵥ* -A) x✝ = (-(v ᵥ* A)) x✝

Tactic:
apply dotProduct_neg

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ v ᵥ* -A = -(v ᵥ* A)

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
x✝ : n
⊢ (v ᵥ* -A) x✝ = (-(v ᵥ* A)) x✝
-- Mathlib/Data/ZMod/Basic.lean
lemma ringEquivCongr_val {a b : ℕ} (h : a = b) (x : ZMod a) :
    ZMod.val ((ZMod.ringEquivCongr h) x) = ZMod.val x

Proof state:
a : ℕ
x : ZMod a
⊢ ((ringEquivCongr ⋯) x).val = x.val

Tactic:
cases a <;> rfl

Result:
no goals

Proof state:
a b : ℕ
h : a = b
x : ZMod a
⊢ ((ringEquivCongr h) x).val = x.val

Tactic:
subst h

Result:
a : ℕ
x : ZMod a
⊢ ((ringEquivCongr ⋯) x).val = x.val