harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.matrix_π (m : ∀ j k, f j ⟶ g k) (k : K) :
    biproduct.matrix m ≫ biproduct.π g k = biproduct.desc fun j => m j k

Proof state:
case w
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
j✝ : J
⊢ ι f j✝ ≫ matrix m ≫ π g k = ι f j✝ ≫ desc fun j => m j k

Tactic:
simp [biproduct.matrix]

Result:
no goals

Proof state:
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
⊢ matrix m ≫ π g k = desc fun j => m j k

Tactic:
ext

Result:
case w
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
k : K
j✝ : J
⊢ ι f j✝ ≫ matrix m ≫ π g k = ι f j✝ ≫ desc fun j => m j k
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_filter (l : Array α) :
    countP p (filter q l) = countP (fun a => p a && q a) l

Proof state:
case mk
α : Type u_1
p q : α → Bool
toList✝ : List α
⊢ countP p (filter q { toList := toList✝ }) = countP (fun a => p a && q a) { toList := toList✝ }

Tactic:
simp [List.countP_filter]

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
l : Array α
⊢ countP p (filter q l) = countP (fun a => p a && q a) l

Tactic:
cases l

Result:
case mk
α : Type u_1
p q : α → Bool
toList✝ : List α
⊢ countP p (filter q { toList := toList✝ }) = countP (fun a => p a && q a) { toList := toList✝ }
-- Mathlib/Data/ZMod/Basic.lean
theorem ker_intCastAddHom (n : ℕ) :
    (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples (n : ℤ)

Proof state:
n : ℕ
⊢ (Int.castAddHom (ZMod n)).ker = AddSubgroup.zmultiples ↑n

Tactic:
ext

Result:
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ (Int.castAddHom (ZMod n)).ker ↔ x✝ ∈ AddSubgroup.zmultiples ↑n

Proof state:
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ (Int.castAddHom (ZMod n)).ker ↔ x✝ ∈ AddSubgroup.zmultiples ↑n

Tactic:
rw [Int.mem_zmultiples_iff, AddMonoidHom.mem_ker, Int.coe_castAddHom,
  intCast_zmod_eq_zero_iff_dvd]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIdempotentElemEquivClopens_one_sub (e : {e : R | IsIdempotentElem e}) :
    isIdempotentElemEquivClopens ⟨_, e.2.one_sub⟩ = (isIdempotentElemEquivClopens e)ᶜ :=
  SetLike.ext' <| by
    simp_rw [Clopens.coe_compl, coe_isIdempotentElemEquivClopens_apply]
    rw [basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_of_isIdempotentElem _ e.2]

Proof state:
R : Type u
inst✝ : CommRing R
e : ↑{e | IsIdempotentElem e}
⊢ ↑(isIdempotentElemEquivClopens ⟨1 - ↑e, ⋯⟩) = ↑(isIdempotentElemEquivClopens e)ᶜ

Tactic:
simp_rw [Clopens.coe_compl, coe_isIdempotentElemEquivClopens_apply]

Result:
R : Type u
inst✝ : CommRing R
e : ↑{e | IsIdempotentElem e}
⊢ ↑(basicOpen (1 - ↑e)) = (↑(basicOpen ↑e))ᶜ

Proof state:
R : Type u
inst✝ : CommRing R
e : ↑{e | IsIdempotentElem e}
⊢ ↑(basicOpen (1 - ↑e)) = (↑(basicOpen ↑e))ᶜ

Tactic:
rw [basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_of_isIdempotentElem _ e.2]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_self {x : V} (hx : x ≠ 0) : angle x x = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ arccos (inner x x / (‖x‖ * ‖x‖)) = 0

Tactic:
rw [← real_inner_self_eq_norm_mul_norm, div_self (inner_self_ne_zero.2 hx : ⟪x, x⟫ ≠ 0),
  Real.arccos_one]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle x x = 0

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ arccos (inner x x / (‖x‖ * ‖x‖)) = 0
-- Mathlib/Logic/Equiv/Basic.lean
theorem update_comp_equiv [DecidableEq α'] [DecidableEq α] (f : α → β)
    (g : α' ≃ α) (a : α) (v : β) :
    update f a v ∘ g = update (f ∘ g) (g.symm a) v

Proof state:
α : Sort u_1
β : Sort u_4
α' : Sort u_9
inst✝¹ : DecidableEq α'
inst✝ : DecidableEq α
f : α → β
g : α' ≃ α
a : α
v : β
⊢ update f a v ∘ ⇑g = update (f ∘ ⇑g) (g.symm a) v

Tactic:
rw [← update_comp_eq_of_injective _ g.injective, g.apply_symm_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Defs.lean
theorem mk_eq_zero : (mk x : M ⧸ p) = 0 ↔ x ∈ p

Proof state:
R : Type u_1
M : Type u_2
x : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ mk x = 0 ↔ x ∈ p

Tactic:
simpa using (Quotient.eq' p : mk x = 0 ↔ _)

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_inter_right [DecidableEq β] (hf : Injective2 f) :
    image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t' :=
  coe_injective <| by
    push_cast
    exact image2_inter_right hf

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
hf : Injective2 f
⊢ ↑(image₂ f s (t ∩ t')) = ↑(image₂ f s t ∩ image₂ f s t')

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
hf : Injective2 f
⊢ image2 f (↑s) (↑t ∩ ↑t') = image2 f ↑s ↑t ∩ image2 f ↑s ↑t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
hf : Injective2 f
⊢ image2 f (↑s) (↑t ∩ ↑t') = image2 f ↑s ↑t ∩ image2 f ↑s ↑t'

Tactic:
exact image2_inter_right hf

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma _root_.Function.Semiconj.preimage_dynEntourage {Y : Type*} {S : X → X} {T : Y → Y} {φ : X → Y}
    (h : Function.Semiconj φ S T) (U : Set (Y × Y)) (n : ℕ) :
    (map φ φ)⁻¹' (dynEntourage T U n) = dynEntourage S ((map φ φ)⁻¹' U) n

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ map φ φ ⁻¹' ((map T T)^[k] ⁻¹' U) = (map S S)^[k] ⁻¹' (map φ φ ⁻¹' U)

Tactic:
rw [← preimage_comp, ← preimage_comp, map_iterate S S k, map_iterate T T k, map_comp_map,
  map_comp_map, (Function.Semiconj.iterate_right h k).comp_eq]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ map φ φ ⁻¹' dynEntourage T U n = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
rw [dynEntourage, preimage_iInter₂]

Result:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ ⋂ i, ⋂ (_ : i < n), map φ φ ⁻¹' ((map T T)^[i] ⁻¹' U) = dynEntourage S (map φ φ ⁻¹' U) n

Proof state:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ ⋂ i, ⋂ (_ : i < n), map φ φ ⁻¹' ((map T T)^[i] ⁻¹' U) = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
refine iInter₂_congr fun k _ ↦ ?_

Result:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ map φ φ ⁻¹' ((map T T)^[k] ⁻¹' U) = (map S S)^[k] ⁻¹' (map φ φ ⁻¹' U)
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum'_ground_eq (M : ι → Matroid α) :
    (Matroid.sum' M).E = ⋃ i, Prod.mk i '' (M i).E

Proof state:
case h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
x✝ : ι × α
⊢ x✝ ∈ (Matroid.sum' M).E ↔ x✝ ∈ ⋃ i, Prod.mk i '' (M i).E

Tactic:
simp [Matroid.sum']

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
⊢ (Matroid.sum' M).E = ⋃ i, Prod.mk i '' (M i).E

Tactic:
ext

Result:
case h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
x✝ : ι × α
⊢ x✝ ∈ (Matroid.sum' M).E ↔ x✝ ∈ ⋃ i, Prod.mk i '' (M i).E
-- Mathlib/Algebra/Homology/Augment.lean
theorem chainComplex_d_succ_succ_zero (C : ChainComplex V ℕ) (i : ℕ) : C.d (i + 2) 0 = 0

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel (i + 2) 0

Tactic:
exact i.succ_succ_ne_one.symm

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ C.d (i + 2) 0 = 0

Tactic:
rw [C.shape]

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel (i + 2) 0
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem le_sum {ι} (f : ι → Cardinal) (i) : f i ≤ sum f

Proof state:
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
i : ι
⊢ f i ≤ sum f

Tactic:
rw [← Quotient.out_eq (f i)]

Result:
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
i : ι
⊢ ⟦Quotient.out (f i)⟧ ≤ sum f

Proof state:
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
i : ι
a b : Quotient.out (f i)
h : (fun a => ⟨i, a⟩) a = (fun a => ⟨i, a⟩) b
⊢ a = b

Tactic:
injection h

Result:
no goals

Proof state:
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
i : ι
⊢ ⟦Quotient.out (f i)⟧ ≤ sum f

Tactic:
exact ⟨⟨fun a => ⟨i, a⟩, fun a b h => by injection h⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
    (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b)

Proof state:
w : Nat
x y : BitVec w
a b : Bool
⊢ x.concat a ^^^ y.concat b = (x ^^^ y).concat (a ^^ b)

Tactic:
ext (_ | i) h <;> simp [getLsbD_concat]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem isCyclic_of_card_pow_eq_one_le : IsCyclic α :=
  have : Finset.Nonempty {a : α | orderOf a = Nat.card α} :=
    card_pos.1 <| by
      rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]
      apply Fintype.card_pos
  let ⟨x, hx⟩ := this
  isCyclic_of_orderOf_eq_card x (Finset.mem_filter.1 hx).2

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < Fintype.card α

Tactic:
apply Fintype.card_pos

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < #(filter (fun a => orderOf a = Nat.card α) univ)

Tactic:
rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]

Result:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
⊢ 0 < Fintype.card α
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_target_subset_range (x : M) : (extChartAt I x).target ⊆ range I

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
⊢ (extChartAt I x).target ⊆ range ↑I

Tactic:
simp only [mfld_simps]

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem pathConnectedSpace_iff_connectedSpace : PathConnectedSpace X ↔ ConnectedSpace X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
⊢ PathConnectedSpace X ↔ ConnectedSpace X

Tactic:
refine ⟨fun _ ↦ inferInstance, fun h ↦ ⟨inferInstance, fun x y ↦ ?_⟩⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
h : ConnectedSpace X
x y : X
⊢ Joined x y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
h : ConnectedSpace X
x y : X
⊢ Joined x y

Tactic:
rw [← mem_pathComponent_iff, (IsClopen.pathComponent _).eq_univ] <;> simp

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
/-- The characteristic is zero if the exponential characteristic is one. -/
lemma charZero_of_expChar_one' [hq : ExpChar R 1] : CharZero R

Proof state:
case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R

Tactic:
assumption

Result:
no goals

Proof state:
case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R

Tactic:
exact False.elim (CharP.char_ne_one R 1 rfl)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hq : ExpChar R 1
⊢ CharZero R

Tactic:
cases hq

Result:
case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R

case prime
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hprime✝ : Nat.Prime 1
hchar✝ : CharP R 1
⊢ CharZero R
-- Mathlib/Tactic/NormNum/PowMod.lean
theorem IsNatPowModT.bit0 :
    IsNatPowModT (Nat.mod (Nat.pow a b) m = c) a (nat_lit 2 * b) m (Nat.mod (Nat.mul c c) m) :=
  ⟨fun h1 => by simp only [two_mul, Nat.pow_eq, pow_add, ← h1, Nat.mul_eq]; exact Nat.mul_mod ..⟩

Proof state:
a b m : ℕ
c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a ^ b * a ^ b).mod m = ((a ^ b).mod m * (a ^ b).mod m).mod m

Tactic:
exact Nat.mul_mod ..

Result:
no goals

Proof state:
a b m : ℕ
c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a.pow (2 * b)).mod m = (c.mul c).mod m

Tactic:
simp only [two_mul, Nat.pow_eq, pow_add, ← h1, Nat.mul_eq]

Result:
a b m : ℕ
c : ℕ
h1 : (a.pow b).mod m = c
⊢ (a ^ b * a ^ b).mod m = ((a ^ b).mod m * (a ^ b).mod m).mod m
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_compl_eq_mk_compl_infinite {α : Type*} [Infinite α] {s t : Set α} (hs : #s < #α)
    (ht : #t < #α) : #(sᶜ : Set α) = #(tᶜ : Set α)

Proof state:
α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #↑sᶜ = #↑tᶜ

Tactic:
rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem separable_X_add_C (a : R) : (X + C a).Separable

Proof state:
R : Type u
inst✝ : CommSemiring R
a : R
⊢ (X + C a).Separable

Tactic:
rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero]

Result:
R : Type u
inst✝ : CommSemiring R
a : R
⊢ IsCoprime (X + C a) 1

Proof state:
R : Type u
inst✝ : CommSemiring R
a : R
⊢ IsCoprime (X + C a) 1

Tactic:
exact isCoprime_one_right

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one {f : ι → κ → G} {s : Set κ}
    {l : Filter ι} :
    UniformCauchySeqOn f l s ↔
      TendstoUniformlyOn (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) s

Proof state:
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) s

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
  uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
  SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_lt_one_mul {z1 z2 : ℤ_[p]} (hz2 : ‖z2‖ < 1) : ‖z1 * z2‖ < 1 :=
  calc
    ‖z1 * z2‖ = ‖z1‖ * ‖z2‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
hz2 : ‖z2‖ < 1
⊢ ‖z1 * z2‖ = ‖z1‖ * ‖z2‖

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem prod_map_atTop_eq {α₁ α₂ β₁ β₂ : Type*} [Preorder β₁] [Preorder β₂]
    (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

Proof state:
α₁ : Type u_6
α₂ : Type u_7
β₁ : Type u_8
β₂ : Type u_9
inst✝¹ : Preorder β₁
inst✝ : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop

Tactic:
rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.dvd_of_dvd_mul_left (H1 : IsCoprime x y) (H2 : x ∣ y * z) : x ∣ z

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ z

Tactic:
rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * (y * z)

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
⊢ x ∣ z

Tactic:
let ⟨a, b, H⟩ := H1

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ z

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * (y * z)

Tactic:
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)

Result:
no goals
-- Mathlib/GroupTheory/Transfer.lean
lemma transferTransversal_apply' (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
    (k : ZMod (minimalPeriod (g • ·) q.out)) :
    ↑((transferTransversal H g).2.leftQuotientEquiv (g ^ (cast k : ℤ) • q.out)) =
      g ^ (cast k : ℤ) * q.out.out

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x => g • x) (Quotient.out q))
⊢ ↑(⋯.leftQuotientEquiv (g ^ k.cast • Quotient.out q)) = g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply,
  apply_symm_apply]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_pos {m : ℕ∞} : 0 < (m : Cardinal) ↔ 0 < m

