harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finsupp/Basic.lean
theorem equivMapDomain_trans' (f : α ≃ β) (g : β ≃ γ) :
    @equivMapDomain _ _ M _ (f.trans g) = equivMapDomain g ∘ equivMapDomain f

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
x : α →₀ M
a✝ : γ
⊢ (equivMapDomain (f.trans g) x) a✝ = ((equivMapDomain g ∘ equivMapDomain f) x) a✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
⊢ equivMapDomain (f.trans g) = equivMapDomain g ∘ equivMapDomain f

Tactic:
ext x

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
x : α →₀ M
a✝ : γ
⊢ (equivMapDomain (f.trans g) x) a✝ = ((equivMapDomain g ∘ equivMapDomain f) x) a✝
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm (w z : ℂ) : Complex.orientation.areaForm w z = (conj w * z).im

Proof state:
w z : ℂ
⊢ (Complex.orientation.areaForm w) z = ((starRingEnd ℂ) w * z).im

Tactic:
let o := Complex.orientation

Result:
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ (Complex.orientation.areaForm w) z = ((starRingEnd ℂ) w * z).im

Proof state:
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re

Tactic:
ring

Result:
no goals

Proof state:
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ (Complex.orientation.areaForm w) z = ((starRingEnd ℂ) w * z).im

Tactic:
simp only [o, o.areaForm_to_volumeForm,
  o.volumeForm_robust Complex.orthonormalBasisOneI rfl, Basis.det_apply, Matrix.det_fin_two,
  Basis.toMatrix_apply, toBasis_orthonormalBasisOneI, Matrix.cons_val_zero, coe_basisOneI_repr,
  Matrix.cons_val_one, Matrix.head_cons, mul_im, conj_re, conj_im]

Result:
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt.dest {a b : Int} (h : a < b) : ∃ n : Nat, a + Nat.succ n = b :=
  let ⟨n, h⟩ := le.dest h; ⟨n, by rwa [Int.add_comm, Int.add_left_comm] at h⟩

Proof state:
a b : Int
h✝ : a < b
n : Nat
h : a + 1 + ↑n = b
⊢ a + ↑n.succ = b

Tactic:
rwa [Int.add_comm, Int.add_left_comm] at h

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem eq_one_or_norm_pos (a : E) : a = 1 ∨ 0 < ‖a‖

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ a = 1 ∨ 0 < ‖a‖

