harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem Derivation.liftKaehlerDifferential_comp (D : Derivation R S M) :
    D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D

Proof state:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D.tensorProductTo ↑⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩ = D a

Tactic:
rw [Subtype.coe_mk, map_sub, Derivation.tensorProductTo_tmul, Derivation.tensorProductTo_tmul,
  one_smul, D.map_one_eq_zero, smul_zero, sub_zero]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
⊢ D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D

Tactic:
ext a

Result:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ (D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S)) a = D a

Proof state:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ (D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S)) a = D a

Tactic:
dsimp [KaehlerDifferential.D_apply]

Result:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) = D a

Proof state:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) = D a

Tactic:
refine (D.liftKaehlerDifferential_apply _).trans ?_

Result:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D.tensorProductTo ↑⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩ = D a
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_smul {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R]
    (s : S) (p : R[X]) (k : ℕ) : derivative^[k] (s • p) = s • derivative^[k] p

Proof state:
R : Type u
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p

Tactic:
induction k generalizing p with
| zero => simp
| succ k ih => simp [ih]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
⊢ (⇑derivative)^[0] (s • p) = s • (⇑derivative)^[0] p

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
inst✝³ : Semiring R
S : Type u_1
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative)^[k] (s • p) = s • (⇑derivative)^[k] p
p : R[X]
⊢ (⇑derivative)^[k + 1] (s • p) = s • (⇑derivative)^[k + 1] p

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma iUnion₂_inter_iUnion₂ {ι₁ κ₁ : Sort*} {ι₂ : ι₁ → Sort*} {k₂ : κ₁ → Sort*}
    (f : ∀ i₁, ι₂ i₁ → Set α) (g : ∀ j₁, k₂ j₁ → Set α) :
    (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂

Proof state:
α : Type u_1
ι₁ : Sort u_12
κ₁ : Sort u_13
ι₂ : ι₁ → Sort u_14
k₂ : κ₁ → Sort u_15
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂

Tactic:
simp_rw [iUnion_inter, inter_iUnion]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem IsCyclic.exists_monoid_generator [Finite α] [IsCyclic α] :
    ∃ x : α, ∀ y : α, y ∈ Submonoid.powers x

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ zpowers x

Tactic:
exact IsCyclic.exists_generator

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ Submonoid.powers x

Tactic:
simp_rw [mem_powers_iff_mem_zpowers]

Result:
α : Type u_1
inst✝² : Group α
inst✝¹ : Finite α
inst✝ : IsCyclic α
⊢ ∃ x, ∀ (y : α), y ∈ zpowers x
-- Mathlib/Order/CompleteLattice.lean
theorem biSup_le_eq_sup : (⨆ j ≤ i, f j) = (⨆ j < i, f j) ⊔ f i

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≤ i), f j = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
rw [iSup_split_single _ i]

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≤ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≤ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
simp only [le_refl, iSup_pos, iSup_and', lt_iff_le_and_ne, and_comm, sup_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.xor_left_inj' (a b c : BitVec w) : (a ^^^ c == c ^^^ b) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == b ^^^ c) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == c ^^^ b) = (a == b)

Tactic:
rw [Bool.eq_iff_iff, BitVec.xor_comm c]