Proof state:
m : ℕ∞
⊢ 0 < ↑m ↔ 0 < m

Tactic:
norm_cast

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem seqTendstoAeSeq_succ (hfg : TendstoInMeasure μ f atTop g) {n : ℕ} :
    seqTendstoAeSeq hfg (n + 1) =
      max (seqTendstoAeSeqAux hfg (n + 1)) (seqTendstoAeSeq hfg n + 1)

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ seqTendstoAeSeq hfg (n + 1) = seqTendstoAeSeqAux hfg (n + 1) ⊔ (seqTendstoAeSeq hfg n + 1)

Tactic:
rw [seqTendstoAeSeq]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndep.meas_iInter [Fintype ι] (hμ : iIndep m μ) (hs : ∀ i, MeasurableSet[m i] (s i)) :
    μ (⋂ i, s i) = ∏ i, μ (s i)

Proof state:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
x✝ : MeasurableSpace Ω
μ : Measure Ω
s : ι → Set Ω
inst✝ : Fintype ι
hμ : iIndep m μ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ μ (⋂ i, s i) = ∏ i : ι, μ (s i)

Tactic:
simp [← hμ.meas_biInter fun _ _ ↦ hs _]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
lemma coverEntropyInf_restrict_subset [UniformSpace X] {T : X → X} {F G : Set X} (hF : F ⊆ G)
    (hG : MapsTo T G G) :
    coverEntropyInf (hG.restrict T G G) (val ⁻¹' F) = coverEntropyInf T F

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropyInf (MapsTo.restrict T G G hG) (val ⁻¹' F) = coverEntropyInf T F

Tactic:
rw [← coverEntropyInf_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
  inter_eq_right.2 hF]

Result:
no goals
-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem IsAssociatedPrime.annihilator_le (h : IsAssociatedPrime I M) :
    (⊤ : Submodule R M).annihilator ≤ I

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hI : Ideal.IsPrime (ker (toSpanSingleton R M x))
⊢ ⊤.annihilator ≤ ker (toSpanSingleton R M x)

Tactic:
rw [← Submodule.annihilator_span_singleton]

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hI : Ideal.IsPrime (ker (toSpanSingleton R M x))
⊢ ⊤.annihilator ≤ (Submodule.span R {x}).annihilator

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hI : Ideal.IsPrime (ker (toSpanSingleton R M x))
⊢ ⊤.annihilator ≤ (Submodule.span R {x}).annihilator

Tactic:
exact Submodule.annihilator_mono le_top

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsAssociatedPrime I M
⊢ ⊤.annihilator ≤ I

Tactic:
obtain ⟨hI, x, rfl⟩ := h

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hI : Ideal.IsPrime (ker (toSpanSingleton R M x))
⊢ ⊤.annihilator ≤ ker (toSpanSingleton R M x)
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isLE_of_iso (n : ℤ) [K.IsLE n] : L.IsLE n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsLE n
⊢ L.IsLE n

Tactic:
apply isSupported_of_iso e

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem inf [SemilatticeInf β] [ContinuousInf β] (hf : FinStronglyMeasurable f μ)
    (hg : FinStronglyMeasurable g μ) : FinStronglyMeasurable (f ⊓ g) μ

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊓ g) μ

Tactic:
refine
  ⟨fun n => hf.approx n ⊓ hg.approx n, fun n => ?_, fun x =>
    (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑((fun n => hf.approx n ⊓ hg.approx n) n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑((fun n => hf.approx n ⊓ hg.approx n) n)) < ⊤

Tactic:
refine (measure_mono (support_inf _ _)).trans_lt ?_

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑(hf.approx n) ∪ support ⇑(hg.approx n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝³ : TopologicalSpace β
inst✝² : Zero β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
n : ℕ
⊢ μ (support ⇑(hf.approx n) ∪ support ⇑(hg.approx n)) < ⊤

Tactic:
exact measure_union_lt_top_iff.mpr ⟨hf.fin_support_approx n, hg.fin_support_approx n⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : Array α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) :
    xs.findIdx? q = none → xs.findIdx? p = none

Proof state:
case mk
α : Type u_1
p q : α → Bool
xs : List α
w : ∀ (x : α), x ∈ { toList := xs } → p x = true → q x = true
⊢ findIdx? q { toList := xs } = none → findIdx? p { toList := xs } = none

Tactic:
simpa using List.findIdx?_eq_none_of_findIdx?_eq_none (by simpa using w)

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p q : α → Bool
w : ∀ (x : α), x ∈ xs → p x = true → q x = true
⊢ findIdx? q xs = none → findIdx? p xs = none

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p q : α → Bool
xs : List α
w : ∀ (x : α), x ∈ { toList := xs } → p x = true → q x = true
⊢ findIdx? q { toList := xs } = none → findIdx? p { toList := xs } = none

Proof state:
α : Type u_1
p q : α → Bool
xs : List α
w : ∀ (x : α), x ∈ { toList := xs } → p x = true → q x = true
⊢ ∀ (x : α), x ∈ xs → p x = true → q x = true

Tactic:
simpa using w

Result:
no goals