Tactic:
simpa [eq_comm] using (norm_nonneg' a).eq_or_lt

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edgeSet_sdiff : (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet

Proof state:
case h.mk.mk
V : Type u
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ \ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet \ G₂.edgeSet

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet

Tactic:
ext ⟨x, y⟩

Result:
case h.mk.mk
V : Type u
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ \ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet \ G₂.edgeSet
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma pow_dvd_sub_pow_of_pow_eq_zero_left (hp : n + m ≤ p + 1) (h_comm : Commute x y)
    (hx : x ^ n = 0) : y ^ m ∣ (x - y) ^ p

Proof state:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (y - x) ^ p

Tactic:
exact h_comm.symm.pow_dvd_sub_pow_of_pow_eq_zero_right hp hx

Result:
no goals

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (y - x) ^ p * (-1) ^ p

Tactic:
apply dvd_mul_of_dvd_left

Result:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (y - x) ^ p

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (x - y) ^ p

Tactic:
rw [← neg_sub y x, neg_pow']

Result:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ y ^ m ∣ (y - x) ^ p * (-1) ^ p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWithAll_map {μ} (f : Option γ → Option δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
    zipWithAll f (l₁.map g) (l₂.map h) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂

Proof state:
γ : Type u_1
δ : Type u_2
α : Type u_1
β : Type u_2
μ : Type u_3
f : Option γ → Option δ → μ
g : α → γ
h : β → δ
l₁ : List α
l₂ : List β
⊢ zipWithAll f (map g l₁) (map h l₂) = zipWithAll (fun a b => f (g <$> a) (h <$> b)) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
/-- See `csSup_mem_of_not_isSuccPrelimit` for the `ConditionallyCompleteLinearOrder` version. -/
lemma csSup_mem_of_not_isSuccPrelimit'
    (hbdd : BddAbove s) (hlim : ¬ IsSuccPrelimit (sSup s)) : sSup s ∈ s

Proof state:
case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s

Tactic:
exact csSup_mem_of_not_isSuccPrelimit hs hbdd hlim

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
hbdd : BddAbove ∅
hlim : ¬IsSuccPrelimit (sSup ∅)
⊢ sSup ∅ ∈ ∅

Tactic:
simp [isSuccPrelimit_bot] at hlim

Result:
no goals

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
hbdd : BddAbove ∅
hlim : ¬IsSuccPrelimit (sSup ∅)
⊢ sSup ∅ ∈ ∅

case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hbdd : BddAbove s
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
@[simp] lemma sinKernel_zero (x : ℝ) : sinKernel 0 x = 0

Proof state:
x : ℝ
⊢ sinKernel 0 x = 0

Tactic:
simpa using sinKernel_neg 0 x

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem le_inf_support_multiset_prod (degt0 : 0 ≤ degt 0)
    (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (m : Multiset R[A]) :
    (m.map fun f : R[A] => f.support.inf degt).sum ≤ m.prod.support.inf degt

Proof state:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0

Tactic:
exact degt0

Result:
no goals

Proof state:
case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)

Tactic:
exact degtm _ _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
⊢ (Multiset.map (fun f => f.support.inf degt) m).sum ≤ m.prod.support.inf degt

Tactic:
refine OrderDual.ofDual_le_ofDual.mpr <|
  sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp ?_)
    (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m

Result:
case refine_1
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
⊢ OrderDual.ofDual (degt 0) ≤ OrderDual.ofDual 0

case refine_2
R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ OrderDual.ofDual (degt (a + b)) ≤ OrderDual.ofDual (degt a + degt b)
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_psum {α β} : IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

Proof state:
α : Sort u_4
β : Sort u_5
⊢ IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_psum, not_or]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem zero_smul (x : M ⊗[R] N) : (0 : R'') • x = 0 :=
  have : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  x.induction_on (by rw [TensorProduct.smul_zero])
    (fun m n => by rw [this, zero_smul, zero_tmul]) fun x y ihx ihy => by
    rw [TensorProduct.smul_add, ihx, ihy, add_zero]

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 0 • 0 = 0

Tactic:
rw [TensorProduct.smul_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
m : M
n : N
⊢ 0 • m ⊗ₜ[R] n = 0

Tactic:
rw [this, zero_smul, zero_tmul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R'' : Type u_3
inst✝⁶ : Semiring R''
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R'' M
inst✝ : SMulCommClass R R'' M
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 0 • x = 0
ihy : 0 • y = 0
⊢ 0 • (x + y) = 0

Tactic:
rw [TensorProduct.smul_add, ihx, ihy, add_zero]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem comp_left_id (r : Rel α β) : @Eq α • r = r

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
x : α
x✝ : β
⊢ (∃ y, x = y ∧ r y x✝) ↔ r x x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ Eq • r = r

Tactic:
unfold comp

Result:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (fun x z => ∃ y, x = y ∧ r y z) = r

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ (fun x z => ∃ y, x = y ∧ r y z) = r

Tactic:
ext x

Result:
case a.h.a
α : Type u_1
β : Type u_2
r : Rel α β
x : α
x✝ : β
⊢ (∃ y, x = y ∧ r y x✝) ↔ r x x✝
-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean
@[ext]
lemma DoubleCentralizer.ext (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜]
    [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A]
    (a b : 𝓜(𝕜, A)) (h : a.toProd = b.toProd) : a = b

Proof state:
case mk.mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
toProd✝¹ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝¹ : ∀ (x y : A), toProd✝¹.2 x * y = x * toProd✝¹.1 y
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), toProd✝.2 x * y = x * toProd✝.1 y
h : { toProd := toProd✝¹, central := central✝¹ }.toProd = { toProd := toProd✝, central := central✝ }.toProd
⊢ { toProd := toProd✝¹, central := central✝¹ } = { toProd := toProd✝, central := central✝ }

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
b : 𝓜(𝕜, A)
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), toProd✝.2 x * y = x * toProd✝.1 y
h : { toProd := toProd✝, central := central✝ }.toProd = b.toProd
⊢ { toProd := toProd✝, central := central✝ } = b

Tactic:
cases b

Result:
case mk.mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
toProd✝¹ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝¹ : ∀ (x y : A), toProd✝¹.2 x * y = x * toProd✝¹.1 y
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), toProd✝.2 x * y = x * toProd✝.1 y
h : { toProd := toProd✝¹, central := central✝¹ }.toProd = { toProd := toProd✝, central := central✝ }.toProd
⊢ { toProd := toProd✝¹, central := central✝¹ } = { toProd := toProd✝, central := central✝ }

Proof state:
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a b : 𝓜(𝕜, A)
h : a.toProd = b.toProd
⊢ a = b

Tactic:
cases a

Result:
case mk
𝕜 : Type u
A : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
b : 𝓜(𝕜, A)
toProd✝ : (A →L[𝕜] A) × (A →L[𝕜] A)
central✝ : ∀ (x y : A), toProd✝.2 x * y = x * toProd✝.1 y
h : { toProd := toProd✝, central := central✝ }.toProd = b.toProd
⊢ { toProd := toProd✝, central := central✝ } = b
-- Mathlib/CategoryTheory/Limits/Lattice.lean
theorem pushout_eq_sup [SemilatticeSup α] [OrderBot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y) :
    pushout f g = x ⊔ y :=
  calc
    pushout f g = colimit (span f g) := rfl
    _ = Finset.univ.sup (span f g).obj

Proof state:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ colimit (span f g) = Finset.univ.sup (span f g).obj

Tactic:
rw [finite_colimit_eq_finset_univ_sup]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y z : α
f : z ⟶ x
g : z ⟶ y
⊢ z ⊔ (x ⊔ (y ⊔ ⊥)) = z ⊔ (x ⊔ y)

Tactic:
rw [sup_bot_eq]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[simp]
lemma cochainsMap_id_f_eq_compLeft {A B : Rep k G} (f : A ⟶ B) (i : ℕ) :
    (cochainsMap (MonoidHom.id G) f).f i = ModuleCat.ofHom (f.hom.hom.compLeft _)

Proof state:
case hf.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
i : ℕ
x✝ : ↑((inhomogeneousCochains A).X i)
⊢ (ModuleCat.Hom.hom ((cochainsMap (MonoidHom.id G) f).f i)) x✝ =
    (ModuleCat.Hom.hom (ModuleCat.ofHom ((ModuleCat.Hom.hom f.hom).compLeft (Fin i → G)))) x✝

Tactic:
rfl

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
i : ℕ
⊢ (cochainsMap (MonoidHom.id G) f).f i = ModuleCat.ofHom ((ModuleCat.Hom.hom f.hom).compLeft (Fin i → G))

Tactic:
ext

Result:
case hf.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
i : ℕ
x✝ : ↑((inhomogeneousCochains A).X i)
⊢ (ModuleCat.Hom.hom ((cochainsMap (MonoidHom.id G) f).f i)) x✝ =
    (ModuleCat.Hom.hom (ModuleCat.ofHom ((ModuleCat.Hom.hom f.hom).compLeft (Fin i → G)))) x✝
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem subset_le_of_restrict_le_restrict {i : Set α} (hi : MeasurableSet i) (hi₂ : v ≤[i] w)
    {j : Set α} (hj : j ⊆ i) : v j ≤ w j

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ ↑v j ≤ ↑w j

Tactic:
exact (restrict_le_restrict_iff _ _ hi).1 hi₂ hj₁ hj

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ ↑v j ≤ ↑w j

Tactic:
rw [v.not_measurable hj₁, w.not_measurable hj₁]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
⊢ ↑v j ≤ ↑w j

Tactic:
by_cases hj₁ : MeasurableSet j

Result:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : MeasurableSet j
⊢ ↑v j ≤ ↑w j

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
hi₂ : v ≤[i] w
j : Set α
hj : j ⊆ i
hj₁ : ¬MeasurableSet j
⊢ ↑v j ≤ ↑w j
-- Mathlib/Data/Sum/Interval.lean
lemma Icc_inl_inl :
    Icc (inlₗ a₁ : α ⊕ₗ β) (inlₗ a₂) = (Icc a₁ a₂).map (Embedding.inl.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Icc a₁ a₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ a₂ : α
⊢ Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIdempotentElemEquivClopens_symm_bot :
    isIdempotentElemEquivClopens.symm ⊥ = ⟨(0 : R), .zero⟩ :=
  isIdempotentElemEquivClopens.symm_apply_eq.mpr <| Clopens.ext <| by
    rw [coe_isIdempotentElemEquivClopens_apply, basicOpen_zero]; rfl

Proof state:
R : Type u
inst✝ : CommRing R
⊢ ↑⊥ = ↑⊥

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
⊢ ↑⊥ = ↑(isIdempotentElemEquivClopens ⟨0, ⋯⟩)

Tactic:
rw [coe_isIdempotentElemEquivClopens_apply, basicOpen_zero]

Result:
R : Type u
inst✝ : CommRing R
⊢ ↑⊥ = ↑⊥
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.one_right (a : ℕ) : jacobiSymNat a 1 = 1

Proof state:
a : ℕ
⊢ jacobiSymNat a 1 = 1

Tactic:
rw [jacobiSymNat, jacobiSym.one_right]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_smul_span : Ideal.span S • span R T = span R (⋃ (s ∈ S) (t ∈ T), {s • t})

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set R
T : Set M
⊢ Ideal.span S • span R T = span R (⋃ s ∈ S, ⋃ t ∈ T, {s • t})

Tactic:
rw [smul_eq_map₂]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set R
T : Set M
⊢ map₂ (LinearMap.lsmul R M) (Ideal.span S) (span R T) = span R (⋃ s ∈ S, ⋃ t ∈ T, {s • t})

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set R
T : Set M
⊢ map₂ (LinearMap.lsmul R M) (Ideal.span S) (span R T) = span R (⋃ s ∈ S, ⋃ t ∈ T, {s • t})

Tactic:
exact (map₂_span_span _ _ _ _).trans <| congr_arg _ <| Set.image2_eq_iUnion _ _ _

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getElem?_getD_replicate_default_eq (r n : ℕ) : (replicate r d)[n]?.getD d = d

Proof state:
case zero
α : Type u
d : α
n : ℕ
⊢ (replicate 0 d)[n]?.getD d = d

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
d : α
r n : ℕ
⊢ (replicate r d)[n]?.getD d = d

Tactic:
induction r generalizing n with
| zero => simp
| succ n ih => simp at ih; cases n <;> simp [ih, replicate_succ]

Result:
no goals

Proof state:
case succ
α : Type u
d : α
n✝ : ℕ
ih : ∀ (n : ℕ), (replicate n✝ d)[n]?.getD d = d
n : ℕ
⊢ (replicate (n✝ + 1) d)[n]?.getD d = d

Tactic:
cases n <;> simp [ih, replicate_succ]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_pow : ∀ n : ℕ, τ (f ^ n) = n * τ f
  | 0 => by simp
  | n + 1 => by
    rw [pow_succ, translationNumber_mul_of_commute (Commute.pow_self f n),
      translationNumber_pow n, Nat.cast_add_one, add_mul, one_mul]

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ (n + 1)) = ↑(n + 1) * τ f

Tactic:
rw [pow_succ, translationNumber_mul_of_commute (Commute.pow_self f n),
  translationNumber_pow n, Nat.cast_add_one, add_mul, one_mul]

Result:
no goals

Proof state:
f : CircleDeg1Lift
⊢ τ (f ^ 0) = ↑0 * τ f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toMultiset_sup [DecidableEq α] (f g : α →₀ ℕ) :
    toMultiset (f ⊔ g) = toMultiset f ∪ toMultiset g

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ Multiset.count a✝ (toMultiset (f ⊔ g)) = Multiset.count a✝ (toMultiset f ∪ toMultiset g)

Tactic:
simp_rw [Multiset.count_union, Finsupp.count_toMultiset, Finsupp.sup_apply]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
⊢ toMultiset (f ⊔ g) = toMultiset f ∪ toMultiset g

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ Multiset.count a✝ (toMultiset (f ⊔ g)) = Multiset.count a✝ (toMultiset f ∪ toMultiset g)
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_ball_comm : x ∈ ball y ε ↔ y ∈ ball x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ ball y ε ↔ y ∈ ball x ε

Tactic:
rw [mem_ball', mem_ball]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_sup_shrink_equiv {s : Set Ordinal.{u}} (hs : Small.{u} s) (a) (ha : a ∈ s) :
    a ≤ sup.{u, u} fun x => ((@equivShrink s hs).symm x).val

Proof state:
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ s
⊢ a ≤ sup fun x => ↑((equivShrink ↑s).symm x)

Tactic:
convert le_sup.{u, u} (fun x => ((@equivShrink s hs).symm x).val) ((@equivShrink s hs) ⟨a, ha⟩)

Result:
case h.e'_3
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ s
⊢ a = ↑((equivShrink ↑s).symm ((equivShrink ↑s) ⟨a, ha⟩))

Proof state:
case h.e'_3
s : Set Ordinal.{u}
hs : Small.{u, u + 1} ↑s
a : Ordinal.{u}
ha : a ∈ s
⊢ a = ↑((equivShrink ↑s).symm ((equivShrink ↑s) ⟨a, ha⟩))

Tactic:
rw [symm_apply_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Basic.lean
theorem comp_mul [Mul M] [CommSemigroup N] [CommSemigroup P] (g : N →ₙ* P) (f₁ f₂ : M →ₙ* N) :
    g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Proof state:
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
⊢ g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂

Tactic:
ext

Result:
case h
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝

Proof state:
case h
M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝

Tactic:
simp only [mul_apply, Function.comp_apply, map_mul, coe_comp]

Result:
no goals