Result:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == b ^^^ c) = true ↔ (a == b) = true
-- Mathlib/RingTheory/Noetherian/Defs.lean
theorem monotone_stabilizes_iff_noetherian :
    (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M

Tactic:
rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Box.lean
@[simp] lemma zero_mem_box : (0 : α) ∈ box n ↔ n = 0

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
⊢ 0 ∈ box n ↔ n = 0

Tactic:
cases n <;> simp [box_succ_eq_sdiff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Sub.lean
theorem sub_eq_zero_of_le (h : μ ≤ ν) : μ - ν = 0 :=
  nonpos_iff_eq_zero'.1 <| sub_le_of_le_add <| by rwa [zero_add]

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≤ ν
⊢ μ ≤ 0 + ν

Tactic:
rwa [zero_add]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
/-- If `t` is a non-empty open subset of `H`,
every chart of `t` is the restriction of some chart on `H`. -/
-- XXX: can I unify this with `chart_eq`?
lemma chart_eq' {t : Opens H} (ht : Nonempty t) {e' : PartialHomeomorph t H}
    (he' : e' ∈ atlas H t) : ∃ x : t, e' = (chartAt H ↑x).subtypeRestr ht

Proof state:
H : Type u
inst✝ : TopologicalSpace H
t : Opens H
ht : Nonempty ↥t
e' : PartialHomeomorph (↥t) H
he' : e' ∈ atlas H ↥t
⊢ ∃ x, e' = (chartAt H ↑x).subtypeRestr ht

Tactic:
rcases he' with ⟨xset, ⟨x, hx⟩, he'⟩

Result:
case intro.intro.intro
H : Type u
inst✝ : TopologicalSpace H
t : Opens H
ht : Nonempty ↥t
e' : PartialHomeomorph (↥t) H
xset : Set (PartialHomeomorph (↥t) H)
he' : e' ∈ xset
x : ↥t
hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ ∃ x, e' = (chartAt H ↑x).subtypeRestr ht

Proof state:
H : Type u
inst✝ : TopologicalSpace H
t : Opens H
ht : Nonempty ↥t
e' : PartialHomeomorph (↥t) H
xset : Set (PartialHomeomorph (↥t) H)
he' : e' ∈ xset
x : ↥t
hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ e' ∈ {(chartAt H ↑x).subtypeRestr ht}

Tactic:
convert he'

Result:
no goals

Proof state:
case intro.intro.intro
H : Type u
inst✝ : TopologicalSpace H
t : Opens H
ht : Nonempty ↥t
e' : PartialHomeomorph (↥t) H
xset : Set (PartialHomeomorph (↥t) H)
he' : e' ∈ xset
x : ↥t
hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ ∃ x, e' = (chartAt H ↑x).subtypeRestr ht

Tactic:
exact ⟨x, mem_singleton_iff.mp (by convert he')⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem div_two_le_of_lt_two {m n : Nat} (p : m < 2 ^ succ n) : m / 2 < 2^n

Proof state:
m n : Nat
p : m < 2 ^ n.succ
⊢ m < 2 ^ n * 2

Tactic:
exact p

Result:
no goals

Proof state:
m n : Nat
p : m < 2 ^ n.succ
⊢ m / 2 < 2 ^ n

Tactic:
simp [div_lt_iff_lt_mul Nat.zero_lt_two]

Result:
m n : Nat
p : m < 2 ^ n.succ
⊢ m < 2 ^ n * 2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_reverse (p : α → Bool) (l : List α) : (l.reverse.filter p) = (l.filter p).reverse

Proof state:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : filter p l.reverse = (filter p l).reverse
⊢ filter p (a :: l).reverse = (filter p (a :: l)).reverse

Tactic:
simp only [reverse_cons, filter_append, filter_cons, ih]

Result:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : filter p l.reverse = (filter p l).reverse
⊢ ((filter p l).reverse ++ if p a = true then a :: filter p [] else filter p []) =
    (if p a = true then a :: filter p l else filter p l).reverse

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ filter p l.reverse = (filter p l).reverse

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp only [reverse_cons, filter_append, filter_cons, ih]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
a : α
l : List α
ih : filter p l.reverse = (filter p l).reverse
⊢ ((filter p l).reverse ++ if p a = true then a :: filter p [] else filter p []) =
    (if p a = true then a :: filter p l else filter p l).reverse

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ filter p [].reverse = (filter p []).reverse

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_compl_subset {f : α → β} {s : Set α} (H : Injective f) : f '' sᶜ ⊆ (f '' s)ᶜ :=
  Disjoint.subset_compl_left <| by simp [disjoint_iff_inf_le, ← image_inter H]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
⊢ Disjoint (f '' s) (f '' sᶜ)

Tactic:
simp [disjoint_iff_inf_le, ← image_inter H]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem dropLast_take {n : ℕ} {xs : Stream' α} :
    (Stream'.take n xs).dropLast = Stream'.take (n-1) xs

Proof state:
α : Type u
n : ℕ
xs : Stream' α
⊢ (take n xs).dropLast = take (n - 1) xs

Tactic:
cases n with
| zero => simp
| succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]

Result:
no goals

Proof state:
case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs

Tactic:
rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]

Result:
no goals

Proof state:
case zero
α : Type u
xs : Stream' α
⊢ (take 0 xs).dropLast = take (0 - 1) xs

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem mem_primeFactorsList_mul_left {p a b : ℕ} (hpa : p ∈ a.primeFactorsList) (hb : b ≠ 0) :
    p ∈ (a * b).primeFactorsList

Proof state:
case inr
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
apply (mem_primeFactorsList_mul ha hb).2 (Or.inl hpa)

Result:
no goals

Proof state:
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ primeFactorsList 0
⊢ p ∈ (0 * b).primeFactorsList

case inr
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Proof state:
case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ primeFactorsList 0
⊢ p ∈ (0 * b).primeFactorsList

Tactic:
simp at hpa

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_le_ωSup_of_le {c₀ c₁ : Chain α} (h : c₀ ≤ c₁) : ωSup c₀ ≤ ωSup c₁ :=
  (ωSup_le _ _) fun i => by
    obtain ⟨_, h⟩ := h i
    exact le_trans h (le_ωSup _ _)

Proof state:
case intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h✝ : c₀ ≤ c₁
i w✝ : ℕ
h : c₀ i ≤ c₁ w✝
⊢ c₀ i ≤ ωSup c₁

Tactic:
exact le_trans h (le_ωSup _ _)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h : c₀ ≤ c₁
i : ℕ
⊢ c₀ i ≤ ωSup c₁

Tactic:
obtain ⟨_, h⟩ := h i

Result:
case intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h✝ : c₀ ≤ c₁
i w✝ : ℕ
h : c₀ i ≤ c₁ w✝
⊢ c₀ i ≤ ωSup c₁
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_zero : ghostFun (0 : 𝕎 R) = 0

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ WittVector.ghostFun 0 = 0

Tactic:
ghost_fun_tac 0, ![]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToIso_map_trans (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
    F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso <| p.trans q)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
p : X = Y
q : Y = Z
⊢ F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso ⋯)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_emod {a b : Int} : -a % b = (b - a) % b

Proof state:
a b : Int
⊢ -a % b = (b - a) % b

Tactic:
rw [← add_emod_self_left]

Result:
a b : Int
⊢ (b + -a) % b = (b - a) % b

Proof state:
a b : Int
⊢ (b + -a) % b = (b - a) % b

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem le_iff_le (x : K) (r : ℝ) : (∀ w : InfinitePlace K, w x ≤ r) ↔ ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r :=
  ⟨fun hw φ => hw (mk φ), by rintro hφ ⟨w, ⟨φ, rfl⟩⟩; exact hφ φ⟩

Proof state:
case mk.intro
K : Type u_2
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x ≤ r

Tactic:
exact hφ φ

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
x : K
r : ℝ
⊢ (∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r) → ∀ (w : InfinitePlace K), w x ≤ r

Tactic:
rintro hφ ⟨w, ⟨φ, rfl⟩⟩

Result:
case mk.intro
K : Type u_2
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x ≤ r
-- Mathlib/Data/Bool/Basic.lean
lemma eq_or_eq_not : ∀ a b, a = b ∨ a = !b

Proof state:
⊢ ∀ (a b : Bool), a = b ∨ a = !b

Tactic:
decide

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.subtypeCongr.right_apply {a : ε} (h : ¬p a) : ep.subtypeCongr en a = en ⟨a, h⟩

Proof state:
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : ¬p a
⊢ (ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)

Tactic:
simp [Perm.subtypeCongr.apply, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_map {f : α → β} {g : β → γ} {as : Array α} :
    (as.map f).map g = as.map (g ∘ f)

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
toList✝ : List α
⊢ map g (map f { toList := toList✝ }) = map (g ∘ f) { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
as : Array α
⊢ map g (map f as) = map (g ∘ f) as

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
toList✝ : List α
⊢ map g (map f { toList := toList✝ }) = map (g ∘ f) { toList := toList✝ }
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem zero_left (X : C) : IsPushout (0 : 0 ⟶ X) (0 : (0 : C) ⟶ 0) (𝟙 X) (0 : 0 ⟶ X) :=
  of_iso_pushout (by simp) ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso _ _).symm) (by simp)
    (by simp [eq_iff_true_of_subsingleton])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 0 ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inr 0 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ 𝟙 X ≫ ((coprodZeroIso X).symm ≪≫ (pushoutZeroZeroIso X 0).symm).hom = pushout.inl 0 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 0 (𝟙 X) 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_sub (y1 y2 : HomogeneousLocalization 𝒜 x) : (y1 - y2).val = y1.val - y2.val

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = y1.val - y2.val

Tactic:
rw [sub_eq_add_neg, ← val_neg, ← val_add]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = (y1 + -y2).val

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : HomogeneousLocalization 𝒜 x
⊢ (y1 - y2).val = (y1 + -y2).val

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
lemma neg_pi_div_two_lt_arg_iff {z : ℂ} : -(π / 2) < arg z ↔ 0 < re z ∨ 0 ≤ im z

Proof state:
z : ℂ
⊢ -(π / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
rw [lt_iff_le_and_ne, neg_pi_div_two_le_arg_iff, ne_comm, Ne, arg_eq_neg_pi_div_two_iff]

Result:
z : ℂ
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Proof state:
case inr.inl
z : ℂ
hre : z.re = 0
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
simp [hre]

Result:
no goals

Proof state:
z : ℂ
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
rcases lt_trichotomy z.re 0 with hre | hre | hre

Result:
case inl
z : ℂ
hre : z.re < 0
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

case inr.inl
z : ℂ
hre : z.re = 0
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Proof state:
case inl
z : ℂ
hre : z.re < 0
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
simp [hre.ne, hre.not_le, hre.not_lt]

Result:
no goals

Proof state:
case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
simp [hre, hre.le, hre.ne']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_mkArray_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
    (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b

Proof state:
α : Type u_1
n : Nat
a b : α
p : α → Bool
⊢ find? p (mkArray n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

Tactic:
simp [← List.toArray_replicate]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma zpow_ne_zero {a : G₀} : ∀ n : ℤ, a ≠ 0 → a ^ n ≠ 0
  | (_ : ℕ) => by rw [zpow_natCast]; exact pow_ne_zero _
  | .negSucc n => fun ha ↦ by rw [zpow_negSucc]; exact inv_ne_zero (pow_ne_zero _ ha)

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ a ^ Int.negSucc n ≠ 0

Tactic:
rw [zpow_negSucc]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ (a ^ (n + 1))⁻¹ ≠ 0

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ a✝ ≠ 0

Tactic:
exact pow_ne_zero _

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ ↑a✝ ≠ 0

Tactic:
rw [zpow_natCast]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ a✝ ≠ 0

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ (a ^ (n + 1))⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (pow_ne_zero _ ha)

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem self_comp_sort (f : Fin n → α) : f ∘ sort f = graph.proj ∘ graphEquiv₂ f :=
  show graph.proj ∘ (graphEquiv₁ f ∘ (graphEquiv₁ f).symm) ∘ (graphEquiv₂ f).toEquiv = _ by simp

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ graph.proj ∘ (⇑(graphEquiv₁ f) ∘ ⇑(graphEquiv₁ f).symm) ∘ ⇑(graphEquiv₂ f).toEquiv = graph.proj ∘ ⇑(graphEquiv₂ f)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/LocallyFinite.lean
theorem closure_iUnion (h : LocallyFinite f) : closure (⋃ i, f i) = ⋃ i, closure (f i)

Proof state:
case h
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
x : X
⊢ x ∈ closure (⋃ i, f i) ↔ x ∈ ⋃ i, closure (f i)

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
⊢ closure (⋃ i, f i) = ⋃ i, closure (f i)

Tactic:
ext x

Result:
case h
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
x : X
⊢ x ∈ closure (⋃ i, f i) ↔ x ∈ ⋃ i, closure (f i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z

Proof state:
case zero
x y : Nat
H : 0 < y
⊢ (x + y * 0) / y = x / y + 0

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

Result:
no goals

Proof state:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ x / y + z + 1 = x / y + (z + 1)

Tactic:
rfl

Result:
no goals

Proof state:
x z y : Nat
H : 0 < y
⊢ (x + y * z) / y = x / y + z

Tactic:
induction z with
| zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
| succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl

Result:
no goals

Proof state:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ (x + y * (z + 1)) / y = x / y + (z + 1)

Tactic:
rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]

Result:
case succ
x y : Nat
H : 0 < y
z : Nat
ih : (x + y * z) / y = x / y + z
⊢ x / y + z + 1 = x / y + (z + 1)
-- Mathlib/CategoryTheory/Sites/CoverPreserving.lean
theorem idCoverPreserving : CoverPreserving J J (𝟭 _) :=
  ⟨fun hS => by simpa using hS⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ J U✝
⊢ Sieve.functorPushforward (𝟭 C) S✝ ∈ J ((𝟭 C).obj U✝)

Tactic:
simpa using hS

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem sin_arctan (x : ℝ) : sin (arctan x) = x / √(1 + x ^ 2)

Proof state:
x : ℝ
⊢ sin (arctan x) = x / √(1 + x ^ 2)

Tactic:
rw_mod_cast [← tan_div_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_subset (hs : s ⊆ s') (ht : t ⊆ t') : image₂ f s t ⊆ image₂ f s' t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f ↑s ↑t ⊆ image2 f ↑s' ↑t'

Tactic:
exact image2_subset hs ht

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image₂ f s t ⊆ image₂ f s' t'

Tactic:
rw [← coe_subset, coe_image₂, coe_image₂]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f ↑s ↑t ⊆ image2 f ↑s' ↑t'